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  4437  dfiin2g  4484  dfiunv2  4487  opeliunxp  5083  elabrex  6383  abrexco  6384  uniuni  6843  finds  6962  finds2  6964  funcnvuni  6990  fun11iun  6997  mapval2  7751  sbthlem2  7934  ssenen  7997  dffi2  8190  dffi3  8198  tctr  8477  tcmin  8478  tc2  8479  tz9.13  8515  tcrank  8608  kardex  8618  karden  8619  cardf2  8630  cardiun  8669  alephval3  8794  dfac3  8805  dfac5lem3  8809  dfac5lem4  8810  dfac2  8814  kmlem12  8844  cardcf  8935  cfeq0  8939  cfsuc  8940  cff1  8941  cflim2  8946  cfss  8948  axdc3lem2  9134  axdc3lem3  9135  axdclem  9202  brdom7disj  9212  brdom6disj  9213  tskuni  9462  gruina  9497  nqpr  9693  supadd  10841  supmul  10845  dfnn2  10883  dfuzi  11303  seqof  12678  hashfacen  13050  hashf1lem1  13051  hashf1lem2  13052  0csh0  13339  trclun  13552  dfrtrcl2  13599  shftfval  13607  infcvgaux1i  14377  symg1bas  17588  pmtrprfvalrn  17680  psgnvali  17700  efgrelexlemb  17935  lss1d  18733  lidldvgen  19025  mpfind  19306  pf1ind  19489  zndvds  19665  cmpsublem  20960  cmpsub  20961  ptpjopn  21173  ptclsg  21176  txdis1cn  21196  tx1stc  21211  hauspwpwf1  21549  qustgplem  21682  ustn0  21782  i1fadd  23213  i1fmul  23214  i1fmulc  23221  2wot2wont  26207  2spot2iun2spont  26212  rusgranumwlkb0  26274  usg2spot2nb  26386  nmosetn0  26798  nmoolb  26804  nmlno0lem  26826  nmopsetn0  27902  nmfnsetn0  27915  nmoplb  27944  nmfnlb  27961  nmlnop0iALT  28032  nmopun  28051  nmcexi  28063  branmfn  28142  pjnmopi  28185  fpwrelmapffslem  28689  ldlfcntref  29043  esumc  29234  orvcval2  29641  derangenlem  30201  mclsssvlem  30507  mclsind  30515  dfon2lem3  30728  dfon2lem7  30732  fnimage  31000  imageval  31001  poimirlem4  32377  poimirlem5  32378  poimirlem6  32379  poimirlem7  32380  poimirlem8  32381  poimirlem9  32382  poimirlem10  32383  poimirlem11  32384  poimirlem12  32385  poimirlem13  32386  poimirlem14  32387  poimirlem15  32388  poimirlem16  32389  poimirlem17  32390  poimirlem18  32391  poimirlem19  32392  poimirlem20  32393  poimirlem21  32394  poimirlem22  32395  poimirlem25  32398  poimirlem26  32399  poimirlem27  32400  poimirlem29  32402  poimirlem31  32404  mblfinlem3  32412  mblfinlem4  32413  ismblfin  32414  itg2addnc  32428  sdclem2  32502  sdclem1  32503  heibor1lem  32572  glbconxN  33476  pmapglbx  33867  dvhb1dimN  35086  eldiophss  36150  setindtrs  36404  hbtlem2  36507  hbtlem5  36511  rngunsnply  36556  dftrcl3  36825  brtrclfv2  36832  dfrtrcl3  36838  dfhe3  36883  nzss  37332  upbdrech  38254  fourierdlem36  38830  sge0resplit  39093  hoidmvlelem1  39279  ausgrusgri  40390  ushgredgedga  40448  ushgredgedgaloop  40450  wspniunwspnon  41122  rusgrnumwwlkb0  41166  fusgr2wsp2nb  41490  opeliun2xp  41896
  Copyright terms: Public domain W3C validator