Metamath Proof Explorer


Theorem en0OLD

Description: Obsolete version of en0 as of 23-Sep-2024. (Contributed by NM, 27-May-1998) Avoid ax-pow . (Revised by BTernaryTau, 31-Jul-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion en0OLD ( 𝐴 ≈ ∅ ↔ 𝐴 = ∅ )

Proof

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