![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dfclel | Structured version Visualization version GIF version |
Description: Characterization of the elements of a class. (Contributed by BJ, 27-Jun-2019.) |
Ref | Expression |
---|---|
dfclel | ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cleljust 2107 | . 2 ⊢ (𝑦 ∈ 𝑧 ↔ ∃𝑢(𝑢 = 𝑦 ∧ 𝑢 ∈ 𝑧)) | |
2 | cleljust 2107 | . 2 ⊢ (𝑡 ∈ 𝑡 ↔ ∃𝑣(𝑣 = 𝑡 ∧ 𝑣 ∈ 𝑡)) | |
3 | 1, 2 | df-clel 2802 | 1 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 394 = wceq 1533 ∃wex 1773 ∈ wcel 2098 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-clel 2802 |
This theorem is referenced by: elex2 2804 issetlem 2805 elissetv 2806 eleq1w 2808 eleq2w 2809 eleq1d 2810 eleq2d 2811 eleq2dALT 2812 clelabOLD 2872 clabel 2873 nfeld 2903 risset 3220 elexOLD 3481 elrabi 3673 sbcimdv 3847 sbcg 3852 sbcabel 3868 ssel 3970 noel 4330 noelOLD 4331 disjsn 4717 pwpw0 4818 mptpreima 6244 fi1uzind 14494 brfi1indALT 14497 ballotlem2 34239 lfuhgr3 34860 eldm3 35486 eliminable3a 36471 eliminable3b 36472 eliminable-abelv 36477 eliminable-abelab 36478 bj-denoteslem 36479 bj-issetwt 36483 bj-elsngl 36578 wl-dfclab 37194 |
Copyright terms: Public domain | W3C validator |