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 ) )