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

Theorem elab 3319
Description: Membership in a class abstraction, using implicit substitution. Compare Theorem 6.13 of [Quine] p. 44. (Contributed by NM, 1-Aug-1994.)
Hypotheses
Ref Expression
elab.1 𝐴 ∈ V
elab.2 (𝑥 = 𝐴 → (𝜑𝜓))
Assertion
Ref Expression
elab (𝐴 ∈ {𝑥𝜑} ↔ 𝜓)
Distinct variable groups:   𝜓,𝑥   𝑥,𝐴
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem elab
StepHypRef Expression
1 nfv 1830 . 2 𝑥𝜓
2 elab.1 . 2 𝐴 ∈ V
3 elab.2 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
41, 2, 3elabf 3318 1 (𝐴 ∈ {𝑥𝜑} ↔ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195   = wceq 1475  wcel 1977  {cab 2596  Vcvv 3173
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175
This theorem is referenced by:  ralab  3334  rexab  3336  intab  4442  dfiin2g  4489  dfiunv2  4492  opeliunxp  5093  elabrex  6405  abrexco  6406  uniuni  6865  finds  6984  finds2  6986  funcnvuni  7012  fun11iun  7019  mapval2  7773  sbthlem2  7956  ssenen  8019  dffi2  8212  dffi3  8220  tctr  8499  tcmin  8500  tc2  8501  tz9.13  8537  tcrank  8630  kardex  8640  karden  8641  cardf2  8652  cardiun  8691  alephval3  8816  dfac3  8827  dfac5lem3  8831  dfac5lem4  8832  dfac2  8836  kmlem12  8866  cardcf  8957  cfeq0  8961  cfsuc  8962  cff1  8963  cflim2  8968  cfss  8970  axdc3lem2  9156  axdc3lem3  9157  axdclem  9224  brdom7disj  9234  brdom6disj  9235  tskuni  9484  gruina  9519  nqpr  9715  supadd  10868  supmul  10872  dfnn2  10910  dfuzi  11344  seqof  12720  hashfacen  13095  hashf1lem1  13096  hashf1lem2  13097  0csh0  13390  trclun  13603  dfrtrcl2  13650  shftfval  13658  infcvgaux1i  14428  symg1bas  17639  pmtrprfvalrn  17731  psgnvali  17751  efgrelexlemb  17986  lss1d  18784  lidldvgen  19076  mpfind  19357  pf1ind  19540  zndvds  19717  cmpsublem  21012  cmpsub  21013  ptpjopn  21225  ptclsg  21228  txdis1cn  21248  tx1stc  21263  hauspwpwf1  21601  qustgplem  21734  ustn0  21834  i1fadd  23268  i1fmul  23269  i1fmulc  23276  2wot2wont  26413  2spot2iun2spont  26418  rusgranumwlkb0  26480  usg2spot2nb  26592  nmosetn0  27004  nmoolb  27010  nmlno0lem  27032  nmopsetn0  28108  nmfnsetn0  28121  nmoplb  28150  nmfnlb  28167  nmlnop0iALT  28238  nmopun  28257  nmcexi  28269  branmfn  28348  pjnmopi  28391  fpwrelmapffslem  28895  ldlfcntref  29249  esumc  29440  orvcval2  29847  derangenlem  30407  mclsssvlem  30713  mclsind  30721  dfon2lem3  30934  dfon2lem7  30938  fnimage  31206  imageval  31207  poimirlem4  32583  poimirlem5  32584  poimirlem6  32585  poimirlem7  32586  poimirlem8  32587  poimirlem9  32588  poimirlem10  32589  poimirlem11  32590  poimirlem12  32591  poimirlem13  32592  poimirlem14  32593  poimirlem15  32594  poimirlem16  32595  poimirlem17  32596  poimirlem18  32597  poimirlem19  32598  poimirlem20  32599  poimirlem21  32600  poimirlem22  32601  poimirlem25  32604  poimirlem26  32605  poimirlem27  32606  poimirlem29  32608  poimirlem31  32610  mblfinlem3  32618  mblfinlem4  32619  ismblfin  32620  itg2addnc  32634  sdclem2  32708  sdclem1  32709  heibor1lem  32778  glbconxN  33682  pmapglbx  34073  dvhb1dimN  35292  eldiophss  36356  setindtrs  36610  hbtlem2  36713  hbtlem5  36717  rngunsnply  36762  dftrcl3  37031  brtrclfv2  37038  dfrtrcl3  37044  dfhe3  37089  nzss  37538  upbdrech  38460  fourierdlem36  39036  sge0resplit  39299  hoidmvlelem1  39485  ausgrusgri  40398  ushgredgedga  40456  ushgredgedgaloop  40458  wspniunwspnon  41130  rusgrnumwwlkb0  41174  fusgr2wsp2nb  41498  opeliun2xp  41904  setrec2lem1  42239
  Copyright terms: Public domain W3C validator