Theorem dfclel 2803

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

Syntax hints:   ↔ wb 205   ∧ wa 394   = wceq 1533  ∃wex 1773   ∈ wcel 2098

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-clel 2802

This theorem is referenced by:  elex2  2804  issetlem  2805  elissetv  2806  eleq1w  2808  eleq2w  2809  eleq1d  2810  eleq2d  2811  eleq2dALT  2812  clelabOLD  2872  clabel  2873  nfeld  2903  risset  3220  elexOLD  3481  elrabi  3673  sbcimdv  3847  sbcg  3852  sbcabel  3868  ssel  3970  noel  4330  noelOLD  4331  disjsn  4717  pwpw0  4818  mptpreima  6244  fi1uzind  14494  brfi1indALT  14497  ballotlem2  34239  lfuhgr3  34860  eldm3  35486  eliminable3a  36471  eliminable3b  36472  eliminable-abelv  36477  eliminable-abelab  36478  bj-denoteslem  36479  bj-issetwt  36483  bj-elsngl  36578  wl-dfclab  37194