Theorem dfclel 2819

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

Syntax hints:   ↔ wb 205   ∧ wa 396   = wceq 1542  ∃wex 1786   ∈ wcel 2110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1787  df-clel 2818

This theorem is referenced by:  elex2  2820  elissetv  2821  elisset  2822  eleq1w  2823  eleq2w  2824  eleq1d  2825  eleq2d  2826  eleq2dALT  2827  clelabOLD  2886  clabel  2887  nfeld  2920  risset  3196  isset  3444  elex  3449  elrabi  3620  sbcimdv  3795  sbcg  3800  sbcabel  3816  ssel  3919  sselOLD  3920  noel  4270  noelOLD  4271  disjsn  4653  pwpw0  4752  pwsnOLD  4838  mptpreima  6139  fi1uzind  14207  brfi1indALT  14210  nelbOLDOLD  30811  ballotlem2  32449  lfuhgr3  33075  eldm3  33722  eliminable3a  35041  eliminable3b  35042  eliminable-abelv  35047  eliminable-abelab  35048  bj-denoteslem  35049  bj-issetwt  35053  bj-elsngl  35152  wl-dfclab  35741