Description: Membership in a class abstraction, using implicit substitution. (Closed theorem version of elabg .) (Contributed by NM, 7-Nov-2005) (Proof shortened by Andrew Salmon, 8-Jun-2011) Reduce axiom usage. (Revised by Gino Giotto, 12-Oct-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | elabgt | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elab6g | |
|
2 | 1 | adantr | |
3 | elisset | |
|
4 | biimp | |
|
5 | 4 | imim3i | |
6 | 5 | al2imi | |
7 | 19.23v | |
|
8 | 6 7 | syl6ib | |
9 | 8 | com3r | |
10 | biimpr | |
|
11 | 10 | imim2i | |
12 | 11 | alimi | |
13 | bi2.04 | |
|
14 | 13 | albii | |
15 | 19.21v | |
|
16 | 14 15 | sylbb | |
17 | 12 16 | syl | |
18 | 17 | a1i | |
19 | 9 18 | impbidd | |
20 | 3 19 | syl | |
21 | 20 | imp | |
22 | 2 21 | bitrd | |