Theorem en0ALT

Description: Shorter proof of en0 , depending on ax-pow and ax-un . (Contributed by NM, 27-May-1998) (Proof modification is discouraged.) (New usage is discouraged.)

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

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	8	enref	⊢ ∅ ≈ ∅
10		breq1	⊢ ( 𝐴 = ∅ → ( 𝐴 ≈ ∅ ↔ ∅ ≈ ∅ ) )
11	9 10	mpbiri	⊢ ( 𝐴 = ∅ → 𝐴 ≈ ∅ )
12	7 11	impbii	⊢ ( 𝐴 ≈ ∅ ↔ 𝐴 = ∅ )