![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > epelc | Structured version Visualization version GIF version |
Description: The epsilon relationship and the membership relation are the same. (Contributed by Scott Fenton, 11-Apr-2012.) |
Ref | Expression |
---|---|
epelc.1 | ⊢ 𝐵 ∈ V |
Ref | Expression |
---|---|
epelc | ⊢ (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | epelc.1 | . 2 ⊢ 𝐵 ∈ V | |
2 | epelg 5178 | . 2 ⊢ (𝐵 ∈ V → (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∈ wcel 2137 Vcvv 3338 class class class wbr 4802 E cep 5176 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1869 ax-4 1884 ax-5 1986 ax-6 2052 ax-7 2088 ax-9 2146 ax-10 2166 ax-11 2181 ax-12 2194 ax-13 2389 ax-ext 2738 ax-sep 4931 ax-nul 4939 ax-pr 5053 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1633 df-ex 1852 df-nf 1857 df-sb 2045 df-eu 2609 df-mo 2610 df-clab 2745 df-cleq 2751 df-clel 2754 df-nfc 2889 df-ne 2931 df-rab 3057 df-v 3340 df-dif 3716 df-un 3718 df-in 3720 df-ss 3727 df-nul 4057 df-if 4229 df-sn 4320 df-pr 4322 df-op 4326 df-br 4803 df-opab 4863 df-eprel 5177 |
This theorem is referenced by: epel 5180 0sn0ep 5181 epini 5651 smoiso 7626 smoiso2 7633 ecid 7977 ordiso2 8583 oismo 8608 cantnflt 8740 cantnfp1lem3 8748 oemapso 8750 cantnflem1b 8754 cantnflem1 8757 cantnf 8761 wemapwe 8765 cnfcomlem 8767 cnfcom 8768 cnfcom3lem 8771 leweon 9022 r0weon 9023 alephiso 9109 fin23lem27 9340 fpwwe2lem9 9650 ex-eprel 27599 dftr6 31945 coep 31946 coepr 31947 brsset 32300 brtxpsd 32305 brcart 32343 dfrecs2 32361 dfrdg4 32362 cnambfre 33769 wepwsolem 38112 dnwech 38118 |
Copyright terms: Public domain | W3C validator |