Metamath Proof Explorer

Theorem ab0OLD

Description: Obsolete version of ab0 as of 8-Sep-2024. (Contributed by BJ, 19-Mar-2021) Avoid df-clel , ax-8 . (Revised by Gino Giotto, 30-Aug-2024) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion ab0OLD 
|- ( { x | ph } = (/) <-> A. x -. ph )

Proof

Step Hyp Ref Expression
1 dfnul4 
 |-  (/) = { x | F. }
2 1 eqeq2i 
 |-  ( { x | ph } = (/) <-> { x | ph } = { x | F. } )
3 dfcleq 
 |-  ( { x | ph } = { x | F. } <-> A. y ( y e. { x | ph } <-> y e. { x | F. } ) )
4 df-clab 
 |-  ( y e. { x | ph } <-> [ y / x ] ph )
5 sb6 
 |-  ( [ y / x ] ph <-> A. x ( x = y -> ph ) )
6 4 5 bitri 
 |-  ( y e. { x | ph } <-> A. x ( x = y -> ph ) )
7 df-clab 
 |-  ( y e. { x | F. } <-> [ y / x ] F. )
8 sbv 
 |-  ( [ y / x ] F. <-> F. )
9 7 8 bitri 
 |-  ( y e. { x | F. } <-> F. )
10 6 9 bibi12i 
 |-  ( ( y e. { x | ph } <-> y e. { x | F. } ) <-> ( A. x ( x = y -> ph ) <-> F. ) )
11 10 albii 
 |-  ( A. y ( y e. { x | ph } <-> y e. { x | F. } ) <-> A. y ( A. x ( x = y -> ph ) <-> F. ) )
12 nbfal 
 |-  ( -. A. x ( x = y -> ph ) <-> ( A. x ( x = y -> ph ) <-> F. ) )
13 12 bicomi 
 |-  ( ( A. x ( x = y -> ph ) <-> F. ) <-> -. A. x ( x = y -> ph ) )
14 13 albii 
 |-  ( A. y ( A. x ( x = y -> ph ) <-> F. ) <-> A. y -. A. x ( x = y -> ph ) )
15 nfna1 
 |-  F/ x -. A. x ( x = y -> ph )
16 nfv 
 |-  F/ y -. ph
17 pm2.27 
 |-  ( x = y -> ( ( x = y -> ph ) -> ph ) )
18 17 spsd 
 |-  ( x = y -> ( A. x ( x = y -> ph ) -> ph ) )
19 18 equcoms 
 |-  ( y = x -> ( A. x ( x = y -> ph ) -> ph ) )
20 ax12v 
 |-  ( x = y -> ( ph -> A. x ( x = y -> ph ) ) )
21 20 equcoms 
 |-  ( y = x -> ( ph -> A. x ( x = y -> ph ) ) )
22 19 21 impbid 
 |-  ( y = x -> ( A. x ( x = y -> ph ) <-> ph ) )
23 22 notbid 
 |-  ( y = x -> ( -. A. x ( x = y -> ph ) <-> -. ph ) )
24 15 16 23 cbvalv1 
 |-  ( A. y -. A. x ( x = y -> ph ) <-> A. x -. ph )
25 11 14 24 3bitri 
 |-  ( A. y ( y e. { x | ph } <-> y e. { x | F. } ) <-> A. x -. ph )
26 2 3 25 3bitri 
 |-  ( { x | ph } = (/) <-> A. x -. ph )