Metamath Proof Explorer


Theorem axextnd

Description: A version of the Axiom of Extensionality with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 14-Aug-2003) (New usage is discouraged.)

Ref Expression
Assertion axextnd 𝑥 ( ( 𝑥𝑦𝑥𝑧 ) → 𝑦 = 𝑧 )

Proof

Step Hyp Ref Expression
1 nfnae 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑦
2 nfnae 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑧
3 1 2 nfan 𝑥 ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 )
4 nfcvf ( ¬ ∀ 𝑥 𝑥 = 𝑦 𝑥 𝑦 )
5 4 adantr ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → 𝑥 𝑦 )
6 5 nfcrd ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 𝑤𝑦 )
7 nfcvf ( ¬ ∀ 𝑥 𝑥 = 𝑧 𝑥 𝑧 )
8 7 adantl ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → 𝑥 𝑧 )
9 8 nfcrd ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 𝑤𝑧 )
10 6 9 nfbid ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 ( 𝑤𝑦𝑤𝑧 ) )
11 elequ1 ( 𝑤 = 𝑥 → ( 𝑤𝑦𝑥𝑦 ) )
12 elequ1 ( 𝑤 = 𝑥 → ( 𝑤𝑧𝑥𝑧 ) )
13 11 12 bibi12d ( 𝑤 = 𝑥 → ( ( 𝑤𝑦𝑤𝑧 ) ↔ ( 𝑥𝑦𝑥𝑧 ) ) )
14 13 a1i ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → ( 𝑤 = 𝑥 → ( ( 𝑤𝑦𝑤𝑧 ) ↔ ( 𝑥𝑦𝑥𝑧 ) ) ) )
15 3 10 14 cbvald ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → ( ∀ 𝑤 ( 𝑤𝑦𝑤𝑧 ) ↔ ∀ 𝑥 ( 𝑥𝑦𝑥𝑧 ) ) )
16 axextg ( ∀ 𝑤 ( 𝑤𝑦𝑤𝑧 ) → 𝑦 = 𝑧 )
17 15 16 syl6bir ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → ( ∀ 𝑥 ( 𝑥𝑦𝑥𝑧 ) → 𝑦 = 𝑧 ) )
18 19.8a ( 𝑦 = 𝑧 → ∃ 𝑥 𝑦 = 𝑧 )
19 17 18 syl6 ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → ( ∀ 𝑥 ( 𝑥𝑦𝑥𝑧 ) → ∃ 𝑥 𝑦 = 𝑧 ) )
20 19 ex ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ( ∀ 𝑥 ( 𝑥𝑦𝑥𝑧 ) → ∃ 𝑥 𝑦 = 𝑧 ) ) )
21 ax6e 𝑥 𝑥 = 𝑧
22 ax7 ( 𝑥 = 𝑦 → ( 𝑥 = 𝑧𝑦 = 𝑧 ) )
23 22 aleximi ( ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑥 𝑥 = 𝑧 → ∃ 𝑥 𝑦 = 𝑧 ) )
24 21 23 mpi ( ∀ 𝑥 𝑥 = 𝑦 → ∃ 𝑥 𝑦 = 𝑧 )
25 24 a1d ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 ( 𝑥𝑦𝑥𝑧 ) → ∃ 𝑥 𝑦 = 𝑧 ) )
26 ax6e 𝑥 𝑥 = 𝑦
27 ax7 ( 𝑥 = 𝑧 → ( 𝑥 = 𝑦𝑧 = 𝑦 ) )
28 equcomi ( 𝑧 = 𝑦𝑦 = 𝑧 )
29 27 28 syl6 ( 𝑥 = 𝑧 → ( 𝑥 = 𝑦𝑦 = 𝑧 ) )
30 29 aleximi ( ∀ 𝑥 𝑥 = 𝑧 → ( ∃ 𝑥 𝑥 = 𝑦 → ∃ 𝑥 𝑦 = 𝑧 ) )
31 26 30 mpi ( ∀ 𝑥 𝑥 = 𝑧 → ∃ 𝑥 𝑦 = 𝑧 )
32 31 a1d ( ∀ 𝑥 𝑥 = 𝑧 → ( ∀ 𝑥 ( 𝑥𝑦𝑥𝑧 ) → ∃ 𝑥 𝑦 = 𝑧 ) )
33 20 25 32 pm2.61ii ( ∀ 𝑥 ( 𝑥𝑦𝑥𝑧 ) → ∃ 𝑥 𝑦 = 𝑧 )
34 33 19.35ri 𝑥 ( ( 𝑥𝑦𝑥𝑧 ) → 𝑦 = 𝑧 )