Theorem dfclel 2894

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

Syntax hints:   ↔ wb 208   ∧ wa 398   = wceq 1537  ∃wex 1780   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-clel 2893

This theorem is referenced by:  eleq1w  2895  eleq2w  2896  eleq1d  2897  eleq2d  2898  eleq2dALT  2899  clelab  2958  clabel  2959  nfeld  2989  risset  3267  elisset  3505  isset  3506  elex  3512  sbcabel  3861  ssel  3961  noel  4296  disjsn  4647  pwpw0  4746  pwsnOLD  4831  mptpreima  6092  fi1uzind  13856  brfi1indALT  13859  nelbOLD  30232  ballotlem2  31746  lfuhgr3  32366  eldm3  32997  eliminable3a  34186  eliminable3b  34187  bj-denoteslem  34188  bj-issetwt  34192  bj-elissetv  34194  bj-elsngl  34283  wl-dfclab  34843