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

Metamath Proof Explorer

Theorem exexneq

Description: There exist two different sets. (Contributed by NM, 7-Nov-2006) Avoid ax-13 . (Revised by BJ, 31-May-2019) Avoid ax-8 . (Revised by SN, 21-Sep-2023) Avoid ax-12 . (Revised by Rohan Ridenour, 9-Oct-2024) Use ax-pr instead of ax-pow . (Revised by BTernaryTau, 3-Dec-2024) Extract this result from the proof of dtru . (Revised by BJ, 2-Jan-2025)

Ref Expression
Assertion exexneq ∃ 𝑥 ∃ 𝑦 ¬ 𝑥 = 𝑦

Proof

Step Hyp Ref Expression
1 exel ⊢ ∃ 𝑥 ∃ 𝑧 𝑧 ∈ 𝑥
2 ax-nul ⊢ ∃ 𝑦 ∀ 𝑧 ¬ 𝑧 ∈ 𝑦
3 exdistrv ⊢ ( ∃ 𝑥 ∃ 𝑦 ( ∃ 𝑧 𝑧 ∈ 𝑥 ∧ ∀ 𝑧 ¬ 𝑧 ∈ 𝑦 ) ↔ ( ∃ 𝑥 ∃ 𝑧 𝑧 ∈ 𝑥 ∧ ∃ 𝑦 ∀ 𝑧 ¬ 𝑧 ∈ 𝑦 ) )
4 1 2 3 mpbir2an ⊢ ∃ 𝑥 ∃ 𝑦 ( ∃ 𝑧 𝑧 ∈ 𝑥 ∧ ∀ 𝑧 ¬ 𝑧 ∈ 𝑦 )
5 ax9v1 ⊢ ( 𝑥 = 𝑦 → ( 𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) )
6 5 eximdv ⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑧 𝑧 ∈ 𝑥 → ∃ 𝑧 𝑧 ∈ 𝑦 ) )
7 df-ex ⊢ ( ∃ 𝑧 𝑧 ∈ 𝑦 ↔ ¬ ∀ 𝑧 ¬ 𝑧 ∈ 𝑦 )
8 6 7 imbitrdi ⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑧 𝑧 ∈ 𝑥 → ¬ ∀ 𝑧 ¬ 𝑧 ∈ 𝑦 ) )
9 8 com12 ⊢ ( ∃ 𝑧 𝑧 ∈ 𝑥 → ( 𝑥 = 𝑦 → ¬ ∀ 𝑧 ¬ 𝑧 ∈ 𝑦 ) )
10 9 con2d ⊢ ( ∃ 𝑧 𝑧 ∈ 𝑥 → ( ∀ 𝑧 ¬ 𝑧 ∈ 𝑦 → ¬ 𝑥 = 𝑦 ) )
11 10 imp ⊢ ( ( ∃ 𝑧 𝑧 ∈ 𝑥 ∧ ∀ 𝑧 ¬ 𝑧 ∈ 𝑦 ) → ¬ 𝑥 = 𝑦 )
12 11 2eximi ⊢ ( ∃ 𝑥 ∃ 𝑦 ( ∃ 𝑧 𝑧 ∈ 𝑥 ∧ ∀ 𝑧 ¬ 𝑧 ∈ 𝑦 ) → ∃ 𝑥 ∃ 𝑦 ¬ 𝑥 = 𝑦 )
13 4 12 ax-mp ⊢ ∃ 𝑥 ∃ 𝑦 ¬ 𝑥 = 𝑦