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		dfcleq	|- ( { x | ph } = { x | F. } <-> A. y ( y e. { x | ph } <-> y e. { x | F. } ) )
5		df-clab	|- ( y e. { x | ph } <-> [ y / x ] ph )
6	1	sbievw	|- ( [ y / x ] ph <-> ps )
7	5 6	bitri	|- ( y e. { x | ph } <-> ps )
8	7	bibi1i	|- ( ( y e. { x | ph } <-> y e. { x | F. } ) <-> ( ps <-> y e. { x | F. } ) )
9		bicom	|- ( ( ps <-> y e. { x | F. } ) <-> ( y e. { x | F. } <-> ps ) )
10	8 9	bitri	|- ( ( y e. { x | ph } <-> y e. { x | F. } ) <-> ( y e. { x | F. } <-> ps ) )
11	10	albii	|- ( A. y ( y e. { x | ph } <-> y e. { x | F. } ) <-> A. y ( y e. { x | F. } <-> ps ) )
12	4 11	bitri	|- ( { x | ph } = { x | F. } <-> A. y ( y e. { x | F. } <-> ps ) )
13		df-clab	|- ( y e. { x | F. } <-> [ y / x ] F. )
14		sbv	|- ( [ y / x ] F. <-> F. )
15	13 14	bitri	|- ( y e. { x | F. } <-> F. )
16	15	bibi1i	|- ( ( y e. { x | F. } <-> ps ) <-> ( F. <-> ps ) )
17	16	albii	|- ( A. y ( y e. { x | F. } <-> ps ) <-> A. y ( F. <-> ps ) )
18		falim	|- ( F. -> ( ps -> -. ps ) )
19		idd	|- ( -. F. -> ( -. ps -> -. ps ) )
20	18 19	bija	|- ( ( F. <-> ps ) -> -. ps )
21		falim	|- ( F. -> ps )
22		id	|- ( ps -> ps )
23	21 22	pm5.21ni	|- ( -. ps -> ( F. <-> ps ) )
24	20 23	impbii	|- ( ( F. <-> ps ) <-> -. ps )
25	24	albii	|- ( A. y ( F. <-> ps ) <-> A. y -. ps )
26	17 25	bitri	|- ( A. y ( y e. { x | F. } <-> ps ) <-> A. y -. ps )
27	12 26	bitri	|- ( { x | ph } = { x | F. } <-> A. y -. ps )
28	3 27	bitri	|- ( { x | ph } = (/) <-> A. y -. ps )