Theorem dfclel 2841

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

Syntax hints:   ↔ wb 209   ∧ wa 400   = wceq 1563  ∃wex 1802   ∈ wcel 2145

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-clel 2840

This theorem is referenced by:  elex2  2842  issettru  2843  issetlem  2845  elissetv  2846  eleq1w  2848  eleq2w  2849  eleq1d  2850  eleq2d  2851  eleq2dALT  2852  clabel  2910  nfeld  2938  risset  3240  elrabi  3649  sbcimdv  3815  sbcg  3819  sbcabel  3834  ssel  3933  noel  4293  disjsn  4673  pwpw0  4774  mptpreima  6229  fi1uzind  14534  brfi1indALT  14537  ballotlem2  34796  lfuhgr3  35483  eldm3  36124  mh-infprim3bi  36921  bj-dfsbc  37136  eliminable3a  37360  eliminable3b  37361  eliminable-abelv  37366  eliminable-abelab  37367  bj-denoteslem  37368  bj-issetwt  37372  bj-elsngl  37465  wl-dfcleq  38020  wl-dfclab  38100  chnsubseqword  47452