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

Theorem elab 3382
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 1883 . 2 𝑥𝜓
2 elab.1 . 2 𝐴 ∈ V
3 elab.2 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
41, 2, 3elabf 3381 1 (𝐴 ∈ {𝑥𝜑} ↔ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1523  wcel 2030  {cab 2637  Vcvv 3231
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233
This theorem is referenced by:  ralab  3400  rexab  3402  intab  4539  dfiin2g  4585  dfiunv2  4588  opeliunxp  5204  elabrex  6541  abrexco  6542  uniuni  7013  finds  7134  finds2  7136  funcnvuni  7161  fun11iun  7168  mapval2  7929  sbthlem2  8112  ssenen  8175  dffi2  8370  dffi3  8378  tctr  8654  tcmin  8655  tc2  8656  tz9.13  8692  tcrank  8785  kardex  8795  karden  8796  cardf2  8807  cardiun  8846  alephval3  8971  dfac3  8982  dfac5lem3  8986  dfac5lem4  8987  dfac2  8991  kmlem12  9021  cardcf  9112  cfeq0  9116  cfsuc  9117  cff1  9118  cflim2  9123  cfss  9125  axdc3lem2  9311  axdc3lem3  9312  axdclem  9379  brdom7disj  9391  brdom6disj  9392  tskuni  9643  gruina  9678  nqpr  9874  supadd  11029  supmul  11033  dfnn2  11071  dfuzi  11506  seqof  12898  hashfacen  13276  hashf1lem1  13277  hashf1lem2  13278  0csh0  13585  trclun  13799  dfrtrcl2  13846  shftfval  13854  infcvgaux1i  14633  symg1bas  17862  pmtrprfvalrn  17954  psgnvali  17974  efgrelexlemb  18209  lss1d  19011  lidldvgen  19303  mpfind  19584  pf1ind  19767  zndvds  19946  cmpsublem  21250  cmpsub  21251  ptpjopn  21463  ptclsg  21466  txdis1cn  21486  tx1stc  21501  hauspwpwf1  21838  qustgplem  21971  ustn0  22071  i1fadd  23507  i1fmul  23508  i1fmulc  23515  ausgrusgri  26108  ushgredgedg  26166  ushgredgedgloop  26168  wspniunwspnon  26888  rusgrnumwwlkb0  26938  fusgr2wsp2nb  27314  nmosetn0  27748  nmoolb  27754  nmlno0lem  27776  nmopsetn0  28852  nmfnsetn0  28865  nmoplb  28894  nmfnlb  28911  nmlnop0iALT  28982  nmopun  29001  nmcexi  29013  branmfn  29092  pjnmopi  29135  fpwrelmapffslem  29635  ldlfcntref  30049  esumc  30241  orvcval2  30648  derangenlem  31279  mclsssvlem  31585  mclsind  31593  dfon2lem3  31814  dfon2lem7  31818  nosupno  31974  nosupbnd1lem1  31979  fnimage  32161  imageval  32162  poimirlem4  33543  poimirlem5  33544  poimirlem6  33545  poimirlem7  33546  poimirlem8  33547  poimirlem9  33548  poimirlem10  33549  poimirlem11  33550  poimirlem12  33551  poimirlem13  33552  poimirlem14  33553  poimirlem15  33554  poimirlem16  33555  poimirlem17  33556  poimirlem18  33557  poimirlem19  33558  poimirlem20  33559  poimirlem21  33560  poimirlem22  33561  poimirlem25  33564  poimirlem26  33565  poimirlem27  33566  poimirlem29  33568  poimirlem31  33570  mblfinlem3  33578  mblfinlem4  33579  ismblfin  33580  itg2addnc  33594  sdclem2  33668  sdclem1  33669  heibor1lem  33738  glbconxN  34982  pmapglbx  35373  dvhb1dimN  36591  eldiophss  37655  setindtrs  37909  hbtlem2  38011  hbtlem5  38015  rngunsnply  38060  dftrcl3  38329  brtrclfv2  38336  dfrtrcl3  38342  dfhe3  38386  nzss  38833  upbdrech  39833  fourierdlem36  40678  sge0resplit  40941  hoidmvlelem1  41130  elsprel  42050  opeliun2xp  42436  setrec2lem1  42765
  Copyright terms: Public domain W3C validator