MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfclel Structured version   Visualization version   GIF version

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.
StepHypRef Expression
1 cleljust 2107 . 2 (𝑦𝑧 ↔ ∃𝑢(𝑢 = 𝑦𝑢𝑧))
2 cleljust 2107 . 2 (𝑡𝑡 ↔ ∃𝑣(𝑣 = 𝑡𝑣𝑡))
31, 2df-clel 2802 1 (𝐴𝐵 ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator