Theorem dfclel 2837

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

Syntax hints:   ↔ wb 208   ∧ wa 399   = wceq 1559  ∃wex 1798   ∈ wcel 2141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-clel 2836

This theorem is referenced by:  elex2  2838  issettru  2839  issetlem  2841  elissetv  2842  eleq1w  2844  eleq2w  2845  eleq1d  2846  eleq2d  2847  eleq2dALT  2848  clabel  2906  nfeld  2934  risset  3236  elrabi  3646  sbcimdv  3812  sbcg  3816  sbcabel  3831  ssel  3930  noel  4290  disjsn  4669  pwpw0  4770  mptpreima  6221  fi1uzind  14517  brfi1indALT  14520  ballotlem2  34747  lfuhgr3  35434  eldm3  36075  mh-infprim3bi  36872  bj-dfsbc  37088  eliminable3a  37312  eliminable3b  37313  eliminable-abelv  37318  eliminable-abelab  37319  bj-denoteslem  37320  bj-issetwt  37324  bj-elsngl  37417  wl-dfcleq  37972  wl-dfclab  38052  chnsubseqword  47418