Theorem fo_or_insto_fo_ex ≪ | index | src | ≫

\fo\or插入成\ex

theorem fo_or_insto_fo_ex {x: set} (A B: wff x):
  $ \fo x (A \or B) \imp \fo x A \or \ex x B $;
StepHypRefExpression
1 imp_iff_tran_imp 
(\fo x (\neg A \imp B) \imp \ex x \neg A \imp \ex x B) \imp
  (\ex x \neg A \imp \ex x B \iff \neg \fo x A \imp \ex x B) \imp
  \fo x (\neg A \imp B) \imp
  \neg \fo x A \imp
  \ex x B
2 fo_imp_insto_ex 
\fo x (\neg A \imp B) \imp \ex x \neg A \imp \ex x B
3 1, 2 ax_mp 
(\ex x \neg A \imp \ex x B \iff \neg \fo x A \imp \ex x B) \imp \fo x (\neg A \imp B) \imp \neg \fo x A \imp \ex x B
4 iff_intror_imp 
(\ex x \neg A \iff \neg \fo x A) \imp (\ex x \neg A \imp \ex x B \iff \neg \fo x A \imp \ex x B)
5 exneg_eqv_negfo 
\ex x \neg A \iff \neg \fo x A
6 4, 5 ax_mp 
\ex x \neg A \imp \ex x B \iff \neg \fo x A \imp \ex x B
7 3, 6 ax_mp 
\fo x (\neg A \imp B) \imp \neg \fo x A \imp \ex x B
8 7 conv or 
\fo x (A \or B) \imp \fo x A \or \ex x B

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3, ax_gen, ax_4)