![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > epel | Structured version Visualization version GIF version |
Description: The membership relation and the membership predicate agree when the "containing" class is a setvar. Definition 1.6 of [Schloeder] p. 1. (Contributed by NM, 13-Aug-1995.) Replace the first setvar variable with a class variable. (Revised by BJ, 13-Sep-2022.) |
Ref | Expression |
---|---|
epel | ⊢ (𝐴 E 𝑥 ↔ 𝐴 ∈ 𝑥) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 3447 | . 2 ⊢ 𝑥 ∈ V | |
2 | 1 | epeli 5537 | 1 ⊢ (𝐴 E 𝑥 ↔ 𝐴 ∈ 𝑥) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∈ wcel 2106 class class class wbr 5103 E cep 5534 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 ax-sep 5254 ax-nul 5261 ax-pr 5382 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-ne 2942 df-rab 3406 df-v 3445 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4281 df-if 4485 df-sn 4585 df-pr 4587 df-op 4591 df-br 5104 df-opab 5166 df-eprel 5535 |
This theorem is referenced by: epse 5614 dfepfr 5616 epfrc 5617 wecmpep 5623 wetrep 5624 dmep 5877 rnep 5880 epweon 7705 epweonALT 7706 smoiso 8304 smoiso2 8311 ordunifi 9233 ordiso2 9447 ordtypelem8 9457 oismo 9472 wofib 9477 dford2 9552 noinfep 9592 oemapso 9614 wemapwe 9629 alephiso 10030 cflim2 10195 fin23lem27 10260 om2uzisoi 13851 bnj219 33214 nummin 33564 efrunt 34153 dftr6 34194 dffr5 34197 elpotr 34226 dfon2lem9 34236 dfon2 34237 brsset 34441 dfon3 34444 brbigcup 34450 brapply 34490 brcup 34491 brcap 34492 dfint3 34504 dfssr2 36928 onsupuni 41501 onsupmaxb 41511 |
Copyright terms: Public domain | W3C validator |