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

Syntax hints:   ↔ wb 205   ∧ wa 394   = wceq 1539  ∃wex 1779   ∈ wcel 2104

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 1911  ax-6 1969  ax-7 2009  ax-8 2106

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-clel 2808

This theorem is referenced by:  elex2  2810  issetlem  2811  elissetv  2812  eleq1w  2814  eleq2w  2815  eleq1d  2816  eleq2d  2817  eleq2dALT  2818  clelabOLD  2878  clabel  2879  nfeld  2912  risset  3228  elex  3491  elrabi  3676  sbcimdv  3850  sbcg  3855  sbcabel  3871  ssel  3974  sselOLD  3975  noel  4329  noelOLD  4330  disjsn  4714  pwpw0  4815  pwsnOLD  4900  mptpreima  6236  fi1uzind  14462  brfi1indALT  14465  ballotlem2  33785  lfuhgr3  34408  eldm3  35035  eliminable3a  36045  eliminable3b  36046  eliminable-abelv  36051  eliminable-abelab  36052  bj-denoteslem  36053  bj-issetwt  36057  bj-elsngl  36152  wl-dfclab  36761