This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrrdi ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧 ) → 𝑦 = 𝑧 ) )
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 ⊢ ∃ 𝑥 ( ( 𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧 ) → 𝑦 = 𝑧 )