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 | |
|
elrab2w.2 | |
||
elrab2w.3 | |
||
Assertion | elrab2w | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elrab2w.1 | |
|
2 | elrab2w.2 | |
|
3 | elrab2w.3 | |
|
4 | elex | |
|
5 | elex | |
|
6 | 5 | adantr | |
7 | eleq1w | |
|
8 | 7 1 | anbi12d | |
9 | eleq1 | |
|
10 | 9 2 | anbi12d | |
11 | df-rab | |
|
12 | 3 11 | eqtri | |
13 | 8 10 12 | elab2gw | |
14 | 4 6 13 | pm5.21nii | |