MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rspcev Unicode version

Theorem rspcev 2960
Description: Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998.)
Hypothesis
Ref Expression
rspcv.1  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
rspcev  |-  ( ( A  e.  B  /\  ps )  ->  E. x  e.  B  ph )
Distinct variable groups:    x, A    x, B    ps, x
Allowed substitution hint:    ph( x)

Proof of Theorem rspcev
StepHypRef Expression
1 nfv 1619 . 2  |-  F/ x ps
2 rspcv.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
31, 2rspce 2955 1  |-  ( ( A  e.  B  /\  ps )  ->  E. x  e.  B  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1642    e. wcel 1710   E.wrex 2620
This theorem is referenced by:  rspc2ev  2968  rspc3ev  2970  reu6i  3032  rspesbca  3147  wefrc  4469  wereu2  4472  onfr  4513  ordunidif  4522  onssmin  4670  onminex  4680  onuninsuci  4713  elrnmpt1s  5009  dffv2  5675  foco2  5763  elabrex  5851  f1elima  5874  fcofo  5885  fliftfun  5898  fliftval  5902  f1oiso2  5936  fo1st  6226  fo2nd  6227  sorpssuni  6373  sorpssint  6374  onnseq  6448  tfrlem12  6492  seqomlem2  6550  oawordeulem  6639  oaass  6646  odi  6664  omass  6665  omeulem1  6667  oen0  6671  oeordi  6672  oelim2  6680  oeeulem  6686  nnawordex  6722  nneob  6737  ecelqsg  6801  resixpfo  6942  elixpsn  6943  ixpsnf1o  6944  boxcutc  6947  snfi  7029  onfin  7139  pssnn  7169  ssnnfi  7170  dif1enOLD  7180  dif1en  7181  findcard  7187  frfi  7192  fisupg  7195  nnsdomg  7206  unfi  7214  fofinf1o  7227  pwfilem  7240  fissuni  7250  fipreima  7251  finsschain  7252  indexfi  7253  elfir  7259  fiin  7265  marypha1lem  7276  eqsup  7297  supmaxlem  7305  fisup2g  7307  fisupcl  7308  suppr  7309  supisoex  7312  wofib  7350  wemaplem2  7352  card2inf  7359  brwdom2  7377  cnfcom3clem  7498  trcl  7500  r1ordg  7540  r1pwss  7546  tz9.12lem3  7551  tz9.12  7552  r1elwf  7558  tcrank  7644  scottex  7645  scott0  7646  isnumi  7669  onsdom  7719  fseqdom  7743  ondomen  7754  infpwfien  7779  cardaleph  7806  cardalephex  7807  infenaleph  7808  alephfplem4  7824  alephfp2  7826  dfac2  7847  ackbij1lem18  7953  ackbij1  7954  cflem  7962  cflecard  7969  cfsuc  7973  cfflb  7975  cofsmo  7985  cfsmolem  7986  coftr  7989  fin23lem7  8032  fin23lem11  8033  enfin2i  8037  fin23lem26  8041  fin23lem38  8065  isf32lem5  8073  isf34lem4  8093  isfin1-3  8102  fin1a2lem7  8122  fin1a2lem11  8126  fin1a2lem13  8128  axdc3lem2  8167  axdc3lem4  8169  ttukeylem7  8232  iunfo  8251  ficard  8277  pwcfsdom  8295  fpwwe2lem12  8353  wunex  8451  eltsk2g  8463  grur1  8532  axgroth6  8540  inaprc  8548  nqereu  8643  archnq  8694  genpnmax  8721  ltexpri  8757  prlem936  8761  reclem3pr  8763  recexpr  8765  supexpr  8768  negexsr  8814  recexsrlem  8815  recexsr  8819  supsrlem  8823  axrnegex  8874  axrrecex  8875  axpre-sup  8881  1re  8927  cnegex  9083  cnegex2  9084  recex  9490  receu  9503  fimaxre2  9792  lbinfm  9797  infm3lem  9802  supmul1  9809  supmullem2  9811  supmul  9812  infmrcl  9823  cju  9832  nn2ge  9861  nominpos  10040  zdiv  10174  btwnz  10206  uzwo  10373  uzwoOLD  10374  uzinfmi  10389  ublbneg  10394  lbzbi  10398  zsupss  10399  uzsupss  10402  zq  10414  rpnnen1lem1  10434  rpnnen1lem2  10435  rpnnen1lem3  10436  rpnnen1lem4  10437  rpnnen1lem5  10438  z2ge  10617  qbtwnre  10618  qbtwnxr  10619  xralrple  10624  xrsupsslem  10717  xrinfmsslem  10718  supxrpnf  10729  icc0  10796  iccsupr  10828  flval3  11037  uzsup  11059  fsequb  11129  expnbnd  11323  expmulnbnd  11326  hashkf  11432  hashdom  11454  iswrdi  11513  shftlem  11659  shftfval  11661  sqrlem3  11826  01sqrex  11831  resqrex  11832  sqrneg  11849  abs1m  11915  rexanuz  11925  rexanre  11926  rexuz3  11928  rexuzre  11932  rexico  11933  caubnd2  11937  caubnd  11938  sqreu  11940  rlim2lt  12067  rlim3  12068  lo1bdd2  12094  lo1bddrp  12095  o1lo1  12107  climconst  12113  rlimconst  12114  rlimclim1  12115  climshftlem  12144  rlimcn2  12160  reccn2  12166  cn1lem  12167  rlimo1  12186  o1rlimmul  12188  lo1add  12196  lo1mul  12197  lo1le  12221  isercoll  12237  isercoll2  12238  caucvgrlem  12242  serf0  12250  zsum  12288  fsum  12290  fsumcvg3  12299  climcnds  12407  divrcnv  12408  infcvgaux2i  12413  mertenslem1  12437  mertenslem2  12438  ruclem12  12616  dvdsval2  12631  dvds0lem  12636  dvds1lem  12637  dvds2lem  12638  odd2np1lem  12683  odd2np1  12684  divalglem9  12697  gcdcllem3  12789  bezoutlem1  12814  qredeu  12883  exprmfct  12886  isprm5  12888  maxprmfct  12889  odzcllem  12954  opeo  12963  omeo  12964  pythagtriplem19  12983  pcprmpw2  13031  pcprmpw  13032  pockthi  13051  infpnlem2  13055  prmreclem1  13060  prmreclem5  13064  prmreclem6  13065  1arithlem4  13070  vdwapun  13118  vdwlem1  13125  vdwlem2  13126  vdwlem6  13130  vdwlem8  13132  vdwlem10  13134  vdwlem13  13137  ramcl2lem  13153  ramz  13169  ramub1lem1  13170  elrestr  13432  imasleval  13542  mreexexlem3d  13647  mreexexlem4d  13648  iscatd  13674  poslubd  14350  fpwipodrs  14366  spwpr4  14439  ismgmid2  14489  ismndd  14495  gsumvallem1  14547  gsumval2a  14558  gsumwspan  14567  isgrpd2  14604  isgrpd  14606  imasgrp2  14709  gaorber  14861  orbsta  14866  cayleyth  14889  odf1o2  14983  pgpfi1  15005  sylow1lem3  15010  sylow1lem5  15012  pgpfi  15015  pgpssslw  15024  sylow2alem2  15028  slwhash  15034  fislw  15035  lsmelvalm  15061  pj1id  15107  efgs1b  15144  efgrelexlemb  15158  efgredeu  15160  gexex  15244  cyggeninv  15269  0cyg  15278  lt6abl  15280  eldprdi  15352  pgpfac1lem3a  15410  pgpfac1lem3  15411  pgpfac1lem5  15413  pgpfaclem1  15415  pgpfaclem3  15417  ablfaclem2  15420  dvdsrmul  15529  dvdsr01  15536  irredrmul  15588  lss1d  15819  lspf  15830  lspval  15831  lssats2  15856  lspsn  15858  lspsneq  15974  lspfixed  15980  lspsolvlem  15994  lspprat  16005  lbsextlem2  16011  lpi0  16098  lpi1  16099  aspval  16167  zlpir  16550  zcyg  16551  zncyg  16608  znf1o  16611  cygznlem3  16629  cygth  16631  frgpcyg  16633  fiinbas  16796  topbas  16816  pptbas  16851  clsval  16880  clsval2  16893  elcls  16916  neiint  16947  neips  16956  opnneissb  16957  opnssneib  16958  innei  16968  restbas  16995  restcld  17009  restcldi  17010  restopnb  17012  restcls  17017  ordtbas2  17027  ordtopn1  17030  ordtopn2  17031  leordtval2  17048  iocpnfordt  17051  icomnfordt  17052  lecldbas  17055  pnfnei  17056  mnfnei  17057  lmconst  17097  cncnpi  17113  cnconst2  17117  cnprest  17123  cnpdis  17127  pnrmopn  17177  nrmsep  17191  regsep2  17210  cmpcovf  17224  cncmp  17225  fincmp  17226  cmpsublem  17232  cmpsub  17233  tgcmp  17234  cmpcld  17235  uncmp  17236  hauscmplem  17239  cmpfi  17241  consubclo  17256  concompid  17263  2ndci  17280  2ndcsb  17281  2ndc1stc  17283  1stcrest  17285  2ndcctbss  17287  2ndcdisj  17288  2ndcomap  17290  2ndcsep  17291  dis2ndc  17292  restlly  17315  islly2  17316  hausllycmp  17326  cldllycmp  17327  lly1stc  17328  dislly  17329  llycmpkgen2  17351  cmpkgen  17352  1stckgenlem  17354  elptr  17374  ptbasfi  17382  ptpjopn  17412  txcnp  17420  ptcnplem  17421  txlly  17436  txnlly  17437  txtube  17440  txcmplem1  17441  txcmplem2  17442  tx1stc  17450  txkgen  17452  xkococnlem  17459  txcon  17489  tgqtop  17509  qtopeu  17513  kqreglem1  17538  kqreglem2  17539  kqnrmlem1  17540  kqnrmlem2  17541  reghmph  17590  nrmhmph  17591  fbssfi  17634  opnfbas  17639  isfil2  17653  fsubbas  17664  ssfg  17669  fgss2  17671  fbasrn  17681  filuni  17682  fgtr  17687  ssufl  17715  uffix  17718  elfm  17744  elfm2  17745  elfm3  17747  imaelfm  17748  rnelfmlem  17749  rnelfm  17750  fmfnfmlem3  17753  fmfnfmlem4  17754  fmfnfm  17755  fmco  17758  ufldom  17759  hausflim  17778  flimcls  17782  hauspwpwf1  17784  flffbas  17792  txflf  17803  fclscf  17822  fclsfnflim  17824  alexsubALTlem3  17845  alexsubALTlem4  17846  alexsubALT  17847  ptcmplem2  17849  ptcmplem3  17850  ptcmplem5  17852  tmdgsum2  17881  symgtgp  17886  subgntr  17891  opnsubg  17892  ghmcnp  17899  divstgpopn  17904  tsmsfbas  17912  tsmsgsum  17923  tsmsres  17928  tsmsxplem1  17937  tsmsxp  17939  imasdsf1olem  18039  blss  18074  blssex  18075  ssblex  18076  blin2  18077  neibl  18149  blcld  18153  metss2  18160  stdbdmopn  18166  mopnex  18167  met1stc  18169  met2ndci  18170  metrest  18172  prdsxmslem2  18177  metcnp3  18188  metcnpi3  18194  dscopn  18198  ngptgp  18254  nlmvscnlem1  18299  nrginvrcnlem  18303  nghmcn  18356  tgioo  18404  tgqioo  18408  xrsmopn  18420  zcld  18421  recld2  18422  zdis  18424  icccmplem1  18430  icccmplem2  18431  icccmplem3  18432  reconnlem2  18435  xmetdcn2  18445  metdscn  18463  addcnlem  18471  elcncf1di  18502  icoopnst  18541  iocopnst  18542  xrhmeo  18548  cnheibor  18557  cnllycmp  18558  lebnumlem3  18565  lebnum  18566  xlebnum  18567  lebnumii  18568  elpi1i  18648  ipcnlem1  18776  lmnn  18793  iscfil3  18803  cfilres  18826  flimcfil  18843  cncmet  18848  bcthlem4  18853  bcthlem5  18854  minveclem4c  18893  minveclem2  18894  minveclem3b  18896  minveclem3  18897  minveclem4  18900  minveclem6  18902  ivthlem2  18916  ivthlem3  18917  ivth  18918  ivthle  18920  ivthle2  18921  cniccbdd  18925  elovolmr  18939  ovolunlem1  18960  ovoliunlem1  18965  ovoliunlem2  18966  ovoliun2  18969  ovolicc1  18979  iundisj  19009  iunmbl2  19018  ioombl1lem4  19022  uniioombllem2  19042  uniioombllem3  19044  uniioombllem6  19047  dyadmbllem  19058  volcn  19065  volivth  19066  vitalilem2  19068  mbfinf  19124  mbflimsup  19125  i1faddlem  19152  i1fmullem  19153  itg1addlem4  19158  i1fmulc  19162  itg1climres  19173  itg2lr  19189  itg2monolem1  19209  itg2i1fseq  19214  itg2i1fseq2  19215  itg2cnlem1  19220  itg2cnlem2  19221  limcnlp  19332  ellimc3  19333  limcflf  19335  limciun  19348  dveflem  19430  rollelem  19440  c1lip1  19448  lhop1lem  19464  evlseu  19504  ply1divex  19626  ig1peu  19661  ply1lpir  19668  elply2  19682  plyeq0lem  19696  coeeq  19713  plydivlem3  19779  plydivlem4  19780  elqaalem3  19805  qaa  19807  iaa  19809  aareccl  19810  aannenlem2  19813  aalioulem2  19817  aalioulem3  19818  aalioulem5  19820  aalioulem6  19821  aaliou  19822  aaliou2  19824  aaliou3lem8  19829  ulmshftlem  19872  ulmbdd  19881  mtestbdd  19888  iblulm  19890  abelthlem8  19922  reeff1o  19930  pilem2  19935  pilem3  19936  efif1olem2  20012  eflogeq  20063  divlogrlim  20093  efopn  20116  cxpcn3lem  20198  cxpeq  20208  angpieqvd  20239  dcubic2  20251  quart  20268  rlimcnp  20371  xrlimcnp  20374  cxplim  20377  cxploglim  20383  emcllem6  20406  ftalem1  20422  ftalem2  20423  ftalem3  20424  ftalem5  20426  ftalem7  20428  isppw2  20465  sgmnncl  20497  dvdsppwf1o  20538  musum  20543  dvdsmulf1o  20546  perfect  20582  dchrptlem1  20615  dchrptlem2  20616  dchrpt  20618  bpos1lem  20633  lgsqrlem4  20695  lgsdchrval  20698  lgsquadlem1  20705  2sqlem2  20715  mul2sq  20716  2sqlem3  20717  2sqlem9  20724  2sqlem10  20725  2sqblem  20728  dchrisumlem3  20752  dchrisum0  20781  chpdifbndlem2  20815  pntrsumbnd2  20828  pntpbnd1  20847  pntpbnd2  20848  pntpbnd  20849  pntibndlem2  20852  pntibndlem3  20853  pntleme  20869  pntlem3  20870  ostth2  20898  ostth3  20899  lpni  20958  isgrpo  20975  isgrpoi  20977  grpoinvf  21019  isgrpda  21076  isgrpod  21077  isablod  21079  opidon  21101  ghgrp  21147  isrngod  21158  cnrngo  21182  rngmgmbs4  21196  vacn  21381  nmcvcn  21382  smcnlem  21384  nmosetn0  21457  nmoolb  21463  nmobndi  21467  nmoo0  21483  nmlno0lem  21485  isblo3i  21493  blo3i  21494  blocnilem  21496  blocni  21497  ubthlem1  21563  ubthlem2  21564  ubthlem3  21565  minvecolem2  21568  minvecolem3  21569  minvecolem4c  21572  minvecolem4  21573  minvecolem5  21574  minvecolem6  21575  htthlem  21611  norm1exi  21943  occl  21997  shsel3  22008  spanval  22026  spancl  22029  shsval2i  22080  pjhthlem2  22085  ococin  22101  h1de2ctlem  22248  spansncol  22261  pjoml6i  22282  nmopsetn0  22559  nmfnsetn0  22572  nmoplb  22601  nmfnlb  22618  0cnop  22673  0cnfn  22674  idcnop  22675  nmop0  22680  nmfn0  22681  nmlnop0iALT  22689  nmopun  22708  nmcexi  22720  lnconi  22727  lnopcnbd  22730  lnfncnbd  22751  riesz3i  22756  riesz1  22759  cnlnadjlem2  22762  cnlnadjlem8  22768  cnlnadjlem9  22769  adjbd1o  22779  branmfn  22799  opsqrlem1  22834  pjnmopi  22842  strlem1  22944  stri  22951  hstri  22959  cvcon3  22978  cvnbtwn  22980  superpos  23048  shatomici  23052  atcvat4i  23091  mdsymlem2  23098  cdj1i  23127  cdj3lem2  23129  cdj3i  23135  rexunirn  23173  iundisjf  23227  elunirn2  23266  inelfi  23318  ssnnssfz  23350  iundisjfi  23356  xreceu  23372  rexdiv  23376  rhmdvdsr  23422  neiptopnei  23445  iscnp4  23447  tpr2rico  23466  rge0scvg  23491  pnfneige0  23492  ustexsym  23521  elrnust  23528  trust  23533  utoptop  23538  restutop  23541  restutopopn  23542  ustuqtop1  23545  ustuqtop2  23546  ustuqtop4  23548  ustuqtop5  23549  utopsnneiplem  23551  iducn  23578  fmucnd  23586  metuval  23593  metustexhalf  23600  metustfbas  23601  cfilucfil  23603  restmetu  23615  qqhcn  23648  indf1ofs  23689  gsumesum  23717  esumpcvgval  23734  dmsigagen  23793  dya2icoseg  23891  dya2iocnrect  23895  dya2iocuni  23897  sxbrsigalem2  23900  dstfrvunirn  23981  ballotlem4  24005  ballotlemrc  24037  lgambdd  24070  subfacp1lem3  24117  erdsze2lem2  24139  cnpcon  24165  txpcon  24167  ptpcon  24168  indispcon  24169  conpcon  24170  cvxpcon  24177  cnllyscon  24180  cvmsss2  24209  cvmcov2  24210  cvmopnlem  24213  cvmfolem  24214  cvmliftlem14  24232  cvmliftlem15  24233  cvmlift2lem11  24248  cvmlift2lem12  24249  cvmlift2lem13  24250  cvmlift3lem2  24255  cvmlift3lem6  24259  cvmlift3lem9  24262  umgraex  24279  eupa0  24302  eupares  24303  eupap1  24304  rtrclreclem.refl  24445  rtrclreclem.subset  24446  rtrclreclem.trans  24447  dedekind  24488  dedekindle  24489  ntrivcvgn0  24527  ntrivcvgmullem  24530  zprod  24564  fprod  24568  fprodntriv  24569  fprodser  24576  br8  24671  br6  24672  br4  24673  dfon2lem9  24705  trpredtr  24791  dftrpred3g  24794  frmin  24800  poseq  24811  frrlem5e  24847  elno2  24866  sltval2  24868  noreson  24872  sltres  24876  noxpsgn  24877  bdayfo  24887  nodenselem3  24895  nodenselem6  24898  nodense  24901  nobndlem2  24905  nobndlem4  24907  nobndlem6  24909  nobndlem8  24911  nobndup  24912  nobnddown  24913  nofulllem4  24917  nofulllem5  24918  fobigcup  24998  brbtwn  25086  brcgr  25087  brbtwn2  25092  axpasch  25128  axlowdimlem14  25142  axlowdim2  25147  axcontlem2  25152  axcontlem4  25154  axcontlem7  25157  axcontlem8  25158  axcontlem10  25160  axcontlem12  25162  fvtransport  25214  brcolinear  25241  brsegle  25290  seglerflx  25294  seglemin  25295  btwnsegle  25299  fvray  25323  fvline  25326  hilbert1.1  25336  elhf2  25364  0hf  25366  onsucsuccmpi  25441  limsucncmpi  25443  supaddc  25482  supadd  25483  volsupnfl  25491  itg2addnclem  25492  itg2addnclem2  25493  itg2addnc  25494  nn0prpwlem  25562  nn0prpw  25563  opnregcld  25572  cldregopn  25573  fness  25606  ssref  25607  fneref  25608  refref  25609  fnessref  25617  refssfne  25618  finlocfin  25623  locfindis  25629  comppfsc  25631  neibastop2lem  25633  fnemeet1  25639  tailfb  25650  filnetlem4  25654  unirep  25673  cover2  25682  indexa  25736  frinfm  25740  sdclem1  25777  fdc  25779  incsequz  25782  caushft  25801  istotbnd3  25818  0totbnd  25820  sstotbnd2  25821  sstotbnd  25822  sstotbnd3  25823  isbnd2  25830  isbnd3  25831  ssbnd  25835  totbndbnd  25836  equivbnd  25837  prdsbnd  25840  prdstotbnd  25841  cntotbnd  25843  heibor1lem  25856  heiborlem1  25858  heiborlem3  25860  heiborlem6  25863  heiborlem8  25865  heibor  25868  bfplem2  25870  rrncmslem  25879  iccbnd  25887  exidres  25891  isdrngo2  25912  igenval  26009  igenidl  26011  prnc  26015  prtlem10  26056  elrfi  26092  nacsfix  26110  mzpcompact2lem  26152  eldioph  26160  diophrw  26161  eldioph2b  26165  eldioph3  26168  diophin  26175  rexrabdioph  26198  rexzrexnn0  26208  eldioph4b  26217  eldioph4i  26218  rencldnfilem  26226  irrapxlem5  26234  irrapxlem6  26235  pell1234qrdich  26269  pell14qrdich  26277  infmrgelbi  26286  pellqrex  26287  pellfundre  26289  pellfundlb  26292  pellfund14  26306  rmxyelqirr  26318  rmxynorm  26326  congrep  26383  acongrep  26390  jm2.27  26424  fnwe2lem2  26471  islssfgi  26493  pwssplit1  26511  filnm  26515  frlmup4  26576  unxpwdom3  26579  islindf4  26631  lpirlnr  26644  hbtlem2  26651  hbtlem4  26653  hbtlem5  26655  hbt  26657  dgraaub  26676  mpaaeu  26678  aaitgo  26690  rgspnval  26696  rgspncl  26697  rngunsnply  26701  psgnunilem2  26741  psgnunilem3  26742  psgneldm2i  26751  psgnvalii  26755  dvconstbi  26874  ubelsupr  27014  climsuse  27057  stoweidlem9  27081  stoweidlem18  27090  stoweidlem21  27093  stoweidlem29  27101  stoweidlem34  27106  stoweidlem35  27107  stoweidlem39  27111  stoweidlem41  27113  stoweidlem45  27117  stoweidlem52  27124  stoweidlem55  27127  stoweidlem57  27129  stoweidlem60  27132  stirlinglem5  27150  stirlinglem13  27158  stirlinglem14  27159  sigarcol  27177  elrnrexdm  27427  eldmrexrn  27429  cusgrares  27635  usgrasscusgra  27646  lshpnel2N  29244  lsatlspsn2  29251  lsatlspsn  29252  lsmsat  29267  lssatomic  29270  lcvnbtwn  29284  lfl1  29329  eqlkr  29358  lshpkrlem1  29369  lshpkrex  29377  lfl1dim  29380  lfl1dim2N  29381  lkrss2N  29428  cvrcon3b  29536  glbconN  29635  cvrat4  29701  3dim3  29727  ps-2  29736  llni  29766  llnle  29776  lplni  29790  lplnle  29798  lplnexllnN  29822  lvoli  29833  atpointN  30001  lnatexN  30037  elpaddn0  30058  pclfinN  30158  ispsubcl2N  30205  lhprelat3N  30298  4atexlemex2  30329  4atex  30334  4atex2-0aOLDN  30336  4atex2-0cOLDN  30338  lautcvr  30350  cdleme0ex1N  30481  cdleme50rnlem  30802  cdleme50ex  30817  cdlemg1cex  30846  cdlemkid5  31193  cdlemk  31232  tendoex  31233  cdleml5N  31238  cdlemm10N  31377  dihglblem2aN  31552  dihglblem2N  31553  dih1dimatlem0  31587  dihatexv  31597  dihjat1lem  31687  dvh4dimat  31697  dvh3dim2  31707  dvh3dim3N  31708  dochfl1  31735  dochkr1  31737  dochkr1OLDN  31738  lcfl8  31761  lcfrvalsnN  31800  lcfrlem9  31809  lcfrlem27  31828  lcfrlem37  31838  lcfr  31844  mapdval2N  31889  mapdval4N  31891  mapd1o  31907  mapdcv  31919  mapdspex  31927  mapdpglem23  31953  hdmap11lem2  32104  hdmap14lem2a  32129  hdmap14lem6  32135
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-rex 2625  df-v 2866
  Copyright terms: Public domain W3C validator