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	⊢ ∃ 𝑥 ∃ 𝑦 ¬ 𝑥 = 𝑦