This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )