Theorem dfclel 2804

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

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

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 2008  ax-8 2111

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

This theorem is referenced by:  elex2  2805  issettru  2806  issetlem  2808  elissetv  2809  eleq1w  2811  eleq2w  2812  eleq1d  2813  eleq2d  2814  eleq2dALT  2815  clabel  2874  nfeld  2903  risset  3204  elexOLD  3460  elrabi  3645  sbcimdv  3813  sbcg  3817  sbcabel  3832  ssel  3931  noel  4291  disjsn  4665  pwpw0  4767  mptpreima  6191  fi1uzind  14432  brfi1indALT  14435  ballotlem2  34456  lfuhgr3  35092  eldm3  35733  eliminable3a  36836  eliminable3b  36837  eliminable-abelv  36842  eliminable-abelab  36843  bj-denoteslem  36844  bj-issetwt  36848  bj-elsngl  36941  wl-dfclab  37569