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

Theorem elab 3490
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 1992 . 2 𝑥𝜓
2 elab.1 . 2 𝐴 ∈ V
3 elab.2 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
41, 2, 3elabf 3489 1 (𝐴 ∈ {𝑥𝜑} ↔ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1632  wcel 2139  {cab 2746  Vcvv 3340
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342
This theorem is referenced by:  ralab  3508  rexab  3510  intab  4659  dfiin2g  4705  dfiunv2  4708  opeliunxp  5327  elabrex  6665  abrexco  6666  uniuni  7137  finds  7258  finds2  7260  funcnvuni  7285  fun11iun  7292  mapval2  8055  sbthlem2  8238  ssenen  8301  dffi2  8496  dffi3  8504  tctr  8791  tcmin  8792  tc2  8793  tz9.13  8829  tcrank  8922  kardex  8932  karden  8933  cardf2  8979  cardiun  9018  alephval3  9143  dfac3  9154  dfac5lem3  9158  dfac5lem4  9159  dfac2b  9163  dfac2OLD  9165  kmlem12  9195  cardcf  9286  cfeq0  9290  cfsuc  9291  cff1  9292  cflim2  9297  cfss  9299  axdc3lem2  9485  axdc3lem3  9486  axdclem  9553  brdom7disj  9565  brdom6disj  9566  tskuni  9817  gruina  9852  nqpr  10048  supadd  11203  supmul  11207  dfnn2  11245  dfuzi  11680  seqof  13072  hashfacen  13450  hashf1lem1  13451  hashf1lem2  13452  0csh0  13759  trclun  13974  dfrtrcl2  14021  shftfval  14029  infcvgaux1i  14808  symg1bas  18036  pmtrprfvalrn  18128  psgnvali  18148  efgrelexlemb  18383  lss1d  19185  lidldvgen  19477  mpfind  19758  pf1ind  19941  zndvds  20120  cmpsublem  21424  cmpsub  21425  ptpjopn  21637  ptclsg  21640  txdis1cn  21660  tx1stc  21675  hauspwpwf1  22012  qustgplem  22145  ustn0  22245  i1fadd  23681  i1fmul  23682  i1fmulc  23689  ausgrusgri  26283  ushgredgedg  26341  ushgredgedgloop  26343  wspniunwspnon  27064  rusgrnumwwlkb0  27114  fusgr2wsp2nb  27509  nmosetn0  27950  nmoolb  27956  nmlno0lem  27978  nmopsetn0  29054  nmfnsetn0  29067  nmoplb  29096  nmfnlb  29113  nmlnop0iALT  29184  nmopun  29203  nmcexi  29215  branmfn  29294  pjnmopi  29337  fpwrelmapffslem  29837  ldlfcntref  30251  esumc  30443  orvcval2  30850  derangenlem  31481  mclsssvlem  31787  mclsind  31795  dfon2lem3  32016  dfon2lem7  32020  nosupno  32176  nosupbnd1lem1  32181  fnimage  32363  imageval  32364  poimirlem4  33744  poimirlem5  33745  poimirlem6  33746  poimirlem7  33747  poimirlem8  33748  poimirlem9  33749  poimirlem10  33750  poimirlem11  33751  poimirlem12  33752  poimirlem13  33753  poimirlem14  33754  poimirlem15  33755  poimirlem16  33756  poimirlem17  33757  poimirlem18  33758  poimirlem19  33759  poimirlem20  33760  poimirlem21  33761  poimirlem22  33762  poimirlem25  33765  poimirlem26  33766  poimirlem27  33767  poimirlem29  33769  poimirlem31  33771  mblfinlem3  33779  mblfinlem4  33780  ismblfin  33781  itg2addnc  33795  sdclem2  33869  sdclem1  33870  heibor1lem  33939  glbconxN  35185  pmapglbx  35576  dvhb1dimN  36794  eldiophss  37858  setindtrs  38112  hbtlem2  38214  hbtlem5  38218  rngunsnply  38263  dftrcl3  38532  brtrclfv2  38539  dfrtrcl3  38545  dfhe3  38589  nzss  39036  upbdrech  40036  fourierdlem36  40881  sge0resplit  41144  hoidmvlelem1  41333  elsprel  42253  opeliun2xp  42639  setrec2lem1  42968
  Copyright terms: Public domain W3C validator