Theorem dfclel 2809

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1541  ∃wex 1780   ∈ wcel 2113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2808

This theorem is referenced by:  elex2  2810  issettru  2811  issetlem  2813  elissetv  2814  eleq1w  2816  eleq2w  2817  eleq1d  2818  eleq2d  2819  eleq2dALT  2820  clabel  2878  nfeld  2907  risset  3208  elexOLD  3459  elrabi  3639  sbcimdv  3806  sbcg  3810  sbcabel  3825  ssel  3924  noel  4287  disjsn  4663  pwpw0  4764  mptpreima  6190  fi1uzind  14416  brfi1indALT  14419  ballotlem2  34523  lfuhgr3  35185  eldm3  35826  eliminable3a  36928  eliminable3b  36929  eliminable-abelv  36934  eliminable-abelab  36935  bj-denoteslem  36936  bj-issetwt  36940  bj-elsngl  37033  wl-dfclab  37650  chnsubseqword  47000