Theorem dfclel 2813

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 2812	1 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-clel 2812

This theorem is referenced by:  elex2  2814  issettru  2815  issetlem  2817  elissetv  2818  eleq1w  2820  eleq2w  2821  eleq1d  2822  eleq2d  2823  eleq2dALT  2824  clabel  2882  nfeld  2911  risset  3213  elexOLD  3452  elrabi  3631  sbcimdv  3798  sbcg  3802  sbcabel  3817  ssel  3916  noel  4279  disjsn  4656  pwpw0  4757  mptpreima  6196  fi1uzind  14460  brfi1indALT  14463  ballotlem2  34649  lfuhgr3  35318  eldm3  35959  mh-infprim3bi  36746  bj-dfsbc  36962  eliminable3a  37186  eliminable3b  37187  eliminable-abelv  37192  eliminable-abelab  37193  bj-denoteslem  37194  bj-issetwt  37198  bj-elsngl  37291  wl-dfcleq  37844  wl-dfclab  37924  chnsubseqword  47324