Theorem iff_intro_ex ≪ | index | src | ≫

\iff引入\ex

theorem iff_intro_ex {x: set} (A B: wff x):
  $ A \iff B $ >
  $ \ex x A \iff \ex x B $;

Step	Hyp	Ref	Expression
1		fo_iff_insto_ex	\fo x (A \iff B) \imp (\ex x A \iff \ex x B)
2		hyp h	A \iff B
3	2	intro_fo	\fo x (A \iff B)
4	1, 3	ax_mp	\ex x A \iff \ex x B

Axiom use

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