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 2119 | . 2 ⊢ (𝑦 ∈ 𝑧 ↔ ∃𝑢(𝑢 = 𝑦 ∧ 𝑢 ∈ 𝑧)) | |
2 | cleljust 2119 | . 2 ⊢ (𝑡 ∈ 𝑡 ↔ ∃𝑣(𝑣 = 𝑡 ∧ 𝑣 ∈ 𝑡)) | |
3 | 1, 2 | df-clel 2816 | 1 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 ∧ wa 399 = wceq 1543 ∃wex 1787 ∈ wcel 2110 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1788 df-clel 2816 |
This theorem is referenced by: elissetv 2818 elisset 2819 eleq1w 2820 eleq2w 2821 eleq1d 2822 eleq2d 2823 eleq2dALT 2824 clelabOLD 2881 clabel 2882 nfeld 2915 risset 3186 isset 3421 elex 3426 elrabi 3596 sbcimdv 3769 sbcg 3774 sbcabel 3790 ssel 3893 sselOLD 3894 noel 4245 noelOLD 4246 disjsn 4627 pwpw0 4726 pwsnOLD 4812 mptpreima 6101 fi1uzind 14063 brfi1indALT 14066 nelbOLD 30536 ballotlem2 32167 lfuhgr3 32794 eldm3 33447 eliminable3a 34784 eliminable3b 34785 eliminable-abelv 34790 eliminable-abelab 34791 bj-denoteslem 34792 bj-issetwt 34796 bj-elsngl 34895 wl-dfclab 35484 |
Copyright terms: Public domain | W3C validator |