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

Theorem rspcev 2988
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 1626 . 2  |-  F/ x ps
2 rspcv.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
31, 2rspce 2983 1  |-  ( ( A  e.  B  /\  ps )  ->  E. x  e.  B  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1649    e. wcel 1717   E.wrex 2643
This theorem is referenced by:  rspc2ev  2996  rspc3ev  2998  reu6i  3061  rspesbca  3177  wefrc  4510  wereu2  4513  onfr  4554  ordunidif  4563  onssmin  4710  onminex  4720  onuninsuci  4753  elrnmpt1s  5051  dffv2  5728  elrnrexdm  5806  eldmrexrn  5808  foco2  5821  elabrex  5917  f1elima  5941  fcofo  5953  fliftfun  5966  fliftval  5970  f1oiso2  6004  fo1st  6298  fo2nd  6299  sorpssuni  6460  sorpssint  6461  onnseq  6535  tfrlem12  6579  seqomlem2  6637  oawordeulem  6726  oaass  6733  odi  6751  omass  6752  omeulem1  6754  oen0  6758  oeordi  6759  oelim2  6767  oeeulem  6773  nnawordex  6809  nneob  6824  ecelqsg  6888  resixpfo  7029  elixpsn  7030  ixpsnf1o  7031  boxcutc  7034  snfi  7116  onfin  7226  pssnn  7256  ssnnfi  7257  dif1enOLD  7269  dif1en  7270  findcard  7276  frfi  7281  fisupg  7284  nnsdomg  7295  unfi  7303  fofinf1o  7316  pwfilem  7329  fissuni  7339  fipreima  7340  finsschain  7341  indexfi  7342  elfir  7348  inelfi  7351  fiin  7355  marypha1lem  7366  eqsup  7387  supmaxlem  7395  fisup2g  7397  fisupcl  7398  supisoex  7402  wofib  7440  wemaplem2  7442  card2inf  7449  brwdom2  7467  cnfcom3clem  7588  trcl  7590  r1ordg  7630  r1pwss  7636  tz9.12lem3  7641  tz9.12  7642  r1elwf  7648  tcrank  7734  scottex  7735  scott0  7736  isnumi  7759  onsdom  7809  fseqdom  7833  ondomen  7844  infpwfien  7869  cardaleph  7896  cardalephex  7897  infenaleph  7898  alephfplem4  7914  alephfp2  7916  dfac2  7937  ackbij1lem18  8043  ackbij1  8044  cflem  8052  cflecard  8059  cfsuc  8063  cfflb  8065  cofsmo  8075  cfsmolem  8076  coftr  8079  fin23lem7  8122  fin23lem11  8123  enfin2i  8127  fin23lem26  8131  fin23lem38  8155  isf32lem5  8163  isf34lem4  8183  isfin1-3  8192  fin1a2lem7  8212  fin1a2lem11  8216  fin1a2lem13  8218  axdc3lem2  8257  axdc3lem4  8259  ttukeylem7  8321  iunfo  8340  ficard  8366  pwcfsdom  8384  fpwwe2lem12  8442  wunex  8540  eltsk2g  8552  grur1  8621  axgroth6  8629  inaprc  8637  nqereu  8732  archnq  8783  genpnmax  8810  ltexpri  8846  prlem936  8850  reclem3pr  8852  recexpr  8854  supexpr  8857  negexsr  8903  recexsrlem  8904  recexsr  8908  supsrlem  8912  axrnegex  8963  axrrecex  8964  axpre-sup  8970  1re  9016  cnegex  9172  cnegex2  9173  recex  9579  receu  9592  fimaxre2  9881  infm3lem  9891  supmul1  9898  supmullem2  9900  supmul  9901  infmrcl  9912  cju  9921  nn2ge  9950  nominpos  10129  zdiv  10265  btwnz  10297  uzwo  10464  uzwoOLD  10465  uzinfmi  10480  ublbneg  10485  lbzbi  10489  zsupss  10490  uzsupss  10493  zq  10505  rpnnen1lem1  10525  rpnnen1lem2  10526  rpnnen1lem3  10527  rpnnen1lem4  10528  rpnnen1lem5  10529  z2ge  10709  qbtwnre  10710  qbtwnxr  10711  xralrple  10716  xrsupsslem  10810  xrinfmsslem  10811  supxrpnf  10822  icc0  10889  iccsupr  10922  flval3  11142  uzsup  11164  fsequb  11234  expnbnd  11428  expmulnbnd  11431  hashkf  11540  hashdom  11573  iswrdi  11651  shftlem  11803  shftfval  11805  sqrlem3  11970  01sqrex  11975  resqrex  11976  sqrneg  11993  abs1m  12059  rexanuz  12069  rexanre  12070  rexuz3  12072  rexuzre  12076  rexico  12077  caubnd2  12081  caubnd  12082  sqreu  12084  rlim2lt  12211  rlim3  12212  lo1bdd2  12238  lo1bddrp  12239  o1lo1  12251  climconst  12257  rlimconst  12258  rlimclim1  12259  climshftlem  12288  rlimcn2  12304  reccn2  12310  cn1lem  12311  rlimo1  12330  o1rlimmul  12332  lo1add  12340  lo1mul  12341  lo1le  12365  isercoll  12381  isercoll2  12382  caucvgrlem  12386  serf0  12394  zsum  12432  fsum  12434  fsumcvg3  12443  climcnds  12551  divrcnv  12552  infcvgaux2i  12557  mertenslem1  12581  mertenslem2  12582  ruclem12  12760  dvdsval2  12775  dvds0lem  12780  dvds1lem  12781  dvds2lem  12782  odd2np1lem  12827  odd2np1  12828  divalglem9  12841  gcdcllem3  12933  bezoutlem1  12958  qredeu  13027  exprmfct  13030  isprm5  13032  maxprmfct  13033  odzcllem  13098  opeo  13107  omeo  13108  pythagtriplem19  13127  pcprmpw2  13175  pcprmpw  13176  pockthi  13195  infpnlem2  13199  prmreclem1  13204  prmreclem5  13208  prmreclem6  13209  1arithlem4  13214  vdwapun  13262  vdwlem1  13269  vdwlem2  13270  vdwlem6  13274  vdwlem8  13276  vdwlem10  13278  vdwlem13  13281  ramz  13313  ramub1lem1  13314  elrestr  13576  imasleval  13686  mreexexlem3d  13791  mreexexlem4d  13792  iscatd  13818  poslubd  14494  fpwipodrs  14510  spwpr4  14583  ismgmid2  14633  ismndd  14639  gsumvallem1  14691  gsumval2a  14702  gsumwspan  14711  isgrpd2  14748  isgrpd  14750  imasgrp2  14853  gaorber  15005  orbsta  15010  cayleyth  15033  odf1o2  15127  pgpfi1  15149  sylow1lem3  15154  sylow1lem5  15156  pgpfi  15159  pgpssslw  15168  sylow2alem2  15172  slwhash  15178  fislw  15179  lsmelvalm  15205  pj1id  15251  efgs1b  15288  efgrelexlemb  15302  efgredeu  15304  gexex  15388  cyggeninv  15413  0cyg  15422  lt6abl  15424  eldprdi  15496  pgpfac1lem3a  15554  pgpfac1lem3  15555  pgpfac1lem5  15557  pgpfaclem1  15559  pgpfaclem3  15561  ablfaclem2  15564  dvdsrmul  15673  dvdsr01  15680  irredrmul  15732  lss1d  15959  lspf  15970  lspval  15971  lssats2  15996  lspsn  15998  lspsneq  16114  lspfixed  16120  lspsolvlem  16134  lspprat  16145  lbsextlem2  16151  lpi0  16238  lpi1  16239  aspval  16307  zlpir  16687  zcyg  16688  zncyg  16745  znf1o  16748  cygznlem3  16766  cygth  16768  frgpcyg  16770  fiinbas  16933  topbas  16953  pptbas  16988  clsval  17017  clsval2  17030  elcls  17053  neiint  17084  neips  17093  opnneissb  17094  opnssneib  17095  innei  17105  neiptopnei  17112  restbas  17137  restcld  17151  restcldi  17152  restopnb  17154  neitr  17159  restcls  17160  ordtbas2  17170  ordtopn1  17173  ordtopn2  17174  leordtval2  17191  iocpnfordt  17194  icomnfordt  17195  lecldbas  17198  pnfnei  17199  mnfnei  17200  lmconst  17240  iscnp4  17242  cncnpi  17257  cnconst2  17262  cnprest  17268  cnpdis  17272  pnrmopn  17322  nrmsep  17336  regsep2  17355  cmpcovf  17369  cncmp  17370  fincmp  17371  cmpsublem  17377  cmpsub  17378  tgcmp  17379  cmpcld  17380  uncmp  17381  hauscmplem  17384  cmpfi  17386  consubclo  17401  concompid  17408  2ndci  17425  2ndcsb  17426  2ndc1stc  17428  1stcrest  17430  2ndcctbss  17432  2ndcdisj  17433  2ndcomap  17435  2ndcsep  17436  dis2ndc  17437  restlly  17460  islly2  17461  hausllycmp  17471  cldllycmp  17472  lly1stc  17473  dislly  17474  llycmpkgen2  17496  cmpkgen  17497  1stckgenlem  17499  elptr  17519  ptbasfi  17527  neitx  17553  ptpjopn  17558  txcnp  17566  ptcnplem  17567  txlly  17582  txnlly  17583  txtube  17586  txcmplem1  17587  txcmplem2  17588  tx1stc  17596  txkgen  17598  xkococnlem  17605  txcon  17635  tgqtop  17658  qtopeu  17662  kqreglem1  17687  kqreglem2  17688  kqnrmlem1  17689  kqnrmlem2  17690  reghmph  17739  nrmhmph  17740  fbssfi  17783  opnfbas  17788  isfil2  17802  fsubbas  17813  ssfg  17818  fgss2  17820  fbasrn  17830  filuni  17831  fgtr  17836  ssufl  17864  uffix  17867  elfm  17893  elfm2  17894  elfm3  17896  imaelfm  17897  rnelfmlem  17898  rnelfm  17899  fmfnfmlem3  17902  fmfnfmlem4  17903  fmfnfm  17904  fmco  17907  ufldom  17908  hausflim  17927  flimcls  17931  hauspwpwf1  17933  flffbas  17941  txflf  17952  fclscf  17971  fclsfnflim  17973  alexsubALTlem3  17994  alexsubALTlem4  17995  alexsubALT  17996  ptcmplem2  17998  ptcmplem3  17999  ptcmplem5  18001  tmdgsum2  18040  symgtgp  18045  subgntr  18050  opnsubg  18051  ghmcnp  18058  divstgpopn  18063  tsmsfbas  18071  tsmsgsum  18082  tsmsres  18087  tsmsxplem1  18096  tsmsxp  18098  ustexsym  18159  elrnust  18168  trust  18173  utoptop  18178  restutop  18181  restutopopn  18182  ustuqtop1  18185  ustuqtop2  18186  ustuqtop4  18188  ustuqtop5  18189  utopsnneiplem  18191  utopsnnei  18193  iducn  18227  fmucnd  18236  cfilufg  18237  trcfilu  18238  neipcfilu  18240  imasdsf1olem  18304  blss  18339  blssex  18340  ssblex  18341  blin2  18342  neibl  18414  blcld  18418  metss2  18425  stdbdmopn  18431  mopnex  18432  met1stc  18434  met2ndci  18435  metrest  18437  prdsxmslem2  18442  metcnp3  18453  metcnpi3  18459  metuval  18462  metustexhalf  18469  metustfbas  18470  cfilucfil  18472  restmetu  18482  metucn  18483  dscopn  18485  ngptgp  18541  nlmvscnlem1  18586  nrginvrcnlem  18590  nghmcn  18643  tgioo  18691  tgqioo  18695  xrsmopn  18707  zcld  18708  recld2  18709  zdis  18711  icccmplem1  18717  icccmplem2  18718  icccmplem3  18719  reconnlem2  18722  xmetdcn2  18732  metdscn  18750  addcnlem  18758  elcncf1di  18789  icoopnst  18828  iocopnst  18829  xrhmeo  18835  cnheibor  18844  cnllycmp  18845  lebnumlem3  18852  lebnum  18853  xlebnum  18854  lebnumii  18855  elpi1i  18935  ipcnlem1  19063  lmnn  19080  iscfil3  19090  cfilres  19113  flimcfil  19130  cncmet  19137  bcthlem4  19142  bcthlem5  19143  minveclem4c  19186  minveclem2  19187  minveclem3b  19189  minveclem3  19190  minveclem4  19193  minveclem6  19195  ivthlem2  19209  ivthlem3  19210  ivth  19211  ivthle  19213  ivthle2  19214  cniccbdd  19218  elovolmr  19232  ovolunlem1  19253  ovoliunlem1  19258  ovoliunlem2  19259  ovoliun2  19262  ovolicc1  19272  iundisj  19302  iunmbl2  19311  ioombl1lem4  19315  uniioombllem2  19335  uniioombllem3  19337  uniioombllem6  19340  dyadmbllem  19351  volcn  19358  volivth  19359  vitalilem2  19361  mbfinf  19417  mbflimsup  19418  i1faddlem  19445  i1fmullem  19446  itg1addlem4  19451  i1fmulc  19455  itg1climres  19466  itg2lr  19482  itg2monolem1  19502  itg2i1fseq  19507  itg2i1fseq2  19508  itg2cnlem1  19513  itg2cnlem2  19514  limcnlp  19625  ellimc3  19626  limcflf  19628  limciun  19641  dveflem  19723  rollelem  19733  c1lip1  19741  lhop1lem  19757  evlseu  19797  ply1divex  19919  ig1peu  19954  ply1lpir  19961  elply2  19975  plyeq0lem  19989  coeeq  20006  plydivlem3  20072  plydivlem4  20073  elqaalem3  20098  qaa  20100  iaa  20102  aareccl  20103  aannenlem2  20106  aalioulem2  20110  aalioulem3  20111  aalioulem5  20113  aalioulem6  20114  aaliou  20115  aaliou2  20117  aaliou3lem8  20122  ulmshftlem  20165  ulmbdd  20174  mtestbdd  20181  iblulm  20183  abelthlem8  20215  reeff1o  20223  pilem2  20228  pilem3  20229  efif1olem2  20305  eflogeq  20356  divlogrlim  20386  efopn  20409  cxpcn3lem  20491  cxpeq  20501  angpieqvd  20532  dcubic2  20544  quart  20561  rlimcnp  20664  xrlimcnp  20667  cxplim  20670  cxploglim  20676  emcllem6  20699  ftalem1  20715  ftalem2  20716  ftalem3  20717  ftalem5  20719  ftalem7  20721  isppw2  20758  sgmnncl  20790  dvdsppwf1o  20831  musum  20836  dvdsmulf1o  20839  perfect  20875  dchrptlem1  20908  dchrptlem2  20909  dchrpt  20911  bpos1lem  20926  lgsqrlem4  20988  lgsdchrval  20991  lgsquadlem1  20998  2sqlem2  21008  mul2sq  21009  2sqlem3  21010  2sqlem9  21017  2sqlem10  21018  2sqblem  21021  dchrisumlem3  21045  dchrisum0  21074  chpdifbndlem2  21108  pntrsumbnd2  21121  pntpbnd1  21140  pntpbnd2  21141  pntpbnd  21142  pntibndlem2  21145  pntibndlem3  21146  pntleme  21162  pntlem3  21163  ostth2  21191  ostth3  21192  umgraex  21218  cusgrares  21340  usgrasscusgra  21351  eupa0  21537  eupares  21538  eupap1  21539  lpni  21608  isgrpo  21625  isgrpoi  21627  grpoinvf  21669  isgrpda  21726  isgrpod  21727  isablod  21729  opidon  21751  ghgrp  21797  isrngod  21808  cnrngo  21832  rngmgmbs4  21846  vacn  22031  nmcvcn  22032  smcnlem  22034  nmosetn0  22107  nmoolb  22113  nmobndi  22117  nmoo0  22133  nmlno0lem  22135  isblo3i  22143  blo3i  22144  blocnilem  22146  blocni  22147  ubthlem1  22213  ubthlem2  22214  ubthlem3  22215  minvecolem2  22218  minvecolem3  22219  minvecolem4c  22222  minvecolem4  22223  minvecolem5  22224  minvecolem6  22225  htthlem  22261  norm1exi  22593  occl  22647  shsel3  22658  spanval  22676  spancl  22679  shsval2i  22730  pjhthlem2  22735  ococin  22751  h1de2ctlem  22898  spansncol  22911  pjoml6i  22932  nmopsetn0  23209  nmfnsetn0  23222  nmoplb  23251  nmfnlb  23268  0cnop  23323  0cnfn  23324  idcnop  23325  nmop0  23330  nmfn0  23331  nmlnop0iALT  23339  nmopun  23358  nmcexi  23370  lnconi  23377  lnopcnbd  23380  lnfncnbd  23401  riesz3i  23406  riesz1  23409  cnlnadjlem2  23412  cnlnadjlem8  23418  cnlnadjlem9  23419  adjbd1o  23429  branmfn  23449  opsqrlem1  23484  pjnmopi  23492  strlem1  23594  stri  23601  hstri  23609  cvcon3  23628  cvnbtwn  23630  superpos  23698  shatomici  23702  atcvat4i  23741  mdsymlem2  23748  cdj1i  23777  cdj3lem2  23779  cdj3i  23785  rexunirn  23815  iundisjf  23865  elunirn2  23898  ssnnssfz  23977  iundisjfi  23983  xreceu  23999  rexdiv  24003  rhmdvdsr  24065  tpr2rico  24107  rge0scvg  24132  pnfneige0  24133  qqhcn  24167  qqhucn  24168  rrhre  24176  indf1ofs  24212  gsumesum  24240  esumcst  24244  esumpcvgval  24257  dmsigagen  24316  dya2icoseg  24414  dya2iocnrect  24418  dya2iocuni  24420  sxbrsigalem2  24423  dstfrvunirn  24504  ballotlem4  24528  ballotlemic  24536  ballotlem1c  24537  ballotlemrc  24560  lgambdd  24593  subfacp1lem3  24640  erdsze2lem2  24662  cnpcon  24689  txpcon  24691  ptpcon  24692  indispcon  24693  conpcon  24694  cvxpcon  24701  cnllyscon  24704  cvmsss2  24733  cvmcov2  24734  cvmopnlem  24737  cvmfolem  24738  cvmliftlem14  24756  cvmliftlem15  24757  cvmlift2lem11  24772  cvmlift2lem12  24773  cvmlift2lem13  24774  cvmlift3lem2  24779  cvmlift3lem6  24783  cvmlift3lem9  24786  rtrclreclem.refl  24916  rtrclreclem.subset  24917  rtrclreclem.trans  24918  dedekind  24959  dedekindle  24960  ntrivcvgn0  24998  ntrivcvgmullem  25001  zprod  25035  fprod  25039  fprodntriv  25040  fprodser  25047  br8  25130  br6  25131  br4  25132  dfon2lem9  25164  trpredtr  25250  dftrpred3g  25253  frmin  25259  poseq  25270  frrlem5e  25306  elno2  25325  sltval2  25327  noreson  25331  sltres  25335  noxpsgn  25336  bdayfo  25346  nodenselem3  25354  nodenselem6  25357  nodense  25360  nobndlem2  25364  nobndlem4  25366  nobndlem6  25368  nobndlem8  25370  nobndup  25371  nobnddown  25372  nofulllem4  25376  nofulllem5  25377  fobigcup  25457  brbtwn  25545  brcgr  25546  brbtwn2  25551  axpasch  25587  axlowdimlem14  25601  axlowdim2  25606  axcontlem2  25611  axcontlem4  25613  axcontlem7  25616  axcontlem8  25617  axcontlem10  25619  axcontlem12  25621  fvtransport  25673  brcolinear  25700  brsegle  25749  seglerflx  25753  seglemin  25754  btwnsegle  25758  fvray  25782  fvline  25785  hilbert1.1  25795  elhf2  25823  0hf  25825  onsucsuccmpi  25900  limsucncmpi  25902  supaddc  25940  supadd  25941  volsupnfl  25949  itg2addnclem  25950  itg2addnclem2  25951  itg2addnc  25952  nn0prpwlem  26009  nn0prpw  26010  opnregcld  26017  cldregopn  26018  fness  26046  ssref  26047  fneref  26048  refref  26049  fnessref  26057  refssfne  26058  finlocfin  26063  locfindis  26069  comppfsc  26071  neibastop2lem  26073  fnemeet1  26079  tailfb  26090  filnetlem4  26094  unirep  26098  cover2  26099  indexa  26119  frinfm  26121  sdclem1  26131  fdc  26133  incsequz  26136  caushft  26151  istotbnd3  26164  0totbnd  26166  sstotbnd2  26167  sstotbnd  26168  sstotbnd3  26169  isbnd2  26176  isbnd3  26177  ssbnd  26181  totbndbnd  26182  equivbnd  26183  prdsbnd  26186  prdstotbnd  26187  cntotbnd  26189  heibor1lem  26202  heiborlem1  26204  heiborlem3  26206  heiborlem6  26209  heiborlem8  26211  heibor  26214  bfplem2  26216  rrncmslem  26225  iccbnd  26233  exidres  26237  isdrngo2  26258  igenval  26355  igenidl  26357  prnc  26361  prtlem10  26398  elrfi  26432  nacsfix  26450  mzpcompact2lem  26492  eldioph  26500  diophrw  26501  eldioph2b  26505  eldioph3  26508  diophin  26515  rexrabdioph  26538  rexzrexnn0  26548  eldioph4b  26556  eldioph4i  26557  rencldnfilem  26565  irrapxlem5  26573  irrapxlem6  26574  pell1234qrdich  26608  pell14qrdich  26616  infmrgelbi  26625  pellqrex  26626  pellfundre  26628  pellfundlb  26631  pellfund14  26645  rmxyelqirr  26657  rmxynorm  26665  congrep  26722  acongrep  26729  jm2.27  26763  fnwe2lem2  26810  islssfgi  26832  pwssplit1  26850  filnm  26854  frlmup4  26915  unxpwdom3  26918  islindf4  26970  lpirlnr  26983  hbtlem2  26990  hbtlem4  26992  hbtlem5  26994  hbt  26996  dgraaub  27015  mpaaeu  27017  aaitgo  27029  rgspnval  27035  rgspncl  27036  rngunsnply  27040  psgnunilem2  27080  psgnunilem3  27081  psgneldm2i  27090  psgnvalii  27094  dvconstbi  27213  ubelsupr  27352  climsuse  27395  stoweidlem9  27419  stoweidlem14  27424  stoweidlem18  27428  stoweidlem21  27431  stoweidlem29  27439  stoweidlem34  27444  stoweidlem35  27445  stoweidlem39  27449  stoweidlem41  27451  stoweidlem45  27455  stoweidlem52  27462  stoweidlem55  27465  stoweidlem57  27467  stoweidlem60  27470  stirlinglem5  27488  stirlinglem13  27496  stirlinglem14  27497  sigarcol  27515  lshpnel2N  29151  lsatlspsn2  29158  lsatlspsn  29159  lsmsat  29174  lssatomic  29177  lcvnbtwn  29191  lfl1  29236  eqlkr  29265  lshpkrlem1  29276  lshpkrex  29284  lfl1dim  29287  lfl1dim2N  29288  lkrss2N  29335  cvrcon3b  29443  glbconN  29542  cvrat4  29608  3dim3  29634  ps-2  29643  llni  29673  llnle  29683  lplni  29697  lplnle  29705  lplnexllnN  29729  lvoli  29740  atpointN  29908  lnatexN  29944  elpaddn0  29965  pclfinN  30065  ispsubcl2N  30112  lhprelat3N  30205  4atexlemex2  30236  4atex  30241  4atex2-0aOLDN  30243  4atex2-0cOLDN  30245  lautcvr  30257  cdleme0ex1N  30388  cdleme50rnlem  30709  cdleme50ex  30724  cdlemg1cex  30753  cdlemkid5  31100  cdlemk  31139  tendoex  31140  cdleml5N  31145  cdlemm10N  31284  dihglblem2aN  31459  dihglblem2N  31460  dih1dimatlem0  31494  dihatexv  31504  dihjat1lem  31594  dvh4dimat  31604  dvh3dim2  31614  dvh3dim3N  31615  dochfl1  31642  dochkr1  31644  dochkr1OLDN  31645  lcfl8  31668  lcfrvalsnN  31707  lcfrlem9  31716  lcfrlem27  31735  lcfrlem37  31745  lcfr  31751  mapdval2N  31796  mapdval4N  31798  mapd1o  31814  mapdcv  31826  mapdspex  31834  mapdpglem23  31860  hdmap11lem2  32011  hdmap14lem2a  32036  hdmap14lem6  32042
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-rex 2648  df-v 2894
  Copyright terms: Public domain W3C validator