![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > elab2 | Unicode version |
Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995.) |
Ref | Expression |
---|---|
elab2.1 | |
elab2.2 | |
elab2.3 |
Ref | Expression |
---|---|
elab2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elab2.1 | . 2 | |
2 | elab2.2 | . . 3 | |
3 | elab2.3 | . . 3 | |
4 | 2, 3 | elab2g 3248 | . 2 |
5 | 1, 4 | ax-mp 5 | 1 |
Colors of variables: wff setvar class |
Syntax hints: -> wi 4 <-> wb 184
= wceq 1395 e. wcel 1818 { cab 2442
cvv 3109 |
This theorem is referenced by: elpw 4018 elint 4292 opabid 4759 elrn2 5247 elimasn 5367 oprabid 6323 tfrlem3a 7065 cardprclem 8381 iunfictbso 8516 aceq3lem 8522 dfac5lem4 8528 kmlem9 8559 domtriomlem 8843 ltexprlem3 9437 ltexprlem4 9438 reclem2pr 9447 reclem3pr 9448 supsrlem 9509 supmul1 10533 supmullem1 10534 supmullem2 10535 supmul 10536 sqrlem6 13081 infcvgaux2i 13669 mertenslem1 13693 mertenslem2 13694 4sqlem12 14474 conjnmzb 16301 sylow3lem2 16648 mdetunilem9 19122 txuni2 20066 xkoopn 20090 met2ndci 21025 2sqlem8 23647 2sqlem11 23650 eulerpartlemt 28310 eulerpartlemr 28313 eulerpartlemn 28320 subfacp1lem3 28626 subfacp1lem5 28628 soseq 29334 nofulllem5 29466 supaddc 30041 supadd 30042 heiborlem1 30307 heiborlem6 30312 heiborlem8 30314 cllem0 37751 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1618 ax-4 1631 ax-5 1704 ax-6 1747 ax-7 1790 ax-10 1837 ax-11 1842 ax-12 1854 ax-13 1999 ax-ext 2435 |
This theorem depends on definitions: df-bi 185 df-an 371 df-tru 1398 df-ex 1613 df-nf 1617 df-sb 1740 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-v 3111 |
Copyright terms: Public domain | W3C validator |