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

Theorem rspcev 2897
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 1609 . 2  |-  F/ x ps
2 rspcv.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
31, 2rspce 2892 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 1632    e. wcel 1696   E.wrex 2557
This theorem is referenced by:  rspc2ev  2905  rspc3ev  2907  reu6i  2969  rspesbca  3084  wefrc  4403  wereu2  4406  onfr  4447  ordunidif  4456  onssmin  4604  onminex  4614  onuninsuci  4647  elrnmpt1s  4943  dffv2  5608  foco2  5696  elabrex  5781  f1elima  5803  fcofo  5814  fliftfun  5827  fliftval  5831  f1oiso2  5865  fo1st  6155  fo2nd  6156  sorpssuni  6302  sorpssint  6303  onnseq  6377  tfrlem12  6421  seqomlem2  6479  oawordeulem  6568  oaass  6575  odi  6593  omass  6594  omeulem1  6596  oen0  6600  oeordi  6601  oelim2  6609  oeeulem  6615  nnawordex  6651  nneob  6666  ecelqsg  6730  resixpfo  6870  elixpsn  6871  ixpsnf1o  6872  boxcutc  6875  snfi  6957  onfin  7067  pssnn  7097  ssnnfi  7098  dif1enOLD  7106  dif1en  7107  findcard  7113  frfi  7118  fisupg  7121  nnsdomg  7132  unfi  7140  fofinf1o  7153  pwfilem  7166  fissuni  7176  fipreima  7177  finsschain  7178  indexfi  7179  elfir  7185  fiin  7191  marypha1lem  7202  eqsup  7223  supmaxlem  7231  fisup2g  7233  fisupcl  7234  suppr  7235  supisoex  7238  wofib  7276  wemaplem2  7278  card2inf  7285  brwdom2  7303  cnfcom3clem  7424  trcl  7426  r1ordg  7466  r1pwss  7472  tz9.12lem3  7477  tz9.12  7478  r1elwf  7484  tcrank  7570  scottex  7571  scott0  7572  isnumi  7595  onsdom  7645  fseqdom  7669  ondomen  7680  infpwfien  7705  cardaleph  7732  cardalephex  7733  infenaleph  7734  alephfplem4  7750  alephfp2  7752  dfac2  7773  ackbij1lem18  7879  ackbij1  7880  cflem  7888  cflecard  7895  cfsuc  7899  cfflb  7901  cofsmo  7911  cfsmolem  7912  coftr  7915  fin23lem7  7958  fin23lem11  7959  enfin2i  7963  fin23lem26  7967  fin23lem38  7991  isf32lem5  7999  isf34lem4  8019  isfin1-3  8028  fin1a2lem7  8048  fin1a2lem11  8052  fin1a2lem13  8054  axdc3lem2  8093  axdc3lem4  8095  ttukeylem7  8158  iunfo  8177  ficard  8203  pwcfsdom  8221  fpwwe2lem12  8279  wunex  8377  eltsk2g  8389  grur1  8458  axgroth6  8466  inaprc  8474  nqereu  8569  archnq  8620  genpnmax  8647  ltexpri  8683  prlem936  8687  reclem3pr  8689  recexpr  8691  supexpr  8694  negexsr  8740  recexsrlem  8741  recexsr  8745  supsrlem  8749  axrnegex  8800  axrrecex  8801  axpre-sup  8807  1re  8853  cnegex  9009  cnegex2  9010  recex  9416  receu  9429  fimaxre2  9718  lbinfm  9723  infm3lem  9728  supmul1  9735  supmullem2  9737  supmul  9738  infmrcl  9749  cju  9758  nn2ge  9787  nominpos  9964  zdiv  10098  btwnz  10130  uzwo  10297  uzwoOLD  10298  uzinfmi  10313  ublbneg  10318  lbzbi  10322  zsupss  10323  uzsupss  10326  zq  10338  rpnnen1lem1  10358  rpnnen1lem2  10359  rpnnen1lem3  10360  rpnnen1lem4  10361  rpnnen1lem5  10362  z2ge  10541  qbtwnre  10542  qbtwnxr  10543  xralrple  10548  xrsupsslem  10641  xrinfmsslem  10642  supxrpnf  10653  icc0  10720  iccsupr  10752  flval3  10961  uzsup  10983  fsequb  11053  expnbnd  11246  expmulnbnd  11249  hashkf  11355  hashdom  11377  iswrdi  11433  shftlem  11579  shftfval  11581  sqrlem3  11746  01sqrex  11751  resqrex  11752  sqrneg  11769  abs1m  11835  rexanuz  11845  rexanre  11846  rexuz3  11848  rexuzre  11852  rexico  11853  caubnd2  11857  caubnd  11858  sqreu  11860  rlim2lt  11987  rlim3  11988  lo1bdd2  12014  lo1bddrp  12015  o1lo1  12027  climconst  12033  rlimconst  12034  rlimclim1  12035  climshftlem  12064  rlimcn2  12080  reccn2  12086  cn1lem  12087  rlimo1  12106  o1rlimmul  12108  lo1add  12116  lo1mul  12117  lo1le  12141  isercoll  12157  isercoll2  12158  caucvgrlem  12161  serf0  12169  zsum  12207  fsum  12209  fsumcvg3  12218  climcnds  12326  divrcnv  12327  infcvgaux2i  12332  mertenslem1  12356  mertenslem2  12357  ruclem12  12535  dvdsval2  12550  dvds0lem  12555  dvds1lem  12556  dvds2lem  12557  odd2np1lem  12602  odd2np1  12603  divalglem9  12616  gcdcllem3  12708  bezoutlem1  12733  qredeu  12802  exprmfct  12805  isprm5  12807  maxprmfct  12808  odzcllem  12873  opeo  12882  omeo  12883  pythagtriplem19  12902  pcprmpw2  12950  pcprmpw  12951  pockthi  12970  infpnlem2  12974  prmreclem1  12979  prmreclem5  12983  prmreclem6  12984  1arithlem4  12989  vdwapun  13037  vdwlem1  13044  vdwlem2  13045  vdwlem6  13049  vdwlem8  13051  vdwlem10  13053  vdwlem13  13056  ramcl2lem  13072  ramz  13088  ramub1lem1  13089  elrestr  13349  imasleval  13459  mreexexlem3d  13564  mreexexlem4d  13565  iscatd  13591  poslubd  14267  fpwipodrs  14283  spwpr4  14356  ismgmid2  14406  ismndd  14412  gsumvallem1  14464  gsumval2a  14475  gsumwspan  14484  isgrpd2  14521  isgrpd  14523  imasgrp2  14626  gaorber  14778  orbsta  14783  cayleyth  14806  odf1o2  14900  pgpfi1  14922  sylow1lem3  14927  sylow1lem5  14929  pgpfi  14932  pgpssslw  14941  sylow2alem2  14945  slwhash  14951  fislw  14952  lsmelvalm  14978  pj1id  15024  efgs1b  15061  efgrelexlemb  15075  efgredeu  15077  gexex  15161  cyggeninv  15186  0cyg  15195  lt6abl  15197  eldprdi  15269  pgpfac1lem3a  15327  pgpfac1lem3  15328  pgpfac1lem5  15330  pgpfaclem1  15332  pgpfaclem3  15334  ablfaclem2  15337  dvdsrmul  15446  dvdsr01  15453  irredrmul  15505  lss1d  15736  lspf  15747  lspval  15748  lssats2  15773  lspsn  15775  lspsneq  15891  lspfixed  15897  lspsolvlem  15911  lspprat  15922  lbsextlem2  15928  lpi0  16015  lpi1  16016  aspval  16084  zlpir  16460  zcyg  16461  zncyg  16518  znf1o  16521  cygznlem3  16539  cygth  16541  frgpcyg  16543  fiinbas  16706  topbas  16726  pptbas  16761  clsval  16790  clsval2  16803  elcls  16826  neiint  16857  neips  16866  opnneissb  16867  opnssneib  16868  innei  16878  restbas  16905  restcld  16919  restcldi  16920  restopnb  16922  restcls  16927  ordtbas2  16937  ordtopn1  16940  ordtopn2  16941  leordtval2  16958  iocpnfordt  16961  icomnfordt  16962  lecldbas  16965  pnfnei  16966  mnfnei  16967  lmconst  17007  cncnpi  17023  cnconst2  17027  cnprest  17033  cnpdis  17037  pnrmopn  17087  nrmsep  17101  regsep2  17120  cmpcovf  17134  cncmp  17135  fincmp  17136  cmpsublem  17142  cmpsub  17143  tgcmp  17144  cmpcld  17145  uncmp  17146  hauscmplem  17149  cmpfi  17151  consubclo  17166  concompid  17173  2ndci  17190  2ndcsb  17191  2ndc1stc  17193  1stcrest  17195  2ndcctbss  17197  2ndcdisj  17198  2ndcomap  17200  2ndcsep  17201  dis2ndc  17202  restlly  17225  islly2  17226  hausllycmp  17236  cldllycmp  17237  lly1stc  17238  dislly  17239  llycmpkgen2  17261  cmpkgen  17262  1stckgenlem  17264  elptr  17284  ptbasfi  17292  ptpjopn  17322  txcnp  17330  ptcnplem  17331  txlly  17346  txnlly  17347  txtube  17350  txcmplem1  17351  txcmplem2  17352  tx1stc  17360  txkgen  17362  xkococnlem  17369  txcon  17399  tgqtop  17419  qtopeu  17423  kqreglem1  17448  kqreglem2  17449  kqnrmlem1  17450  kqnrmlem2  17451  reghmph  17500  nrmhmph  17501  fbssfi  17548  opnfbas  17553  isfil2  17567  fsubbas  17578  ssfg  17583  fgss2  17585  fbasrn  17595  filuni  17596  fgtr  17601  ssufl  17629  uffix  17632  elfm  17658  elfm2  17659  elfm3  17661  imaelfm  17662  rnelfmlem  17663  rnelfm  17664  fmfnfmlem3  17667  fmfnfmlem4  17668  fmfnfm  17669  fmco  17672  ufldom  17673  hausflim  17692  flimcls  17696  hauspwpwf1  17698  flffbas  17706  txflf  17717  fclscf  17736  fclsfnflim  17738  alexsubALTlem3  17759  alexsubALTlem4  17760  alexsubALT  17761  ptcmplem2  17763  ptcmplem3  17764  ptcmplem5  17766  tmdgsum2  17795  symgtgp  17800  subgntr  17805  opnsubg  17806  ghmcnp  17813  divstgpopn  17818  tsmsfbas  17826  tsmsgsum  17837  tsmsres  17842  tsmsxplem1  17851  tsmsxp  17853  imasdsf1olem  17953  blss  17988  blssex  17989  ssblex  17990  blin2  17991  neibl  18063  blcld  18067  metss2  18074  stdbdmopn  18080  mopnex  18081  met1stc  18083  met2ndci  18084  metrest  18086  prdsxmslem2  18091  metcnp3  18102  metcnpi3  18108  dscopn  18112  ngptgp  18168  nlmvscnlem1  18213  nrginvrcnlem  18217  nghmcn  18270  tgioo  18318  tgqioo  18322  xrsmopn  18334  zcld  18335  recld2  18336  zdis  18338  icccmplem1  18343  icccmplem2  18344  icccmplem3  18345  reconnlem2  18348  xmetdcn2  18358  metdscn  18376  addcnlem  18384  elcncf1di  18415  icoopnst  18453  iocopnst  18454  xrhmeo  18460  cnheibor  18469  cnllycmp  18470  lebnumlem3  18477  lebnum  18478  xlebnum  18479  lebnumii  18480  elpi1i  18560  ipcnlem1  18688  lmnn  18705  iscfil3  18715  cfilres  18738  flimcfil  18755  cncmet  18760  bcthlem4  18765  bcthlem5  18766  minveclem4c  18805  minveclem2  18806  minveclem3b  18808  minveclem3  18809  minveclem4  18812  minveclem6  18814  ivthlem2  18828  ivthlem3  18829  ivth  18830  ivthle  18832  ivthle2  18833  cniccbdd  18837  elovolmr  18851  ovolunlem1  18872  ovoliunlem1  18877  ovoliunlem2  18878  ovoliun2  18881  ovolicc1  18891  iundisj  18921  iunmbl2  18930  ioombl1lem4  18934  uniioombllem2  18954  uniioombllem3  18956  uniioombllem6  18959  dyadmbllem  18970  volcn  18977  volivth  18978  vitalilem2  18980  mbfinf  19036  mbflimsup  19037  i1faddlem  19064  i1fmullem  19065  itg1addlem4  19070  i1fmulc  19074  itg1climres  19085  itg2lr  19101  itg2monolem1  19121  itg2i1fseq  19126  itg2i1fseq2  19127  itg2cnlem1  19132  itg2cnlem2  19133  limcnlp  19244  ellimc3  19245  limcflf  19247  limciun  19260  dveflem  19342  rollelem  19352  c1lip1  19360  lhop1lem  19376  evlseu  19416  ply1divex  19538  ig1peu  19573  ply1lpir  19580  elply2  19594  plyeq0lem  19608  coeeq  19625  plydivlem3  19691  plydivlem4  19692  elqaalem3  19717  qaa  19719  iaa  19721  aareccl  19722  aannenlem2  19725  aalioulem2  19729  aalioulem3  19730  aalioulem5  19732  aalioulem6  19733  aaliou  19734  aaliou2  19736  aaliou3lem8  19741  ulmshftlem  19784  ulmbdd  19791  iblulm  19799  abelthlem8  19831  reeff1o  19839  pilem2  19844  pilem3  19845  efif1olem2  19921  eflogeq  19971  divlogrlim  19998  efopn  20021  cxpcn3lem  20103  cxpeq  20113  angpieqvd  20144  dcubic2  20156  quart  20173  rlimcnp  20276  xrlimcnp  20279  cxplim  20282  cxploglim  20288  emcllem6  20310  ftalem1  20326  ftalem2  20327  ftalem3  20328  ftalem5  20330  ftalem7  20332  isppw2  20369  sgmnncl  20401  dvdsppwf1o  20442  musum  20447  dvdsmulf1o  20450  perfect  20486  dchrptlem1  20519  dchrptlem2  20520  dchrpt  20522  bpos1lem  20537  lgsqrlem4  20599  lgsdchrval  20602  lgsquadlem1  20609  2sqlem2  20619  mul2sq  20620  2sqlem3  20621  2sqlem9  20628  2sqlem10  20629  2sqblem  20632  dchrisumlem3  20656  dchrisum0  20685  chpdifbndlem2  20719  pntrsumbnd2  20732  pntpbnd1  20751  pntpbnd2  20752  pntpbnd  20753  pntibndlem2  20756  pntibndlem3  20757  pntleme  20773  pntlem3  20774  ostth2  20802  ostth3  20803  lpni  20862  isgrpo  20879  isgrpoi  20881  grpoinvf  20923  isgrpda  20980  isgrpod  20981  isablod  20983  opidon  21005  ghgrp  21051  isrngod  21062  cnrngo  21086  rngmgmbs4  21100  vacn  21283  nmcvcn  21284  smcnlem  21286  nmosetn0  21359  nmoolb  21365  nmobndi  21369  nmoo0  21385  nmlno0lem  21387  isblo3i  21395  blo3i  21396  blocnilem  21398  blocni  21399  ubthlem1  21465  ubthlem2  21466  ubthlem3  21467  minvecolem2  21470  minvecolem3  21471  minvecolem4c  21474  minvecolem4  21475  minvecolem5  21476  minvecolem6  21477  htthlem  21513  norm1exi  21845  occl  21899  shsel3  21910  spanval  21928  spancl  21931  shsval2i  21982  pjhthlem2  21987  ococin  22003  h1de2ctlem  22150  spansncol  22163  pjoml6i  22184  nmopsetn0  22461  nmfnsetn0  22474  nmoplb  22503  nmfnlb  22520  0cnop  22575  0cnfn  22576  idcnop  22577  nmop0  22582  nmfn0  22583  nmlnop0iALT  22591  nmopun  22610  nmcexi  22622  lnconi  22629  lnopcnbd  22632  lnfncnbd  22653  riesz3i  22658  riesz1  22661  cnlnadjlem2  22664  cnlnadjlem8  22670  cnlnadjlem9  22671  adjbd1o  22681  branmfn  22701  opsqrlem1  22736  pjnmopi  22744  strlem1  22846  stri  22853  hstri  22861  cvcon3  22880  cvnbtwn  22882  superpos  22950  shatomici  22954  atcvat4i  22993  mdsymlem2  23000  cdj1i  23029  cdj3lem2  23031  cdj3i  23037  ballotlem4  23073  ballotlemrc  23105  xreceu  23121  rexdiv  23125  rexunirn  23156  elunirn2  23230  ssnnssfz  23292  tpr2rico  23311  iundisjfi  23378  iundisjf  23380  rge0scvg  23388  pnfneige0  23389  esumpcvgval  23461  dmsigagen  23520  dya2iocseg  23594  indf1ofs  23624  dstfrvunirn  23690  subfacp1lem3  23728  erdsze2lem2  23750  cnpcon  23776  txpcon  23778  ptpcon  23779  indispcon  23780  conpcon  23781  cvxpcon  23788  cnllyscon  23791  cvmsss2  23820  cvmcov2  23821  cvmopnlem  23824  cvmfolem  23825  cvmliftlem14  23843  cvmliftlem15  23844  cvmlift2lem11  23859  cvmlift2lem12  23860  cvmlift2lem13  23861  cvmlift3lem2  23866  cvmlift3lem6  23870  cvmlift3lem9  23873  umgraex  23890  eupa0  23913  eupares  23914  eupap1  23915  rtrclreclem.refl  24056  rtrclreclem.subset  24057  rtrclreclem.trans  24058  dedekind  24097  dedekindle  24098  faclimlem5  24121  zprod  24160  zprodn0  24162  fprod  24164  br8  24184  br6  24185  br4  24186  dfon2lem9  24218  trpredtr  24304  dftrpred3g  24307  frmin  24313  poseq  24324  frrlem5e  24360  elno2  24379  sltval2  24381  noreson  24385  sltres  24389  noxpsgn  24390  bdayfo  24400  nodenselem3  24408  nodenselem6  24411  nodense  24414  nobndlem2  24418  nobndlem4  24420  nobndlem6  24422  nobndlem8  24424  nobndup  24425  nobnddown  24426  nofulllem4  24430  nofulllem5  24431  fobigcup  24511  brbtwn  24599  brcgr  24600  brbtwn2  24605  axpasch  24641  axlowdimlem14  24655  axlowdim2  24660  axcontlem2  24665  axcontlem4  24667  axcontlem7  24670  axcontlem8  24671  axcontlem10  24673  axcontlem12  24675  fvtransport  24727  brcolinear  24754  brsegle  24803  seglerflx  24807  seglemin  24808  btwnsegle  24812  fvray  24836  fvline  24839  hilbert1.1  24849  elhf2  24877  0hf  24879  onsucsuccmpi  24954  limsucncmpi  24956  supaddc  24995  supadd  24996  itg2addnclem  25003  itg2addnclem2  25004  itg2addnc  25005  imgfldref2  25167  prj1b  25182  prj3  25183  prl  25270  domncnt  25385  ranncnt  25386  latdir  25398  dffprod  25422  mgmlion  25440  trran2  25496  ltrran2  25506  rltrran  25517  svs2  25590  unint2t  25621  intfmu2  25622  apnei  25623  basexre  25625  sallnei  25632  nsn  25633  osneisi  25634  intopcoaconlem3b  25641  intopcoaconlem3  25642  istopx  25650  efilcp  25655  iscnp4  25666  prdnei  25676  limptlimpr2lem2  25678  flfnei2  25680  islimrs4  25685  iintlem1  25713  iintlem2  25714  trran  25717  lvsovso  25729  vecaddonto  25762  cnegvex2  25763  rnegvex2  25764  negveud  25771  negveudr  25772  vecscmonto  25789  tcnvec  25793  idfisf  25944  idsubfun  25961  partarelt1  25999  partarelt2  26000  1iskle  26092  empklst  26112  clscnc  26113  phckle  26130  psckle  26131  fnckle  26148  cndpv  26152  pgapspf  26155  gltpntl  26175  lppotos  26247  bosser  26270  pdiveql  26271  nn0prpwlem  26341  nn0prpw  26342  opnregcld  26351  cldregopn  26352  fness  26385  ssref  26386  fneref  26387  refref  26388  fnessref  26396  refssfne  26397  finlocfin  26402  locfindis  26408  comppfsc  26410  neibastop2lem  26412  fnemeet1  26418  tailfb  26429  filnetlem4  26433  unirep  26452  cover2  26461  indexa  26515  frinfm  26519  sdclem1  26556  fdc  26558  incsequz  26561  caushft  26580  istotbnd3  26598  0totbnd  26600  sstotbnd2  26601  sstotbnd  26602  sstotbnd3  26603  isbnd2  26610  isbnd3  26611  ssbnd  26615  totbndbnd  26616  equivbnd  26617  prdsbnd  26620  prdstotbnd  26621  cntotbnd  26623  heibor1lem  26636  heiborlem1  26638  heiborlem3  26640  heiborlem6  26643  heiborlem8  26645  heibor  26648  bfplem2  26650  rrncmslem  26659  iccbnd  26667  exidres  26671  isdrngo2  26692  igenval  26789  igenidl  26791  prnc  26795  prtlem10  26836  elrfi  26872  nacsfix  26890  mzpcompact2lem  26932  eldioph  26940  diophrw  26941  eldioph2b  26945  eldioph3  26948  diophin  26955  rexrabdioph  26978  rexzrexnn0  26988  eldioph4b  26997  eldioph4i  26998  rencldnfilem  27006  irrapxlem5  27014  irrapxlem6  27015  pell1234qrdich  27049  pell14qrdich  27057  infmrgelbi  27066  pellqrex  27067  pellfundre  27069  pellfundlb  27072  pellfund14  27086  rmxyelqirr  27098  rmxynorm  27106  congrep  27163  acongrep  27170  jm2.27  27204  fnwe2lem2  27251  islssfgi  27273  pwssplit1  27291  filnm  27295  frlmup4  27356  unxpwdom3  27359  islindf4  27411  lpirlnr  27424  hbtlem2  27431  hbtlem4  27433  hbtlem5  27435  hbt  27437  dgraaub  27456  mpaaeu  27458  aaitgo  27470  rgspnval  27476  rgspncl  27477  rngunsnply  27481  psgnunilem2  27521  psgnunilem3  27522  psgneldm2i  27531  psgnvalii  27535  dvconstbi  27654  ubelsupr  27794  climsuse  27837  stoweidlem9  27861  stoweidlem18  27870  stoweidlem21  27873  stoweidlem29  27881  stoweidlem34  27886  stoweidlem35  27887  stoweidlem39  27891  stoweidlem41  27893  stoweidlem45  27897  stoweidlem52  27904  stoweidlem55  27907  stoweidlem57  27909  stoweidlem60  27912  stirlinglem5  27930  stirlinglem13  27938  stirlinglem14  27939  sigarcol  27957  lshpnel2N  29797  lsatlspsn2  29804  lsatlspsn  29805  lsmsat  29820  lssatomic  29823  lcvnbtwn  29837  lfl1  29882  eqlkr  29911  lshpkrlem1  29922  lshpkrex  29930  lfl1dim  29933  lfl1dim2N  29934  lkrss2N  29981  cvrcon3b  30089  glbconN  30188  cvrat4  30254  3dim3  30280  ps-2  30289  llni  30319  llnle  30329  lplni  30343  lplnle  30351  lplnexllnN  30375  lvoli  30386  atpointN  30554  lnatexN  30590  elpaddn0  30611  pclfinN  30711  ispsubcl2N  30758  lhprelat3N  30851  4atexlemex2  30882  4atex  30887  4atex2-0aOLDN  30889  4atex2-0cOLDN  30891  lautcvr  30903  cdleme0ex1N  31034  cdleme50rnlem  31355  cdleme50ex  31370  cdlemg1cex  31399  cdlemkid5  31746  cdlemk  31785  tendoex  31786  cdleml5N  31791  cdlemm10N  31930  dihglblem2aN  32105  dihglblem2N  32106  dih1dimatlem0  32140  dihatexv  32150  dihjat1lem  32240  dvh4dimat  32250  dvh3dim2  32260  dvh3dim3N  32261  dochfl1  32288  dochkr1  32290  dochkr1OLDN  32291  lcfl8  32314  lcfrvalsnN  32353  lcfrlem9  32362  lcfrlem27  32381  lcfrlem37  32391  lcfr  32397  mapdval2N  32442  mapdval4N  32444  mapd1o  32460  mapdcv  32472  mapdspex  32480  mapdpglem23  32506  hdmap11lem2  32657  hdmap14lem2a  32682  hdmap14lem6  32688
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rex 2562  df-v 2803
  Copyright terms: Public domain W3C validator