Theorem ab0w

Description: The class of sets verifying a property is the empty class if and only if that property is a contradiction. Version of ab0 using implicit substitution, which requires fewer axioms. (Contributed by GG, 3-Oct-2024)

	Ref	Expression
Hypothesis	ab0w.1	|- ( x = y -> ( ph <-> ps ) )
Assertion	ab0w	|- ( { x | ph } = (/) <-> A. y -. ps )

Proof

Step	Hyp	Ref	Expression
1		ab0w.1	|- ( x = y -> ( ph <-> ps ) )
2		dfnul4	|- (/) = { x | F. }
3	2	eqeq2i	|- ( { x | ph } = (/) <-> { x | ph } = { x | F. } )
4		df-clab	|- ( y e. { x | F. } <-> [ y / x ] F. )
5		sbv	|- ( [ y / x ] F. <-> F. )
6	4 5	bitri	|- ( y e. { x | F. } <-> F. )
7	6	bibi2i	|- ( ( ps <-> y e. { x | F. } ) <-> ( ps <-> F. ) )
8	7	albii	|- ( A. y ( ps <-> y e. { x | F. } ) <-> A. y ( ps <-> F. ) )
9	1	eqabcbw	|- ( { x | ph } = { x | F. } <-> A. y ( ps <-> y e. { x | F. } ) )
10		nbfal	|- ( -. ps <-> ( ps <-> F. ) )
11	10	albii	|- ( A. y -. ps <-> A. y ( ps <-> F. ) )
12	8 9 11	3bitr4i	|- ( { x | ph } = { x | F. } <-> A. y -. ps )
13	3 12	bitri	|- ( { x | ph } = (/) <-> A. y -. ps )