![]() |
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 2090 | . 2 ⊢ (𝑦 ∈ 𝑧 ↔ ∃𝑢(𝑢 = 𝑦 ∧ 𝑢 ∈ 𝑧)) | |
2 | cleljust 2090 | . 2 ⊢ (𝑡 ∈ 𝑡 ↔ ∃𝑣(𝑣 = 𝑡 ∧ 𝑣 ∈ 𝑡)) | |
3 | 1, 2 | df-clel 2863 | 1 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 ∧ wa 396 = wceq 1522 ∃wex 1761 ∈ wcel 2081 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1762 df-clel 2863 |
This theorem is referenced by: eleq1w 2865 eleq2w 2866 eleq1d 2867 eleq2d 2868 eleq2dALT 2869 clelab 2930 clabel 2931 nfeld 2958 risset 3231 elisset 3448 isset 3449 elex 3455 sbcabel 3789 ssel 3883 noel 4216 disjsn 4554 pwpw0 4653 pwsnALT 4738 mptpreima 5967 fi1uzind 13701 brfi1indALT 13704 nelb 29924 ballotlem2 31363 lfuhgr3 31978 eldm3 32605 bj-clabel 33699 eliminable3a 33756 eliminable3b 33757 bj-denotes 33759 bj-issetwt 33761 bj-elissetv 33763 bj-elsngl 33885 wl-dfclab 34359 |
Copyright terms: Public domain | W3C validator |