Theorem dfclel 2864

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

Syntax hints:   ↔ wb 207   ∧ wa 396   = wceq 1522  ∃wex 1761   ∈ wcel 2081

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1762  df-clel 2863

This theorem is referenced by:  eleq1w  2865  eleq2w  2866  eleq1d  2867  eleq2d  2868  eleq2dALT  2869  clelab  2930  clabel  2931  nfeld  2958  risset  3231  elisset  3448  isset  3449  elex  3455  sbcabel  3789  ssel  3883  noel  4216  disjsn  4554  pwpw0  4653  pwsnALT  4738  mptpreima  5967  fi1uzind  13701  brfi1indALT  13704  nelb  29924  ballotlem2  31363  lfuhgr3  31978  eldm3  32605  bj-clabel  33699  eliminable3a  33756  eliminable3b  33757  bj-denotes  33759  bj-issetwt  33761  bj-elissetv  33763  bj-elsngl  33885  wl-dfclab  34359