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  3464  elrabi  3644  sbcimdv  3811  sbcg  3815  sbcabel  3830  ssel  3929  noel  4292  disjsn  4670  pwpw0  4771  mptpreima  6204  fi1uzind  14442  brfi1indALT  14445  ballotlem2  34666  lfuhgr3  35333  eldm3  35974  eliminable3a  37105  eliminable3b  37106  eliminable-abelv  37111  eliminable-abelab  37112  bj-denoteslem  37113  bj-issetwt  37117  bj-elsngl  37210  wl-dfclab  37834  chnsubseqword  47230