Metamath Proof Explorer


Theorem ensn1OLD

Description: Obsolete version of ensn1 as of 23-Sep-2024. (Contributed by NM, 4-Nov-2002) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis ensn1OLD.1 𝐴 ∈ V
Assertion ensn1OLD { 𝐴 } ≈ 1o

Proof

Step Hyp Ref Expression
1 ensn1OLD.1 𝐴 ∈ V
2 snex { ⟨ 𝐴 , ∅ ⟩ } ∈ V
3 f1oeq1 ( 𝑓 = { ⟨ 𝐴 , ∅ ⟩ } → ( 𝑓 : { 𝐴 } –1-1-onto→ { ∅ } ↔ { ⟨ 𝐴 , ∅ ⟩ } : { 𝐴 } –1-1-onto→ { ∅ } ) )
4 0ex ∅ ∈ V
5 1 4 f1osn { ⟨ 𝐴 , ∅ ⟩ } : { 𝐴 } –1-1-onto→ { ∅ }
6 2 3 5 ceqsexv2d 𝑓 𝑓 : { 𝐴 } –1-1-onto→ { ∅ }
7 bren ( { 𝐴 } ≈ { ∅ } ↔ ∃ 𝑓 𝑓 : { 𝐴 } –1-1-onto→ { ∅ } )
8 6 7 mpbir { 𝐴 } ≈ { ∅ }
9 df1o2 1o = { ∅ }
10 8 9 breqtrri { 𝐴 } ≈ 1o