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

Metamath Proof Explorer

Theorem rabeq0w

Description: Condition for a restricted class abstraction to be empty. Version of rabeq0 using implicit substitution, which does not require ax-10 , ax-11 , ax-12 , but requires ax-8 . (Contributed by GG, 30-Sep-2024)

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

Proof

Step Hyp Ref Expression
1 rabeq0w.1 
 |-  ( x = y -> ( ph <-> ps ) )
2 eleq1w 
 |-  ( x = y -> ( x e. A <-> y e. A ) )
3 2 1 anbi12d 
 |-  ( x = y -> ( ( x e. A /\ ph ) <-> ( y e. A /\ ps ) ) )
4 3 ab0w 
 |-  ( { x | ( x e. A /\ ph ) } = (/) <-> A. y -. ( y e. A /\ ps ) )
5 df-rab 
 |-  { x e. A | ph } = { x | ( x e. A /\ ph ) }
6 5 eqeq1i 
 |-  ( { x e. A | ph } = (/) <-> { x | ( x e. A /\ ph ) } = (/) )
7 raln 
 |-  ( A. y e. A -. ps <-> A. y -. ( y e. A /\ ps ) )
8 4 6 7 3bitr4i 
 |-  ( { x e. A | ph } = (/) <-> A. y e. A -. ps )