Theorem dfclel 2836

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1569  ∃wex 1811   ∈ wcel 2144

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-clel 2835

This theorem is used by:  elex2  2837  issettru  2838  issetlem  2840  elissetv  2841  eleq1w  2843  eleq2w  2844  eleq1d  2845  eleq2d  2846  eleq2dALT  2847  clabel  2905  nfeld  2933  risset  3237  elrabi  3640  sbcimdv  3806  sbcg  3810  sbcabel  3824  ssel  3902  noel  4283  disjsn  4668  pwpw0  4830  mptpreima  6239  fi1uzind  14655  brfi1indALT  14658  lfuhgr3  29733  ballotlem2  35167  eldm3  36618  mh-infprim3bi  37428  bj-dfsbc  37643  eliminable3a  37867  eliminable3b  37868  eliminable-abelv  37873  eliminable-abelab  37874  bj-denoteslem  37875  bj-issetwt  37879  bj-elsngl  37973  wl-dfcleq  38530  wl-dfclab  38610