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 2123	. 2 ⊢ (𝑦 ∈ 𝑧 ↔ ∃𝑢(𝑢 = 𝑦 ∧ 𝑢 ∈ 𝑧))
2		cleljust 2123	. 2 ⊢ (𝑡 ∈ 𝑡 ↔ ∃𝑣(𝑣 = 𝑡 ∧ 𝑣 ∈ 𝑡))
3	1, 2	df-clel 2811	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 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  3212  elexOLD  3451  elrabi  3630  sbcimdv  3797  sbcg  3801  sbcabel  3816  ssel  3915  noel  4278  disjsn  4655  pwpw0  4756  mptpreima  6202  fi1uzind  14469  brfi1indALT  14472  ballotlem2  34633  lfuhgr3  35302  eldm3  35943  mh-infprim3bi  36730  bj-dfsbc  36946  eliminable3a  37170  eliminable3b  37171  eliminable-abelv  37176  eliminable-abelab  37177  bj-denoteslem  37178  bj-issetwt  37182  bj-elsngl  37275  wl-dfcleq  37830  wl-dfclab  37910  chnsubseqword  47308