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

Theorem dfclel 2864
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 2090 . 2 (𝑦𝑧 ↔ ∃𝑢(𝑢 = 𝑦𝑢𝑧))
2 cleljust 2090 . 2 (𝑡𝑡 ↔ ∃𝑣(𝑣 = 𝑡𝑣𝑡))
31, 2df-clel 2863 1 (𝐴𝐵 ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 207  wa 396   = wceq 1522  wex 1761  wcel 2081
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1762  df-clel 2863
This theorem is referenced by:  eleq1w  2865  eleq2w  2866  eleq1d  2867  eleq2d  2868  eleq2dALT  2869  clelab  2930  clabel  2931  nfeld  2958  risset  3231  elisset  3448  isset  3449  elex  3455  sbcabel  3789  ssel  3883  noel  4216  disjsn  4554  pwpw0  4653  pwsnALT  4738  mptpreima  5967  fi1uzind  13701  brfi1indALT  13704  nelb  29924  ballotlem2  31363  lfuhgr3  31978  eldm3  32605  bj-clabel  33699  eliminable3a  33756  eliminable3b  33757  bj-denotes  33759  bj-issetwt  33761  bj-elissetv  33763  bj-elsngl  33885  wl-dfclab  34359
  Copyright terms: Public domain W3C validator