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

Theorem elab 3665
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 1908 . 2 𝑥𝜓
2 elab.1 . 2 𝐴 ∈ V
3 elab.2 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
41, 2, 3elabf 3663 1 (𝐴 ∈ {𝑥𝜑} ↔ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208   = wceq 1530  wcel 2107  {cab 2797  Vcvv 3493
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-v 3495
This theorem is referenced by:  ralab  3682  rexab  3684  intab  4897  dfiin2g  4948  dfiunv2  4951  opeliunxp  5612  dmopab2rex  5779  elabrex  6994  abrexco  6995  uniuni  7476  finds  7600  finds2  7602  funcnvuni  7628  fiunlem  7635  fiun  7636  f1iun  7637  mapval2  8428  sbthlem2  8620  ssenen  8683  dffi2  8879  dffi3  8887  tctr  9174  tcmin  9175  tc2  9176  tz9.13  9212  tcrank  9305  kardex  9315  karden  9316  cardf2  9364  cardiun  9403  alephval3  9528  dfac3  9539  dfac5lem3  9543  dfac5lem4  9544  dfac2b  9548  kmlem12  9579  cardcf  9666  cfeq0  9670  cfsuc  9671  cff1  9672  cflim2  9677  cfss  9679  axdc3lem2  9865  axdc3lem3  9866  axdclem  9933  brdom7disj  9945  brdom6disj  9946  tskuni  10197  gruina  10232  nqpr  10428  supadd  11601  supmul  11605  dfnn2  11643  dfuzi  12065  seqof  13419  hashfacen  13804  hashf1lem1  13805  hashf1lem2  13806  0csh0  14147  trclun  14366  dfrtrcl2  14413  shftfval  14421  infcvgaux1i  15204  sursubmefmnd  18053  injsubmefmnd  18054  smndex2dnrinv  18072  symg1bas  18511  pmtrprfvalrn  18608  psgnvali  18628  efgrelexlemb  18868  lss1d  19727  lidldvgen  20020  mpfind  20312  pf1ind  20510  zndvds  20688  cmpsublem  21999  cmpsub  22000  ptpjopn  22212  ptclsg  22215  txdis1cn  22235  tx1stc  22250  hauspwpwf1  22587  qustgplem  22721  ustn0  22821  i1fadd  24288  i1fmul  24289  i1fmulc  24296  ausgrusgri  26945  ushgredgedg  27003  ushgredgedgloop  27005  wspniunwspnon  27694  rusgrnumwwlkb0  27742  fusgr2wsp2nb  28105  nmosetn0  28534  nmoolb  28540  nmlno0lem  28562  nmopsetn0  29634  nmfnsetn0  29647  nmoplb  29676  nmfnlb  29693  nmlnop0iALT  29764  nmopun  29783  nmcexi  29795  branmfn  29874  pjnmopi  29917  fpwrelmapffslem  30460  ldlfcntref  31106  esumc  31298  orvcval2  31704  derangenlem  32406  satfrnmapom  32605  fmlaomn0  32625  fmlasucdisj  32634  dmopab3rexdif  32640  2goelgoanfmla1  32659  mclsssvlem  32797  mclsind  32805  dfon2lem3  33018  dfon2lem7  33022  nosupno  33191  nosupbnd1lem1  33196  fnimage  33378  imageval  33379  poimirlem4  34883  poimirlem5  34884  poimirlem6  34885  poimirlem7  34886  poimirlem8  34887  poimirlem9  34888  poimirlem10  34889  poimirlem11  34890  poimirlem12  34891  poimirlem13  34892  poimirlem14  34893  poimirlem15  34894  poimirlem16  34895  poimirlem17  34896  poimirlem18  34897  poimirlem19  34898  poimirlem20  34899  poimirlem21  34900  poimirlem22  34901  poimirlem25  34904  poimirlem26  34905  poimirlem27  34906  poimirlem29  34908  poimirlem31  34910  mblfinlem3  34918  mblfinlem4  34919  ismblfin  34920  itg2addnc  34933  sdclem2  35004  sdclem1  35005  heibor1lem  35074  glbconxN  36501  pmapglbx  36892  dvhb1dimN  38109  eldiophss  39356  setindtrs  39607  hbtlem2  39709  hbtlem5  39713  rngunsnply  39758  dftrcl3  40050  brtrclfv2  40057  dfrtrcl3  40063  dfhe3  40106  elscottab  40565  cpcolld  40579  nzss  40634  upbdrech  41556  fourierdlem36  42413  sge0resplit  42673  hoidmvlelem1  42862  elsprel  43622  opeliun2xp  44366  setrec2lem1  44781
  Copyright terms: Public domain W3C validator