![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elab2 | Structured version Visualization version 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 3198 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | ax-mp 5 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 |
This theorem depends on definitions: df-bi 190 df-an 377 df-tru 1457 df-ex 1674 df-nf 1678 df-sb 1808 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2591 df-v 3058 |
This theorem is referenced by: elpw 3968 elint 4253 opabid 4721 elrn2 5092 elimasn 5211 oprabid 6341 wfrlem3a 7063 tfrlem3a 7120 cardprclem 8438 iunfictbso 8570 aceq3lem 8576 dfac5lem4 8582 kmlem9 8613 domtriomlem 8897 ltexprlem3 9488 ltexprlem4 9489 reclem2pr 9498 reclem3pr 9499 supsrlem 9560 supaddc 10601 supadd 10602 supmul1 10603 supmullem1 10604 supmullem2 10605 supmul 10606 sqrlem6 13359 infcvgaux2i 13964 mertenslem1 13988 mertenslem2 13989 4sqlem12 14948 conjnmzb 16965 sylow3lem2 17328 mdetunilem9 19693 txuni2 20628 xkoopn 20652 met2ndci 21585 2sqlem8 24348 2sqlem11 24351 eulerpartlemt 29252 eulerpartlemr 29255 eulerpartlemn 29262 subfacp1lem3 29953 subfacp1lem5 29955 soseq 30540 nofulllem5 30643 finxpsuclem 31833 heiborlem1 32187 heiborlem6 32192 heiborlem8 32194 cllem0 36214 |
Copyright terms: Public domain | W3C validator |