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

Metamath Proof Explorer

Theorem elrab2w

Description: Membership in a restricted class abstraction. This is to elrab2 what elab2gw is to elab2g . (Contributed by SN, 2-Sep-2024)

Ref Expression
Hypotheses elrab2w.1 
|- ( x = y -> ( ph <-> ps ) )
elrab2w.2 
|- ( y = A -> ( ps <-> ch ) )
elrab2w.3 
|- C = { x e. B | ph }
Assertion elrab2w 
|- ( A e. C <-> ( A e. B /\ ch ) )

Proof

Step Hyp Ref Expression
1 elrab2w.1 
 |-  ( x = y -> ( ph <-> ps ) )
2 elrab2w.2 
 |-  ( y = A -> ( ps <-> ch ) )
3 elrab2w.3 
 |-  C = { x e. B | ph }
4 elex 
 |-  ( A e. C -> A e. _V )
5 elex 
 |-  ( A e. B -> A e. _V )
6 5 adantr 
 |-  ( ( A e. B /\ ch ) -> A e. _V )
7 eleq1w 
 |-  ( x = y -> ( x e. B <-> y e. B ) )
8 7 1 anbi12d 
 |-  ( x = y -> ( ( x e. B /\ ph ) <-> ( y e. B /\ ps ) ) )
9 eleq1 
 |-  ( y = A -> ( y e. B <-> A e. B ) )
10 9 2 anbi12d 
 |-  ( y = A -> ( ( y e. B /\ ps ) <-> ( A e. B /\ ch ) ) )
11 df-rab 
 |-  { x e. B | ph } = { x | ( x e. B /\ ph ) }
12 3 11 eqtri 
 |-  C = { x | ( x e. B /\ ph ) }
13 8 10 12 elab2gw 
 |-  ( A e. _V -> ( A e. C <-> ( A e. B /\ ch ) ) )
14 4 6 13 pm5.21nii 
 |-  ( A e. C <-> ( A e. B /\ ch ) )