Theorem dfclel 2811

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

Syntax hints:   ↔ wb 205   ∧ wa 396   = wceq 1541  ∃wex 1781   ∈ wcel 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-clel 2810

This theorem is referenced by:  elex2  2812  issetlem  2813  elissetv  2814  eleq1w  2816  eleq2w  2817  eleq1d  2818  eleq2d  2819  eleq2dALT  2820  clelabOLD  2880  clabel  2881  nfeld  2914  risset  3230  elex  3492  elrabi  3676  sbcimdv  3850  sbcg  3855  sbcabel  3871  ssel  3974  sselOLD  3975  noel  4329  noelOLD  4330  disjsn  4714  pwpw0  4815  pwsnOLD  4900  mptpreima  6234  fi1uzind  14454  brfi1indALT  14457  ballotlem2  33475  lfuhgr3  34098  eldm3  34719  eliminable3a  35730  eliminable3b  35731  eliminable-abelv  35736  eliminable-abelab  35737  bj-denoteslem  35738  bj-issetwt  35742  bj-elsngl  35837  wl-dfclab  36446