Theorem dfclel 2837

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2145

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2836

This theorem is used by:  elex2  2838  issettru  2839  issetlem  2841  elissetv  2842  eleq1w  2844  eleq2w  2845  eleq1d  2846  eleq2d  2847  eleq2dALT  2848  clabel  2906  nfeld  2934  risset  3238  elrabi  3641  sbcimdv  3807  sbcg  3811  sbcabel  3825  ssel  3925  noel  4284  disjsn  4672  pwpw0  4774  mptpreima  6232  fi1uzind  14632  brfi1indALT  14635  lfuhgr3  29710  ballotlem2  35104  eldm3  36495  mh-infprim3bi  37306  bj-dfsbc  37521  eliminable3a  37745  eliminable3b  37746  eliminable-abelv  37751  eliminable-abelab  37752  bj-denoteslem  37753  bj-issetwt  37757  bj-elsngl  37851  wl-dfcleq  38405  wl-dfclab  38485