Theorem dfclel 2820

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 2819	1 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1537  ∃wex 1777   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-clel 2819

This theorem is referenced by:  elex2  2821  issettru  2822  issetlem  2824  elissetv  2825  eleq1w  2827  eleq2w  2828  eleq1d  2829  eleq2d  2830  eleq2dALT  2831  clabel  2891  nfeld  2920  risset  3239  elexOLD  3510  elrabi  3703  sbcimdv  3878  sbcg  3883  sbcabel  3900  ssel  4002  noel  4360  noelOLD  4361  disjsn  4736  pwpw0  4838  mptpreima  6269  fi1uzind  14556  brfi1indALT  14559  ballotlem2  34453  lfuhgr3  35087  eldm3  35723  eliminable3a  36829  eliminable3b  36830  eliminable-abelv  36835  eliminable-abelab  36836  bj-denoteslem  36837  bj-issetwt  36841  bj-elsngl  36934  wl-dfclab  37550