Theorem ex_fo_swap ≪ | index | src | ≫

\ex\fo交换

theorem ex_fo_swap {x y: set} (A: wff x y):
  $ \ex x \fo y A \imp \fo y \ex x A $;

Step	Hyp	Ref	Expression
1		_nf_ex_same	\nf x \ex x A
2	1	_nf_clos_fo_difvar	\nf x \fo y \ex x A
3		ex_intro	A \imp \ex x A
4	3	imp_intro_fo	\fo y A \imp \fo y \ex x A
5	2, 4	imp_introls_ex_nfrs	\ex x \fo y A \imp \fo y \ex x A

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3, ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12)