Theorem fo_perm ≪ | index | src | ≫

\fo置换

theorem fo_perm {x y: set} (A: wff x y): $ \fo x \fo y A \iff \fo y \fo x A $;
StepHypRefExpression
1 iff_comp 
(\fo x \fo y A \imp \fo y \fo x A) \imp (\fo y \fo x A \imp \fo x \fo y A) \imp (\fo x \fo y A \iff \fo y \fo x A)
2 fo_swap 
\fo x \fo y A \imp \fo y \fo x A
3 1, 2 ax_mp 
(\fo y \fo x A \imp \fo x \fo y A) \imp (\fo x \fo y A \iff \fo y \fo x A)
4 fo_swap 
\fo y \fo x A \imp \fo x \fo y A
5 3, 4 ax_mp 
\fo x \fo y A \iff \fo y \fo x A

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3, ax_11)