Theorem eq0rdv

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

	Ref	Expression
Hypothesis	eq0rdv.1	$$⊢\phi \to \neg x\in A$$
Assertion	eq0rdv	$$⊢\phi \to A=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		eq0rdv.1	$$⊢\phi \to \neg x\in A$$
2	1	alrimiv	$$⊢\phi \to \forall x\neg x\in A$$
3		biidd	$$⊢y=x\to \left(\perp \leftrightarrow \perp \right)$$
4	3	eqabbw	$$⊢A=\left\{y|\perp \right\}\leftrightarrow \forall x\left(x\in A\leftrightarrow \perp \right)$$
5		dfnul4	$$⊢\varnothing =\left\{y|\perp \right\}$$
6	5	eqeq2i	$$⊢A=\varnothing \leftrightarrow A=\left\{y|\perp \right\}$$
7		nbfal	$$⊢\neg x\in A\leftrightarrow \left(x\in A\leftrightarrow \perp \right)$$
8	7	albii	$$⊢\forall x\neg x\in A\leftrightarrow \forall x\left(x\in A\leftrightarrow \perp \right)$$
9	4 6 8	3bitr4ri	$$⊢\forall x\neg x\in A\leftrightarrow A=\varnothing$$
10	2 9	sylib	$$⊢\phi \to A=\varnothing$$