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

Theorem rspcev 2884
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 1605 . 2  |-  F/ x ps
2 rspcv.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
31, 2rspce 2879 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 1623    e. wcel 1684   E.wrex 2544
This theorem is referenced by:  rspc2ev  2892  rspc3ev  2894  reu6i  2956  rspesbca  3071  wefrc  4387  wereu2  4390  onfr  4431  ordunidif  4440  onssmin  4588  onminex  4598  onuninsuci  4631  elrnmpt1s  4927  dffv2  5592  foco2  5680  elabrex  5765  f1elima  5787  fcofo  5798  fliftfun  5811  fliftval  5815  f1oiso2  5849  fo1st  6139  fo2nd  6140  sorpssuni  6286  sorpssint  6287  onnseq  6361  tfrlem12  6405  seqomlem2  6463  oawordeulem  6552  oaass  6559  odi  6577  omass  6578  omeulem1  6580  oen0  6584  oeordi  6585  oelim2  6593  oeeulem  6599  nnawordex  6635  nneob  6650  ecelqsg  6714  resixpfo  6854  elixpsn  6855  ixpsnf1o  6856  boxcutc  6859  snfi  6941  onfin  7051  pssnn  7081  ssnnfi  7082  dif1enOLD  7090  dif1en  7091  findcard  7097  frfi  7102  fisupg  7105  nnsdomg  7116  unfi  7124  fofinf1o  7137  pwfilem  7150  fissuni  7160  fipreima  7161  finsschain  7162  indexfi  7163  elfir  7169  fiin  7175  marypha1lem  7186  eqsup  7207  supmaxlem  7215  fisup2g  7217  fisupcl  7218  suppr  7219  supisoex  7222  wofib  7260  wemaplem2  7262  card2inf  7269  brwdom2  7287  cnfcom3clem  7408  trcl  7410  r1ordg  7450  r1pwss  7456  tz9.12lem3  7461  tz9.12  7462  r1elwf  7468  tcrank  7554  scottex  7555  scott0  7556  isnumi  7579  onsdom  7629  fseqdom  7653  ondomen  7664  infpwfien  7689  cardaleph  7716  cardalephex  7717  infenaleph  7718  alephfplem4  7734  alephfp2  7736  dfac2  7757  ackbij1lem18  7863  ackbij1  7864  cflem  7872  cflecard  7879  cfsuc  7883  cfflb  7885  cofsmo  7895  cfsmolem  7896  coftr  7899  fin23lem7  7942  fin23lem11  7943  enfin2i  7947  fin23lem26  7951  fin23lem38  7975  isf32lem5  7983  isf34lem4  8003  isfin1-3  8012  fin1a2lem7  8032  fin1a2lem11  8036  fin1a2lem13  8038  axdc3lem2  8077  axdc3lem4  8079  ttukeylem7  8142  iunfo  8161  ficard  8187  pwcfsdom  8205  fpwwe2lem12  8263  wunex  8361  eltsk2g  8373  grur1  8442  axgroth6  8450  inaprc  8458  nqereu  8553  archnq  8604  genpnmax  8631  ltexpri  8667  prlem936  8671  reclem3pr  8673  recexpr  8675  supexpr  8678  negexsr  8724  recexsrlem  8725  recexsr  8729  supsrlem  8733  axrnegex  8784  axrrecex  8785  axpre-sup  8791  1re  8837  cnegex  8993  cnegex2  8994  recex  9400  receu  9413  fimaxre2  9702  lbinfm  9707  infm3lem  9712  supmul1  9719  supmullem2  9721  supmul  9722  infmrcl  9733  cju  9742  nn2ge  9771  nominpos  9948  zdiv  10082  btwnz  10114  uzwo  10281  uzwoOLD  10282  uzinfmi  10297  ublbneg  10302  lbzbi  10306  zsupss  10307  uzsupss  10310  zq  10322  rpnnen1lem1  10342  rpnnen1lem2  10343  rpnnen1lem3  10344  rpnnen1lem4  10345  rpnnen1lem5  10346  z2ge  10525  qbtwnre  10526  qbtwnxr  10527  xralrple  10532  xrsupsslem  10625  xrinfmsslem  10626  supxrpnf  10637  icc0  10704  iccsupr  10736  flval3  10945  uzsup  10967  fsequb  11037  expnbnd  11230  expmulnbnd  11233  hashkf  11339  hashdom  11361  iswrdi  11417  shftlem  11563  shftfval  11565  sqrlem3  11730  01sqrex  11735  resqrex  11736  sqrneg  11753  abs1m  11819  rexanuz  11829  rexanre  11830  rexuz3  11832  rexuzre  11836  rexico  11837  caubnd2  11841  caubnd  11842  sqreu  11844  rlim2lt  11971  rlim3  11972  lo1bdd2  11998  lo1bddrp  11999  o1lo1  12011  climconst  12017  rlimconst  12018  rlimclim1  12019  climshftlem  12048  rlimcn2  12064  reccn2  12070  cn1lem  12071  rlimo1  12090  o1rlimmul  12092  lo1add  12100  lo1mul  12101  lo1le  12125  isercoll  12141  isercoll2  12142  caucvgrlem  12145  serf0  12153  zsum  12191  fsum  12193  fsumcvg3  12202  climcnds  12310  divrcnv  12311  infcvgaux2i  12316  mertenslem1  12340  mertenslem2  12341  ruclem12  12519  dvdsval2  12534  dvds0lem  12539  dvds1lem  12540  dvds2lem  12541  odd2np1lem  12586  odd2np1  12587  divalglem9  12600  gcdcllem3  12692  bezoutlem1  12717  qredeu  12786  exprmfct  12789  isprm5  12791  maxprmfct  12792  odzcllem  12857  opeo  12866  omeo  12867  pythagtriplem19  12886  pcprmpw2  12934  pcprmpw  12935  pockthi  12954  infpnlem2  12958  prmreclem1  12963  prmreclem5  12967  prmreclem6  12968  1arithlem4  12973  vdwapun  13021  vdwlem1  13028  vdwlem2  13029  vdwlem6  13033  vdwlem8  13035  vdwlem10  13037  vdwlem13  13040  ramcl2lem  13056  ramz  13072  ramub1lem1  13073  elrestr  13333  imasleval  13443  mreexexlem3d  13548  mreexexlem4d  13549  iscatd  13575  poslubd  14251  fpwipodrs  14267  spwpr4  14340  ismgmid2  14390  ismndd  14396  gsumvallem1  14448  gsumval2a  14459  gsumwspan  14468  isgrpd2  14505  isgrpd  14507  imasgrp2  14610  gaorber  14762  orbsta  14767  cayleyth  14790  odf1o2  14884  pgpfi1  14906  sylow1lem3  14911  sylow1lem5  14913  pgpfi  14916  pgpssslw  14925  sylow2alem2  14929  slwhash  14935  fislw  14936  lsmelvalm  14962  pj1id  15008  efgs1b  15045  efgrelexlemb  15059  efgredeu  15061  gexex  15145  cyggeninv  15170  0cyg  15179  lt6abl  15181  eldprdi  15253  pgpfac1lem3a  15311  pgpfac1lem3  15312  pgpfac1lem5  15314  pgpfaclem1  15316  pgpfaclem3  15318  ablfaclem2  15321  dvdsrmul  15430  dvdsr01  15437  irredrmul  15489  lss1d  15720  lspf  15731  lspval  15732  lssats2  15757  lspsn  15759  lspsneq  15875  lspfixed  15881  lspsolvlem  15895  lspprat  15906  lbsextlem2  15912  lpi0  15999  lpi1  16000  aspval  16068  zlpir  16444  zcyg  16445  zncyg  16502  znf1o  16505  cygznlem3  16523  cygth  16525  frgpcyg  16527  fiinbas  16690  topbas  16710  pptbas  16745  clsval  16774  clsval2  16787  elcls  16810  neiint  16841  neips  16850  opnneissb  16851  opnssneib  16852  innei  16862  restbas  16889  restcld  16903  restcldi  16904  restopnb  16906  restcls  16911  ordtbas2  16921  ordtopn1  16924  ordtopn2  16925  leordtval2  16942  iocpnfordt  16945  icomnfordt  16946  lecldbas  16949  pnfnei  16950  mnfnei  16951  lmconst  16991  cncnpi  17007  cnconst2  17011  cnprest  17017  cnpdis  17021  pnrmopn  17071  nrmsep  17085  regsep2  17104  cmpcovf  17118  cncmp  17119  fincmp  17120  cmpsublem  17126  cmpsub  17127  tgcmp  17128  cmpcld  17129  uncmp  17130  hauscmplem  17133  cmpfi  17135  consubclo  17150  concompid  17157  2ndci  17174  2ndcsb  17175  2ndc1stc  17177  1stcrest  17179  2ndcctbss  17181  2ndcdisj  17182  2ndcomap  17184  2ndcsep  17185  dis2ndc  17186  restlly  17209  islly2  17210  hausllycmp  17220  cldllycmp  17221  lly1stc  17222  dislly  17223  llycmpkgen2  17245  cmpkgen  17246  1stckgenlem  17248  elptr  17268  ptbasfi  17276  ptpjopn  17306  txcnp  17314  ptcnplem  17315  txlly  17330  txnlly  17331  txtube  17334  txcmplem1  17335  txcmplem2  17336  tx1stc  17344  txkgen  17346  xkococnlem  17353  txcon  17383  tgqtop  17403  qtopeu  17407  kqreglem1  17432  kqreglem2  17433  kqnrmlem1  17434  kqnrmlem2  17435  reghmph  17484  nrmhmph  17485  fbssfi  17532  opnfbas  17537  isfil2  17551  fsubbas  17562  ssfg  17567  fgss2  17569  fbasrn  17579  filuni  17580  fgtr  17585  ssufl  17613  uffix  17616  elfm  17642  elfm2  17643  elfm3  17645  imaelfm  17646  rnelfmlem  17647  rnelfm  17648  fmfnfmlem3  17651  fmfnfmlem4  17652  fmfnfm  17653  fmco  17656  ufldom  17657  hausflim  17676  flimcls  17680  hauspwpwf1  17682  flffbas  17690  txflf  17701  fclscf  17720  fclsfnflim  17722  alexsubALTlem3  17743  alexsubALTlem4  17744  alexsubALT  17745  ptcmplem2  17747  ptcmplem3  17748  ptcmplem5  17750  tmdgsum2  17779  symgtgp  17784  subgntr  17789  opnsubg  17790  ghmcnp  17797  divstgpopn  17802  tsmsfbas  17810  tsmsgsum  17821  tsmsres  17826  tsmsxplem1  17835  tsmsxp  17837  imasdsf1olem  17937  blss  17972  blssex  17973  ssblex  17974  blin2  17975  neibl  18047  blcld  18051  metss2  18058  stdbdmopn  18064  mopnex  18065  met1stc  18067  met2ndci  18068  metrest  18070  prdsxmslem2  18075  metcnp3  18086  metcnpi3  18092  dscopn  18096  ngptgp  18152  nlmvscnlem1  18197  nrginvrcnlem  18201  nghmcn  18254  tgioo  18302  tgqioo  18306  xrsmopn  18318  zcld  18319  recld2  18320  zdis  18322  icccmplem1  18327  icccmplem2  18328  icccmplem3  18329  reconnlem2  18332  xmetdcn2  18342  metdscn  18360  addcnlem  18368  elcncf1di  18399  icoopnst  18437  iocopnst  18438  xrhmeo  18444  cnheibor  18453  cnllycmp  18454  lebnumlem3  18461  lebnum  18462  xlebnum  18463  lebnumii  18464  elpi1i  18544  ipcnlem1  18672  lmnn  18689  iscfil3  18699  cfilres  18722  flimcfil  18739  cncmet  18744  bcthlem4  18749  bcthlem5  18750  minveclem4c  18789  minveclem2  18790  minveclem3b  18792  minveclem3  18793  minveclem4  18796  minveclem6  18798  ivthlem2  18812  ivthlem3  18813  ivth  18814  ivthle  18816  ivthle2  18817  cniccbdd  18821  elovolmr  18835  ovolunlem1  18856  ovoliunlem1  18861  ovoliunlem2  18862  ovoliun2  18865  ovolicc1  18875  iundisj  18905  iunmbl2  18914  ioombl1lem4  18918  uniioombllem2  18938  uniioombllem3  18940  uniioombllem6  18943  dyadmbllem  18954  volcn  18961  volivth  18962  vitalilem2  18964  mbfinf  19020  mbflimsup  19021  i1faddlem  19048  i1fmullem  19049  itg1addlem4  19054  i1fmulc  19058  itg1climres  19069  itg2lr  19085  itg2monolem1  19105  itg2i1fseq  19110  itg2i1fseq2  19111  itg2cnlem1  19116  itg2cnlem2  19117  limcnlp  19228  ellimc3  19229  limcflf  19231  limciun  19244  dveflem  19326  rollelem  19336  c1lip1  19344  lhop1lem  19360  evlseu  19400  ply1divex  19522  ig1peu  19557  ply1lpir  19564  elply2  19578  plyeq0lem  19592  coeeq  19609  plydivlem3  19675  plydivlem4  19676  elqaalem3  19701  qaa  19703  iaa  19705  aareccl  19706  aannenlem2  19709  aalioulem2  19713  aalioulem3  19714  aalioulem5  19716  aalioulem6  19717  aaliou  19718  aaliou2  19720  aaliou3lem8  19725  ulmshftlem  19768  ulmbdd  19775  iblulm  19783  abelthlem8  19815  reeff1o  19823  pilem2  19828  pilem3  19829  efif1olem2  19905  eflogeq  19955  divlogrlim  19982  efopn  20005  cxpcn3lem  20087  cxpeq  20097  angpieqvd  20128  dcubic2  20140  quart  20157  rlimcnp  20260  xrlimcnp  20263  cxplim  20266  cxploglim  20272  emcllem6  20294  ftalem1  20310  ftalem2  20311  ftalem3  20312  ftalem5  20314  ftalem7  20316  isppw2  20353  sgmnncl  20385  dvdsppwf1o  20426  musum  20431  dvdsmulf1o  20434  perfect  20470  dchrptlem1  20503  dchrptlem2  20504  dchrpt  20506  bpos1lem  20521  lgsqrlem4  20583  lgsdchrval  20586  lgsquadlem1  20593  2sqlem2  20603  mul2sq  20604  2sqlem3  20605  2sqlem9  20612  2sqlem10  20613  2sqblem  20616  dchrisumlem3  20640  dchrisum0  20669  chpdifbndlem2  20703  pntrsumbnd2  20716  pntpbnd1  20735  pntpbnd2  20736  pntpbnd  20737  pntibndlem2  20740  pntibndlem3  20741  pntleme  20757  pntlem3  20758  ostth2  20786  ostth3  20787  lpni  20846  isgrpo  20863  isgrpoi  20865  grpoinvf  20907  isgrpda  20964  isgrpod  20965  isablod  20967  opidon  20989  ghgrp  21035  isrngod  21046  cnrngo  21070  rngmgmbs4  21084  vacn  21267  nmcvcn  21268  smcnlem  21270  nmosetn0  21343  nmoolb  21349  nmobndi  21353  nmoo0  21369  nmlno0lem  21371  isblo3i  21379  blo3i  21380  blocnilem  21382  blocni  21383  ubthlem1  21449  ubthlem2  21450  ubthlem3  21451  minvecolem2  21454  minvecolem3  21455  minvecolem4c  21458  minvecolem4  21459  minvecolem5  21460  minvecolem6  21461  htthlem  21497  norm1exi  21829  occl  21883  shsel3  21894  spanval  21912  spancl  21915  shsval2i  21966  pjhthlem2  21971  ococin  21987  h1de2ctlem  22134  spansncol  22147  pjoml6i  22168  nmopsetn0  22445  nmfnsetn0  22458  nmoplb  22487  nmfnlb  22504  0cnop  22559  0cnfn  22560  idcnop  22561  nmop0  22566  nmfn0  22567  nmlnop0iALT  22575  nmopun  22594  nmcexi  22606  lnconi  22613  lnopcnbd  22616  lnfncnbd  22637  riesz3i  22642  riesz1  22645  cnlnadjlem2  22648  cnlnadjlem8  22654  cnlnadjlem9  22655  adjbd1o  22665  branmfn  22685  opsqrlem1  22720  pjnmopi  22728  strlem1  22830  stri  22837  hstri  22845  cvcon3  22864  cvnbtwn  22866  superpos  22934  shatomici  22938  atcvat4i  22977  mdsymlem2  22984  cdj1i  23013  cdj3lem2  23015  cdj3i  23021  ballotlem4  23057  ballotlemrc  23089  xreceu  23105  rexdiv  23109  rexunirn  23140  elunirn2  23215  ssnnssfz  23277  tpr2rico  23296  iundisjfi  23363  iundisjf  23365  rge0scvg  23373  pnfneige0  23374  esumpcvgval  23446  dmsigagen  23505  dya2iocseg  23579  indf1ofs  23609  dstfrvunirn  23675  subfacp1lem3  23713  erdsze2lem2  23735  cnpcon  23761  txpcon  23763  ptpcon  23764  indispcon  23765  conpcon  23766  cvxpcon  23773  cnllyscon  23776  cvmsss2  23805  cvmcov2  23806  cvmopnlem  23809  cvmfolem  23810  cvmliftlem14  23828  cvmliftlem15  23829  cvmlift2lem11  23844  cvmlift2lem12  23845  cvmlift2lem13  23846  cvmlift3lem2  23851  cvmlift3lem6  23855  cvmlift3lem9  23858  umgraex  23875  eupa0  23898  eupares  23899  eupap1  23900  rtrclreclem.refl  24041  rtrclreclem.subset  24042  rtrclreclem.trans  24043  dedekind  24082  dedekindle  24083  br8  24113  br6  24114  br4  24115  dfon2lem9  24147  trpredtr  24233  dftrpred3g  24236  frmin  24242  poseq  24253  frrlem5e  24289  elno2  24308  sltval2  24310  noreson  24314  sltres  24318  noxpsgn  24319  bdayfo  24329  nodenselem3  24337  nodenselem6  24340  nodense  24343  nobndlem2  24347  nobndlem4  24349  nobndlem6  24351  nobndlem8  24353  nobndup  24354  nobnddown  24355  nofulllem4  24359  nofulllem5  24360  fobigcup  24440  brbtwn  24527  brcgr  24528  brbtwn2  24533  axpasch  24569  axlowdimlem14  24583  axlowdim2  24588  axcontlem2  24593  axcontlem4  24595  axcontlem7  24598  axcontlem8  24599  axcontlem10  24601  axcontlem12  24603  fvtransport  24655  brcolinear  24682  brsegle  24731  seglerflx  24735  seglemin  24736  btwnsegle  24740  fvray  24764  fvline  24767  hilbert1.1  24777  elhf2  24805  0hf  24807  onsucsuccmpi  24882  limsucncmpi  24884  imgfldref2  25064  prj1b  25079  prj3  25080  prl  25167  domncnt  25282  ranncnt  25283  latdir  25295  dffprod  25319  mgmlion  25337  trran2  25393  ltrran2  25403  rltrran  25414  svs2  25487  unint2t  25518  intfmu2  25519  apnei  25520  basexre  25522  sallnei  25529  nsn  25530  osneisi  25531  intopcoaconlem3b  25538  intopcoaconlem3  25539  istopx  25547  efilcp  25552  iscnp4  25563  prdnei  25573  limptlimpr2lem2  25575  flfnei2  25577  islimrs4  25582  iintlem1  25610  iintlem2  25611  trran  25614  lvsovso  25626  vecaddonto  25659  cnegvex2  25660  rnegvex2  25661  negveud  25668  negveudr  25669  vecscmonto  25686  tcnvec  25690  idfisf  25841  idsubfun  25858  partarelt1  25896  partarelt2  25897  1iskle  25989  empklst  26009  clscnc  26010  phckle  26027  psckle  26028  fnckle  26045  cndpv  26049  pgapspf  26052  gltpntl  26072  lppotos  26144  bosser  26167  pdiveql  26168  nn0prpwlem  26238  nn0prpw  26239  opnregcld  26248  cldregopn  26249  fness  26282  ssref  26283  fneref  26284  refref  26285  fnessref  26293  refssfne  26294  finlocfin  26299  locfindis  26305  comppfsc  26307  neibastop2lem  26309  fnemeet1  26315  tailfb  26326  filnetlem4  26330  unirep  26349  cover2  26358  indexa  26412  frinfm  26416  sdclem1  26453  fdc  26455  incsequz  26458  caushft  26477  istotbnd3  26495  0totbnd  26497  sstotbnd2  26498  sstotbnd  26499  sstotbnd3  26500  isbnd2  26507  isbnd3  26508  ssbnd  26512  totbndbnd  26513  equivbnd  26514  prdsbnd  26517  prdstotbnd  26518  cntotbnd  26520  heibor1lem  26533  heiborlem1  26535  heiborlem3  26537  heiborlem6  26540  heiborlem8  26542  heibor  26545  bfplem2  26547  rrncmslem  26556  iccbnd  26564  exidres  26568  isdrngo2  26589  igenval  26686  igenidl  26688  prnc  26692  prtlem10  26733  elrfi  26769  nacsfix  26787  mzpcompact2lem  26829  eldioph  26837  diophrw  26838  eldioph2b  26842  eldioph3  26845  diophin  26852  rexrabdioph  26875  rexzrexnn0  26885  eldioph4b  26894  eldioph4i  26895  rencldnfilem  26903  irrapxlem5  26911  irrapxlem6  26912  pell1234qrdich  26946  pell14qrdich  26954  infmrgelbi  26963  pellqrex  26964  pellfundre  26966  pellfundlb  26969  pellfund14  26983  rmxyelqirr  26995  rmxynorm  27003  congrep  27060  acongrep  27067  jm2.27  27101  fnwe2lem2  27148  islssfgi  27170  pwssplit1  27188  filnm  27192  frlmup4  27253  unxpwdom3  27256  islindf4  27308  lpirlnr  27321  hbtlem2  27328  hbtlem4  27330  hbtlem5  27332  hbt  27334  dgraaub  27353  mpaaeu  27355  aaitgo  27367  rgspnval  27373  rgspncl  27374  rngunsnply  27378  psgnunilem2  27418  psgnunilem3  27419  psgneldm2i  27428  psgnvalii  27432  dvconstbi  27551  ubelsupr  27691  climsuse  27734  stoweidlem9  27758  stoweidlem18  27767  stoweidlem21  27770  stoweidlem29  27778  stoweidlem34  27783  stoweidlem35  27784  stoweidlem39  27788  stoweidlem41  27790  stoweidlem45  27794  stoweidlem52  27801  stoweidlem55  27804  stoweidlem57  27806  stoweidlem60  27809  stirlinglem5  27827  stirlinglem13  27835  stirlinglem14  27836  sigarcol  27854  lshpnel2N  29175  lsatlspsn2  29182  lsatlspsn  29183  lsmsat  29198  lssatomic  29201  lcvnbtwn  29215  lfl1  29260  eqlkr  29289  lshpkrlem1  29300  lshpkrex  29308  lfl1dim  29311  lfl1dim2N  29312  lkrss2N  29359  cvrcon3b  29467  glbconN  29566  cvrat4  29632  3dim3  29658  ps-2  29667  llni  29697  llnle  29707  lplni  29721  lplnle  29729  lplnexllnN  29753  lvoli  29764  atpointN  29932  lnatexN  29968  elpaddn0  29989  pclfinN  30089  ispsubcl2N  30136  lhprelat3N  30229  4atexlemex2  30260  4atex  30265  4atex2-0aOLDN  30267  4atex2-0cOLDN  30269  lautcvr  30281  cdleme0ex1N  30412  cdleme50rnlem  30733  cdleme50ex  30748  cdlemg1cex  30777  cdlemkid5  31124  cdlemk  31163  tendoex  31164  cdleml5N  31169  cdlemm10N  31308  dihglblem2aN  31483  dihglblem2N  31484  dih1dimatlem0  31518  dihatexv  31528  dihjat1lem  31618  dvh4dimat  31628  dvh3dim2  31638  dvh3dim3N  31639  dochfl1  31666  dochkr1  31668  dochkr1OLDN  31669  lcfl8  31692  lcfrvalsnN  31731  lcfrlem9  31740  lcfrlem27  31759  lcfrlem37  31769  lcfr  31775  mapdval2N  31820  mapdval4N  31822  mapd1o  31838  mapdcv  31850  mapdspex  31858  mapdpglem23  31884  hdmap11lem2  32035  hdmap14lem2a  32060  hdmap14lem6  32066
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549  df-v 2790
  Copyright terms: Public domain W3C validator