Theorem dfclel 2840

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149

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

This theorem is used by:  elex2  2841  issettru  2842  issetlem  2844  elissetv  2845  eleq1w  2847  eleq2w  2848  eleq1d  2849  eleq2d  2850  eleq2dALT  2851  clabel  2909  nfeld  2937  risset  3241  elrabi  3644  sbcimdv  3810  sbcg  3814  sbcabel  3829  ssel  3907  noelOLD  4287  disjsn  4672  pwpw0  4834  mptpreima  6253  fi1uzind  14682  brfi1indALT  14685  lfuhgr3  29761  ballotlem2  35204  eldm3  36717  mh-infprim3bi  37527  bj-dfsbc  37742  eliminable3a  37966  eliminable3b  37967  eliminable-abelv  37972  eliminable-abelab  37973  bj-denoteslem  37974  bj-issetwt  37978  bj-elsngl  38072  wl-dfcleq  38642  wl-dfclab  38722