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 ( ∀ 𝑥𝑦 𝜑 → ∀ 𝑦𝑥 𝜑 )

Proof

Step Hyp Ref Expression
1 2stdpc4 ( ∀ 𝑥𝑦 𝜑 → [ 𝑧 / 𝑥 ] [ 𝑡 / 𝑦 ] 𝜑 )
2 1 gen2 𝑡𝑧 ( ∀ 𝑥𝑦 𝜑 → [ 𝑧 / 𝑥 ] [ 𝑡 / 𝑦 ] 𝜑 )
3 nfv 𝑡 𝜑
4 3 nfal 𝑡𝑦 𝜑
5 4 nfal 𝑡𝑥𝑦 𝜑
6 nfv 𝑧 𝜑
7 6 nfal 𝑧𝑦 𝜑
8 7 nfal 𝑧𝑥𝑦 𝜑
9 5 8 2stdpc5 ( ∀ 𝑡𝑧 ( ∀ 𝑥𝑦 𝜑 → [ 𝑧 / 𝑥 ] [ 𝑡 / 𝑦 ] 𝜑 ) → ( ∀ 𝑥𝑦 𝜑 → ∀ 𝑡𝑧 [ 𝑧 / 𝑥 ] [ 𝑡 / 𝑦 ] 𝜑 ) )
10 2 9 ax-mp ( ∀ 𝑥𝑦 𝜑 → ∀ 𝑡𝑧 [ 𝑧 / 𝑥 ] [ 𝑡 / 𝑦 ] 𝜑 )
11 6 nfsbv 𝑧 [ 𝑡 / 𝑦 ] 𝜑
12 11 sb8v ( ∀ 𝑥 [ 𝑡 / 𝑦 ] 𝜑 ↔ ∀ 𝑧 [ 𝑧 / 𝑥 ] [ 𝑡 / 𝑦 ] 𝜑 )
13 12 albii ( ∀ 𝑡𝑥 [ 𝑡 / 𝑦 ] 𝜑 ↔ ∀ 𝑡𝑧 [ 𝑧 / 𝑥 ] [ 𝑡 / 𝑦 ] 𝜑 )
14 10 13 sylibr ( ∀ 𝑥𝑦 𝜑 → ∀ 𝑡𝑥 [ 𝑡 / 𝑦 ] 𝜑 )
15 sbal ( [ 𝑡 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑥 [ 𝑡 / 𝑦 ] 𝜑 )
16 15 albii ( ∀ 𝑡 [ 𝑡 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑡𝑥 [ 𝑡 / 𝑦 ] 𝜑 )
17 14 16 sylibr ( ∀ 𝑥𝑦 𝜑 → ∀ 𝑡 [ 𝑡 / 𝑦 ] ∀ 𝑥 𝜑 )
18 3 nfal 𝑡𝑥 𝜑
19 18 sb8v ( ∀ 𝑦𝑥 𝜑 ↔ ∀ 𝑡 [ 𝑡 / 𝑦 ] ∀ 𝑥 𝜑 )
20 17 19 sylibr ( ∀ 𝑥𝑦 𝜑 → ∀ 𝑦𝑥 𝜑 )