Theorem dfclel 2842

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2146

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2841

This theorem is used by:  elex2  2843  issettru  2844  issetlem  2846  elissetv  2847  eleq1w  2849  eleq2w  2850  eleq1d  2851  eleq2d  2852  eleq2dALT  2853  clabel  2911  nfeld  2939  risset  3243  elrabi  3649  sbcimdv  3815  sbcg  3819  sbcabel  3834  ssel  3934  noel  4294  disjsn  4682  pwpw0  4784  mptpreima  6244  fi1uzind  14564  brfi1indALT  14567  ballotlem2  34911  lfuhgr3  35633  eldm3  36274  mh-infprim3bi  37100  bj-dfsbc  37315  eliminable3a  37539  eliminable3b  37540  eliminable-abelv  37545  eliminable-abelab  37546  bj-denoteslem  37547  bj-issetwt  37551  bj-elsngl  37645  wl-dfcleq  38201  wl-dfclab  38281  chnsubseqword  47635