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φψ
elrab2w.2 y=Aψχ
elrab2w.3 C=xB|φ
Assertion elrab2w ACABχ

Proof

Step Hyp Ref Expression
1 elrab2w.1 x=yφψ
2 elrab2w.2 y=Aψχ
3 elrab2w.3 C=xB|φ
4 elex ACAV
5 elex ABAV
6 5 adantr ABχAV
7 eleq1w x=yxByB
8 7 1 anbi12d x=yxBφyBψ
9 eleq1 y=AyBAB
10 9 2 anbi12d y=AyBψABχ
11 df-rab xB|φ=x|xBφ
12 3 11 eqtri C=x|xBφ
13 8 10 12 elab2gw AVACABχ
14 4 6 13 pm5.21nii ACABχ