![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > epelc | Structured version Visualization version Unicode version |
Description: The epsilon relationship and the membership relation are the same. (Contributed by Scott Fenton, 11-Apr-2012.) |
Ref | Expression |
---|---|
epelc.1 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
epelc |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | epelc.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | epelg 4745 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | 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 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-9 1895 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 ax-sep 4524 ax-nul 4533 ax-pr 4638 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 986 df-tru 1446 df-ex 1663 df-nf 1667 df-sb 1797 df-eu 2302 df-mo 2303 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-ne 2623 df-rab 2745 df-v 3046 df-dif 3406 df-un 3408 df-in 3410 df-ss 3417 df-nul 3731 df-if 3881 df-sn 3968 df-pr 3970 df-op 3974 df-br 4402 df-opab 4461 df-eprel 4744 |
This theorem is referenced by: epel 4747 epini 5197 smoiso 7078 smoiso2 7085 ecid 7425 ordiso2 8027 oismo 8052 cantnflt 8174 cantnfp1lem3 8182 oemapso 8184 cantnflem1b 8188 cantnflem1 8191 cantnf 8195 wemapwe 8199 cnfcomlem 8201 cnfcom 8202 cnfcom3lem 8205 leweon 8439 r0weon 8440 alephiso 8526 fin23lem27 8755 fpwwe2lem9 9060 ex-eprel 25876 dftr6 30383 coep 30384 coepr 30385 brsset 30649 brtxpsd 30654 brcart 30692 dfrecs2 30710 dfrdg4 30711 cnambfre 31982 wepwsolem 35894 dnwech 35900 |
Copyright terms: Public domain | W3C validator |