Theorem dfclel 2838

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 2837	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 2837

This theorem is used by:  elex2  2839  issettru  2840  issetlem  2842  elissetv  2843  eleq1w  2845  eleq2w  2846  eleq1d  2847  eleq2d  2848  eleq2dALT  2849  clabel  2907  nfeld  2935  risset  3239  elrabi  3644  sbcimdv  3810  sbcg  3814  sbcabel  3828  ssel  3928  noel  4287  disjsn  4675  pwpw0  4777  mptpreima  6238  fi1uzind  14576  brfi1indALT  14579  lfuhgr3  29615  ballotlem2  35008  eldm3  36348  mh-infprim3bi  37175  bj-dfsbc  37390  eliminable3a  37614  eliminable3b  37615  eliminable-abelv  37620  eliminable-abelab  37621  bj-denoteslem  37622  bj-issetwt  37626  bj-elsngl  37720  wl-dfcleq  38276  wl-dfclab  38356