Theorem dfclel 2810

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2809

This theorem is referenced by:  elex2  2811  issettru  2812  issetlem  2814  elissetv  2815  eleq1w  2817  eleq2w  2818  eleq1d  2819  eleq2d  2820  eleq2dALT  2821  clabel  2881  nfeld  2910  risset  3217  elexOLD  3481  elrabi  3666  sbcimdv  3834  sbcg  3838  sbcabel  3853  ssel  3952  noel  4313  disjsn  4687  pwpw0  4789  mptpreima  6227  fi1uzind  14525  brfi1indALT  14528  ballotlem2  34521  lfuhgr3  35142  eldm3  35778  eliminable3a  36881  eliminable3b  36882  eliminable-abelv  36887  eliminable-abelab  36888  bj-denoteslem  36889  bj-issetwt  36893  bj-elsngl  36986  wl-dfclab  37614