Metamath Proof Explorer


Theorem ax11-pm2

Description: Proof of ax-11 from the standard axioms of predicate calculus, similar to PM's proof of alcom (PM*11.2). This proof requires that x and y be distinct. Axiom ax-11 is used in the proof only through nfal , nfsb , sbal , sb8 . See also ax11-pm . (Contributed by BJ, 15-Sep-2018) (Proof modification is discouraged.)

Ref Expression
Assertion ax11-pm2 x y φ y x φ

Proof

Step Hyp Ref Expression
1 2stdpc4 x y φ z x t y φ
2 1 gen2 t z x y φ z x t y φ
3 nfv t φ
4 3 nfal t y φ
5 4 nfal t x y φ
6 nfv z φ
7 6 nfal z y φ
8 7 nfal z x y φ
9 5 8 2stdpc5 t z x y φ z x t y φ x y φ t z z x t y φ
10 2 9 ax-mp x y φ t z z x t y φ
11 6 nfsbv z t y φ
12 11 sb8v x t y φ z z x t y φ
13 12 albii t x t y φ t z z x t y φ
14 10 13 sylibr x y φ t x t y φ
15 sbal t y x φ x t y φ
16 15 albii t t y x φ t x t y φ
17 14 16 sylibr x y φ t t y x φ
18 3 nfal t x φ
19 18 sb8v y x φ t t y x φ
20 17 19 sylibr x y φ y x φ