Theorem dfclel 2818

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

Syntax hints:   ↔ wb 205   ∧ wa 395   = wceq 1539  ∃wex 1783   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-clel 2817

This theorem is referenced by:  elissetv  2819  elisset  2820  eleq1w  2821  eleq2w  2822  eleq1d  2823  eleq2d  2824  eleq2dALT  2825  clelabOLD  2883  clabel  2884  nfeld  2917  risset  3193  isset  3435  elex  3440  elrabi  3611  sbcimdv  3786  sbcg  3791  sbcabel  3807  ssel  3910  sselOLD  3911  noel  4261  noelOLD  4262  disjsn  4644  pwpw0  4743  pwsnOLD  4829  mptpreima  6130  fi1uzind  14139  brfi1indALT  14142  nelbOLDOLD  30718  ballotlem2  32355  lfuhgr3  32981  eldm3  33634  eliminable3a  34974  eliminable3b  34975  eliminable-abelv  34980  eliminable-abelab  34981  bj-denoteslem  34982  bj-issetwt  34986  bj-elsngl  35085  wl-dfclab  35674