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	|- ( ph -> -. x e. A )
Assertion	eq0rdv	|- ( ph -> A = (/) )

Proof

Step	Hyp	Ref	Expression
1		eq0rdv.1	|- ( ph -> -. x e. A )
2	1	alrimiv	|- ( ph -> A. x -. x e. A )
3		dfnul4	|- (/) = { y | F. }
4	3	eqeq2i	|- ( A = (/) <-> A = { y | F. } )
5		dfcleq	|- ( A = { y | F. } <-> A. x ( x e. A <-> x e. { y | F. } ) )
6		df-clab	|- ( x e. { y | F. } <-> [ x / y ] F. )
7		sbv	|- ( [ x / y ] F. <-> F. )
8	6 7	bitri	|- ( x e. { y | F. } <-> F. )
9	8	bibi2i	|- ( ( x e. A <-> x e. { y | F. } ) <-> ( x e. A <-> F. ) )
10	9	albii	|- ( A. x ( x e. A <-> x e. { y | F. } ) <-> A. x ( x e. A <-> F. ) )
11		nbfal	|- ( -. x e. A <-> ( x e. A <-> F. ) )
12	11	bicomi	|- ( ( x e. A <-> F. ) <-> -. x e. A )
13	12	albii	|- ( A. x ( x e. A <-> F. ) <-> A. x -. x e. A )
14	10 13	bitri	|- ( A. x ( x e. A <-> x e. { y | F. } ) <-> A. x -. x e. A )
15	4 5 14	3bitrri	|- ( A. x -. x e. A <-> A = (/) )
16	2 15	sylib	|- ( ph -> A = (/) )