Theorem dfclel 2832

Description: Characterization of the elements of a class. (Contributed by BJ, 27-Jun-2019.)

Assertion

Ref	Expression
dfclel	⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem dfclel

Dummy variables 𝑦 𝑧 𝑡 𝑢 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cleljust 2145	. 2 ⊢ (𝑦 ∈ 𝑧 ↔ ∃𝑢(𝑢 = 𝑦 ∧ 𝑢 ∈ 𝑧))
2		cleljust 2145	. 2 ⊢ (𝑡 ∈ 𝑡 ↔ ∃𝑣(𝑣 = 𝑡 ∧ 𝑣 ∈ 𝑡))
3	1, 2	df-clel 2831	1 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))

Syntax hints:   ↔ wb 208   ∧ wa 398   = wceq 1554  ∃wex 1793   ∈ wcel 2136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1794  df-clel 2831

This theorem is referenced by:  elex2  2833  issettru  2834  issetlem  2836  elissetv  2837  eleq1w  2839  eleq2w  2840  eleq1d  2841  eleq2d  2842  eleq2dALT  2843  clabel  2901  nfeld  2929  risset  3231  elrabi  3641  sbcimdv  3807  sbcg  3811  sbcabel  3826  ssel  3925  noel  4285  disjsn  4664  pwpw0  4765  mptpreima  6214  fi1uzind  14510  brfi1indALT  14513  ballotlem2  34740  lfuhgr3  35418  eldm3  36059  mh-infprim3bi  36856  bj-dfsbc  37072  eliminable3a  37296  eliminable3b  37297  eliminable-abelv  37302  eliminable-abelab  37303  bj-denoteslem  37304  bj-issetwt  37308  bj-elsngl  37401  wl-dfcleq  37956  wl-dfclab  38036  chnsubseqword  47402