Theorem dfclel 2817

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

Syntax hints:   ↔ wb 209   ∧ wa 399   = wceq 1543  ∃wex 1787   ∈ wcel 2110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-clel 2816

This theorem is referenced by:  elissetv  2818  elisset  2819  eleq1w  2820  eleq2w  2821  eleq1d  2822  eleq2d  2823  eleq2dALT  2824  clelabOLD  2881  clabel  2882  nfeld  2915  risset  3186  isset  3421  elex  3426  elrabi  3596  sbcimdv  3769  sbcg  3774  sbcabel  3790  ssel  3893  sselOLD  3894  noel  4245  noelOLD  4246  disjsn  4627  pwpw0  4726  pwsnOLD  4812  mptpreima  6101  fi1uzind  14063  brfi1indALT  14066  nelbOLD  30536  ballotlem2  32167  lfuhgr3  32794  eldm3  33447  eliminable3a  34784  eliminable3b  34785  eliminable-abelv  34790  eliminable-abelab  34791  bj-denoteslem  34792  bj-issetwt  34796  bj-elsngl  34895  wl-dfclab  35484