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

Theorem dfclel 2871
 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 2120 . 2 (𝑦𝑧 ↔ ∃𝑢(𝑢 = 𝑦𝑢𝑧))
2 cleljust 2120 . 2 (𝑡𝑡 ↔ ∃𝑣(𝑣 = 𝑡𝑣𝑡))
31, 2df-clel 2870 1 (𝐴𝐵 ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2111 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-clel 2870 This theorem is referenced by:  eleq1w  2872  eleq2w  2873  eleq1d  2874  eleq2d  2875  eleq2dALT  2876  clelab  2933  clabel  2934  nfeld  2966  risset  3226  elisset  3452  isset  3453  elex  3459  sbcabel  3807  ssel  3908  sselOLD  3909  noel  4247  disjsn  4607  pwpw0  4706  pwsnOLD  4793  mptpreima  6059  fi1uzind  13853  brfi1indALT  13856  nelbOLD  30246  ballotlem2  31868  lfuhgr3  32491  eldm3  33122  eliminable3a  34317  eliminable3b  34318  eliminable-abelv  34323  eliminable-abelab  34324  bj-denoteslem  34325  bj-issetwt  34329  bj-elissetv  34331  bj-elsngl  34420  wl-dfclab  35009
 Copyright terms: Public domain W3C validator