Theorem en0r

Description: The empty set is equinumerous only to itself. (Contributed by BTernaryTau, 29-Nov-2024)

	Ref	Expression
Assertion	en0r	⊢ ( ∅ ≈ 𝐴 ↔ 𝐴 = ∅ )

Proof

Step	Hyp	Ref	Expression
1		encv	⊢ ( ∅ ≈ 𝐴 → ( ∅ ∈ V ∧ 𝐴 ∈ V ) )
2		breng	⊢ ( ( ∅ ∈ V ∧ 𝐴 ∈ V ) → ( ∅ ≈ 𝐴 ↔ ∃ 𝑓 𝑓 : ∅ –1-1-onto→ 𝐴 ) )
3	1 2	syl	⊢ ( ∅ ≈ 𝐴 → ( ∅ ≈ 𝐴 ↔ ∃ 𝑓 𝑓 : ∅ –1-1-onto→ 𝐴 ) )
4	3	ibi	⊢ ( ∅ ≈ 𝐴 → ∃ 𝑓 𝑓 : ∅ –1-1-onto→ 𝐴 )
5		f1o00	⊢ ( 𝑓 : ∅ –1-1-onto→ 𝐴 ↔ ( 𝑓 = ∅ ∧ 𝐴 = ∅ ) )
6	5	simprbi	⊢ ( 𝑓 : ∅ –1-1-onto→ 𝐴 → 𝐴 = ∅ )
7	6	exlimiv	⊢ ( ∃ 𝑓 𝑓 : ∅ –1-1-onto→ 𝐴 → 𝐴 = ∅ )
8	4 7	syl	⊢ ( ∅ ≈ 𝐴 → 𝐴 = ∅ )
9		0ex	⊢ ∅ ∈ V
10		f1oeq1	⊢ ( 𝑓 = ∅ → ( 𝑓 : ∅ –1-1-onto→ ∅ ↔ ∅ : ∅ –1-1-onto→ ∅ ) )
11		f1o0	⊢ ∅ : ∅ –1-1-onto→ ∅
12	9 10 11	ceqsexv2d	⊢ ∃ 𝑓 𝑓 : ∅ –1-1-onto→ ∅
13		breng	⊢ ( ( ∅ ∈ V ∧ ∅ ∈ V ) → ( ∅ ≈ ∅ ↔ ∃ 𝑓 𝑓 : ∅ –1-1-onto→ ∅ ) )
14	9 9 13	mp2an	⊢ ( ∅ ≈ ∅ ↔ ∃ 𝑓 𝑓 : ∅ –1-1-onto→ ∅ )
15	12 14	mpbir	⊢ ∅ ≈ ∅
16		breq2	⊢ ( 𝐴 = ∅ → ( ∅ ≈ 𝐴 ↔ ∅ ≈ ∅ ) )
17	15 16	mpbiri	⊢ ( 𝐴 = ∅ → ∅ ≈ 𝐴 )
18	8 17	impbii	⊢ ( ∅ ≈ 𝐴 ↔ 𝐴 = ∅ )