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	sb8f	⊢ ( ∀ 𝑥 [ 𝑡 / 𝑦 ] 𝜑 ↔ ∀ 𝑧 [ 𝑧 / 𝑥 ] [ 𝑡 / 𝑦 ] 𝜑 )
13	12	albii	⊢ ( ∀ 𝑡 ∀ 𝑥 [ 𝑡 / 𝑦 ] 𝜑 ↔ ∀ 𝑡 ∀ 𝑧 [ 𝑧 / 𝑥 ] [ 𝑡 / 𝑦 ] 𝜑 )
14	10 13	sylibr	⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 → ∀ 𝑡 ∀ 𝑥 [ 𝑡 / 𝑦 ] 𝜑 )
15		sbal	⊢ ( [ 𝑡 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑥 [ 𝑡 / 𝑦 ] 𝜑 )
16	15	albii	⊢ ( ∀ 𝑡 [ 𝑡 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑡 ∀ 𝑥 [ 𝑡 / 𝑦 ] 𝜑 )
17	14 16	sylibr	⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 → ∀ 𝑡 [ 𝑡 / 𝑦 ] ∀ 𝑥 𝜑 )
18	3	nfal	⊢ Ⅎ 𝑡 ∀ 𝑥 𝜑
19	18	sb8f	⊢ ( ∀ 𝑦 ∀ 𝑥 𝜑 ↔ ∀ 𝑡 [ 𝑡 / 𝑦 ] ∀ 𝑥 𝜑 )
20	17 19	sylibr	⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 → ∀ 𝑦 ∀ 𝑥 𝜑 )