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 2123 | . 2 ⊢ (𝑦 ∈ 𝑧 ↔ ∃𝑢(𝑢 = 𝑦 ∧ 𝑢 ∈ 𝑧)) | |
2 | cleljust 2123 | . 2 ⊢ (𝑡 ∈ 𝑡 ↔ ∃𝑣(𝑣 = 𝑡 ∧ 𝑣 ∈ 𝑡)) | |
3 | 1, 2 | df-clel 2893 | 1 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 208 ∧ wa 398 = wceq 1537 ∃wex 1780 ∈ wcel 2114 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1781 df-clel 2893 |
This theorem is referenced by: eleq1w 2895 eleq2w 2896 eleq1d 2897 eleq2d 2898 eleq2dALT 2899 clelab 2958 clabel 2959 nfeld 2989 risset 3267 elisset 3505 isset 3506 elex 3512 sbcabel 3861 ssel 3961 noel 4296 disjsn 4647 pwpw0 4746 pwsnOLD 4831 mptpreima 6092 fi1uzind 13856 brfi1indALT 13859 nelbOLD 30232 ballotlem2 31746 lfuhgr3 32366 eldm3 32997 eliminable3a 34186 eliminable3b 34187 bj-denoteslem 34188 bj-issetwt 34192 bj-elissetv 34194 bj-elsngl 34283 wl-dfclab 34843 |
Copyright terms: Public domain | W3C validator |