Theorem dfclel 2839

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 2152	. 2 ⊢ (𝑦 ∈ 𝑧 ↔ ∃𝑢(𝑢 = 𝑦 ∧ 𝑢 ∈ 𝑧))
2		cleljust 2152	. 2 ⊢ (𝑡 ∈ 𝑡 ↔ ∃𝑣(𝑣 = 𝑡 ∧ 𝑣 ∈ 𝑡))
3	1, 2	df-clel 2838	1 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))

Syntax hints:   ↔ wb 209   ∧ wa 400   = wceq 1570  ∃wex 1809   ∈ wcel 2143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-clel 2838

This theorem is referenced by:  elex2  2840  issettru  2841  issetlem  2843  elissetv  2844  eleq1w  2846  eleq2w  2847  eleq1d  2848  eleq2d  2849  eleq2dALT  2850  clabel  2908  nfeld  2936  risset  3240  elrabi  3647  sbcimdv  3813  sbcg  3817  sbcabel  3832  ssel  3932  noel  4292  disjsn  4678  pwpw0  4780  mptpreima  6241  fi1uzind  14546  brfi1indALT  14549  ballotlem2  34857  lfuhgr3  35590  eldm3  36231  mh-infprim3bi  37037  bj-dfsbc  37252  eliminable3a  37476  eliminable3b  37477  eliminable-abelv  37482  eliminable-abelab  37483  bj-denoteslem  37484  bj-issetwt  37488  bj-elsngl  37582  wl-dfcleq  38138  wl-dfclab  38218  chnsubseqword  47574