Theorem dfclel 2812

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1541  ∃wex 1780   ∈ wcel 2113

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 1968  ax-7 2009  ax-8 2115

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2811

This theorem is referenced by:  elex2  2813  issettru  2814  issetlem  2816  elissetv  2817  eleq1w  2819  eleq2w  2820  eleq1d  2821  eleq2d  2822  eleq2dALT  2823  clabel  2881  nfeld  2910  risset  3211  elexOLD  3462  elrabi  3642  sbcimdv  3809  sbcg  3813  sbcabel  3828  ssel  3927  noel  4290  disjsn  4668  pwpw0  4769  mptpreima  6196  fi1uzind  14430  brfi1indALT  14433  ballotlem2  34646  lfuhgr3  35314  eldm3  35955  eliminable3a  37064  eliminable3b  37065  eliminable-abelv  37070  eliminable-abelab  37071  bj-denoteslem  37072  bj-issetwt  37076  bj-elsngl  37169  wl-dfclab  37786  chnsubseqword  47118