Theorem eq0rdv

Description: Deduction for equality to the empty set. (Contributed by NM, 11-Jul-2014) Avoid ax-8 , df-clel . (Revised by Gino Giotto, 6-Sep-2024)

	Ref	Expression
Hypothesis	eq0rdv.1	⊢ ( 𝜑 → ¬ 𝑥 ∈ 𝐴 )
Assertion	eq0rdv	⊢ ( 𝜑 → 𝐴 = ∅ )

Proof

Step	Hyp	Ref	Expression
1		eq0rdv.1	⊢ ( 𝜑 → ¬ 𝑥 ∈ 𝐴 )
2	1	alrimiv	⊢ ( 𝜑 → ∀ 𝑥 ¬ 𝑥 ∈ 𝐴 )
3		dfnul4	⊢ ∅ = { 𝑦 ∣ ⊥ }
4	3	eqeq2i	⊢ ( 𝐴 = ∅ ↔ 𝐴 = { 𝑦 ∣ ⊥ } )
5		dfcleq	⊢ ( 𝐴 = { 𝑦 ∣ ⊥ } ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ { 𝑦 ∣ ⊥ } ) )
6		df-clab	⊢ ( 𝑥 ∈ { 𝑦 ∣ ⊥ } ↔ [ 𝑥 / 𝑦 ] ⊥ )
7		sbv	⊢ ( [ 𝑥 / 𝑦 ] ⊥ ↔ ⊥ )
8	6 7	bitri	⊢ ( 𝑥 ∈ { 𝑦 ∣ ⊥ } ↔ ⊥ )
9	8	bibi2i	⊢ ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ { 𝑦 ∣ ⊥ } ) ↔ ( 𝑥 ∈ 𝐴 ↔ ⊥ ) )
10	9	albii	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ { 𝑦 ∣ ⊥ } ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ⊥ ) )
11		nbfal	⊢ ( ¬ 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐴 ↔ ⊥ ) )
12	11	bicomi	⊢ ( ( 𝑥 ∈ 𝐴 ↔ ⊥ ) ↔ ¬ 𝑥 ∈ 𝐴 )
13	12	albii	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ⊥ ) ↔ ∀ 𝑥 ¬ 𝑥 ∈ 𝐴 )
14	10 13	bitri	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ { 𝑦 ∣ ⊥ } ) ↔ ∀ 𝑥 ¬ 𝑥 ∈ 𝐴 )
15	4 5 14	3bitrri	⊢ ( ∀ 𝑥 ¬ 𝑥 ∈ 𝐴 ↔ 𝐴 = ∅ )
16	2 15	sylib	⊢ ( 𝜑 → 𝐴 = ∅ )