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

Theorem rspcev 3020
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 3015 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 1721   E.wrex 2675
This theorem is referenced by:  rspc2ev  3028  rspc3ev  3030  reu6i  3093  rspesbca  3209  wefrc  4544  wereu2  4547  onfr  4588  ordunidif  4597  onssmin  4744  onminex  4754  onuninsuci  4787  elrnmpt1s  5085  dffv2  5763  elrnrexdm  5841  eldmrexrn  5843  foco2  5856  elabrex  5952  f1elima  5976  fcofo  5988  fliftfun  6001  fliftval  6005  f1oiso2  6039  fo1st  6333  fo2nd  6334  sorpssuni  6498  sorpssint  6499  onnseq  6573  tfrlem12  6617  seqomlem2  6675  oawordeulem  6764  oaass  6771  odi  6789  omass  6790  omeulem1  6792  oen0  6796  oeordi  6797  oelim2  6805  oeeulem  6811  nnawordex  6847  nneob  6862  ecelqsg  6926  resixpfo  7067  elixpsn  7068  ixpsnf1o  7069  boxcutc  7072  snfi  7154  onfin  7264  pssnn  7294  ssnnfi  7295  dif1enOLD  7307  dif1en  7308  findcard  7314  frfi  7319  fisupg  7322  nnsdomg  7333  unfi  7341  fofinf1o  7354  pwfilem  7367  fissuni  7377  fipreima  7378  finsschain  7379  indexfi  7380  elfir  7386  inelfi  7389  fiin  7393  marypha1lem  7404  eqsup  7425  supmaxlem  7433  fisup2g  7435  fisupcl  7436  supisoex  7440  wofib  7478  wemaplem2  7480  card2inf  7487  brwdom2  7505  cnfcom3clem  7626  trcl  7628  r1ordg  7668  r1pwss  7674  tz9.12lem3  7679  tz9.12  7680  r1elwf  7686  tcrank  7772  scottex  7773  scott0  7774  isnumi  7797  onsdom  7847  fseqdom  7871  ondomen  7882  infpwfien  7907  cardaleph  7934  cardalephex  7935  infenaleph  7936  alephfplem4  7952  alephfp2  7954  dfac2  7975  ackbij1lem18  8081  ackbij1  8082  cflem  8090  cflecard  8097  cfsuc  8101  cfflb  8103  cofsmo  8113  cfsmolem  8114  coftr  8117  fin23lem7  8160  fin23lem11  8161  enfin2i  8165  fin23lem26  8169  fin23lem38  8193  isf32lem5  8201  isf34lem4  8221  isfin1-3  8230  fin1a2lem7  8250  fin1a2lem11  8254  fin1a2lem13  8256  axdc3lem2  8295  axdc3lem4  8297  ttukeylem7  8359  iunfo  8378  ficard  8404  pwcfsdom  8422  fpwwe2lem12  8480  wunex  8578  eltsk2g  8590  grur1  8659  axgroth6  8667  inaprc  8675  nqereu  8770  archnq  8821  genpnmax  8848  ltexpri  8884  prlem936  8888  reclem3pr  8890  recexpr  8892  supexpr  8895  negexsr  8941  recexsrlem  8942  recexsr  8946  supsrlem  8950  axrnegex  9001  axrrecex  9002  axpre-sup  9008  1re  9054  cnegex  9211  cnegex2  9212  recex  9618  receu  9631  fimaxre2  9920  infm3lem  9930  supmul1  9937  supmullem2  9939  supmul  9940  infmrcl  9951  cju  9960  nn2ge  9989  nominpos  10168  zdiv  10304  btwnz  10336  uzwo  10503  uzwoOLD  10504  uzinfmi  10519  ublbneg  10524  lbzbi  10528  zsupss  10529  uzsupss  10532  zq  10544  rpnnen1lem1  10564  rpnnen1lem2  10565  rpnnen1lem3  10566  rpnnen1lem4  10567  rpnnen1lem5  10568  z2ge  10748  qbtwnre  10749  qbtwnxr  10750  xralrple  10755  xrsupsslem  10849  xrinfmsslem  10850  supxrpnf  10861  icc0  10928  iccsupr  10961  flval3  11185  uzsup  11207  fsequb  11277  expnbnd  11471  expmulnbnd  11474  hashkf  11583  hashdom  11616  iswrdi  11694  shftlem  11846  shftfval  11848  sqrlem3  12013  01sqrex  12018  resqrex  12019  sqrneg  12036  abs1m  12102  rexanuz  12112  rexanre  12113  rexuz3  12115  rexuzre  12119  rexico  12120  caubnd2  12124  caubnd  12125  sqreu  12127  rlim2lt  12254  rlim3  12255  lo1bdd2  12281  lo1bddrp  12282  o1lo1  12294  climconst  12300  rlimconst  12301  rlimclim1  12302  climshftlem  12331  rlimcn2  12347  reccn2  12353  cn1lem  12354  rlimo1  12373  o1rlimmul  12375  lo1add  12383  lo1mul  12384  lo1le  12408  isercoll  12424  isercoll2  12425  caucvgrlem  12429  serf0  12437  zsum  12475  fsum  12477  fsumcvg3  12486  climcnds  12594  divrcnv  12595  infcvgaux2i  12600  mertenslem1  12624  mertenslem2  12625  ruclem12  12803  dvdsval2  12818  dvds0lem  12823  dvds1lem  12824  dvds2lem  12825  odd2np1lem  12870  odd2np1  12871  divalglem9  12884  gcdcllem3  12976  bezoutlem1  13001  qredeu  13070  exprmfct  13073  isprm5  13075  maxprmfct  13076  odzcllem  13141  opeo  13150  omeo  13151  pythagtriplem19  13170  pcprmpw2  13218  pcprmpw  13219  pockthi  13238  infpnlem2  13242  prmreclem1  13247  prmreclem5  13251  prmreclem6  13252  1arithlem4  13257  vdwapun  13305  vdwlem1  13312  vdwlem2  13313  vdwlem6  13317  vdwlem8  13319  vdwlem10  13321  vdwlem13  13324  ramz  13356  ramub1lem1  13357  elrestr  13619  imasleval  13729  mreexexlem3d  13834  mreexexlem4d  13835  iscatd  13861  poslubd  14537  fpwipodrs  14553  spwpr4  14626  ismgmid2  14676  ismndd  14682  gsumvallem1  14734  gsumval2a  14745  gsumwspan  14754  isgrpd2  14791  isgrpd  14793  imasgrp2  14896  gaorber  15048  orbsta  15053  cayleyth  15076  odf1o2  15170  pgpfi1  15192  sylow1lem3  15197  sylow1lem5  15199  pgpfi  15202  pgpssslw  15211  sylow2alem2  15215  slwhash  15221  fislw  15222  lsmelvalm  15248  pj1id  15294  efgs1b  15331  efgrelexlemb  15345  efgredeu  15347  gexex  15431  cyggeninv  15456  0cyg  15465  lt6abl  15467  eldprdi  15539  pgpfac1lem3a  15597  pgpfac1lem3  15598  pgpfac1lem5  15600  pgpfaclem1  15602  pgpfaclem3  15604  ablfaclem2  15607  dvdsrmul  15716  dvdsr01  15723  irredrmul  15775  lss1d  16002  lspf  16013  lspval  16014  lssats2  16039  lspsn  16041  lspsneq  16157  lspfixed  16163  lspsolvlem  16177  lspprat  16188  lbsextlem2  16194  lpi0  16281  lpi1  16282  aspval  16350  zlpir  16734  zcyg  16735  zncyg  16792  znf1o  16795  cygznlem3  16813  cygth  16815  frgpcyg  16817  fiinbas  16980  topbas  17000  pptbas  17035  clsval  17064  clsval2  17077  elcls  17100  neiint  17131  neips  17140  opnneissb  17141  opnssneib  17142  innei  17152  neiptopnei  17159  restbas  17184  restcld  17198  restcldi  17199  restopnb  17201  neitr  17206  restcls  17207  ordtbas2  17217  ordtopn1  17220  ordtopn2  17221  leordtval2  17238  iocpnfordt  17241  icomnfordt  17242  lecldbas  17245  pnfnei  17246  mnfnei  17247  lmconst  17287  iscnp4  17289  cncnpi  17304  cnconst2  17309  cnprest  17315  cnpdis  17319  pnrmopn  17369  nrmsep  17383  regsep2  17402  cmpcovf  17416  cncmp  17417  fincmp  17418  cmpsublem  17424  cmpsub  17425  tgcmp  17426  cmpcld  17427  uncmp  17428  hauscmplem  17431  cmpfi  17433  consubclo  17448  concompid  17455  2ndci  17472  2ndcsb  17473  2ndc1stc  17475  1stcrest  17477  2ndcctbss  17479  2ndcdisj  17480  2ndcomap  17482  2ndcsep  17483  dis2ndc  17484  restlly  17507  islly2  17508  hausllycmp  17518  cldllycmp  17519  lly1stc  17520  dislly  17521  llycmpkgen2  17543  cmpkgen  17544  1stckgenlem  17546  elptr  17566  ptbasfi  17574  neitx  17600  ptpjopn  17605  txcnp  17613  ptcnplem  17614  txlly  17629  txnlly  17630  txtube  17633  txcmplem1  17634  txcmplem2  17635  tx1stc  17643  txkgen  17645  xkococnlem  17652  txcon  17682  tgqtop  17705  qtopeu  17709  kqreglem1  17734  kqreglem2  17735  kqnrmlem1  17736  kqnrmlem2  17737  reghmph  17786  nrmhmph  17787  fbssfi  17830  opnfbas  17835  isfil2  17849  fsubbas  17860  ssfg  17865  fgss2  17867  fbasrn  17877  filuni  17878  fgtr  17883  ssufl  17911  uffix  17914  elfm  17940  elfm2  17941  elfm3  17943  imaelfm  17944  rnelfmlem  17945  rnelfm  17946  fmfnfmlem3  17949  fmfnfmlem4  17950  fmfnfm  17951  fmco  17954  ufldom  17955  hausflim  17974  flimcls  17978  hauspwpwf1  17980  flffbas  17988  txflf  17999  fclscf  18018  fclsfnflim  18020  alexsubALTlem3  18041  alexsubALTlem4  18042  alexsubALT  18043  ptcmplem2  18045  ptcmplem3  18046  ptcmplem5  18048  tmdgsum2  18087  symgtgp  18092  subgntr  18097  opnsubg  18098  ghmcnp  18105  divstgpopn  18110  tsmsfbas  18118  tsmsgsum  18129  tsmsres  18134  tsmsxplem1  18143  tsmsxp  18145  ustexsym  18206  elrnust  18215  trust  18220  utoptop  18225  restutop  18228  restutopopn  18229  ustuqtop1  18232  ustuqtop2  18233  ustuqtop4  18235  ustuqtop5  18236  utopsnneiplem  18238  utopsnnei  18240  iducn  18274  fmucnd  18283  cfilufg  18284  trcfilu  18285  neipcfilu  18287  imasdsf1olem  18364  blssps  18415  blss  18416  blssexps  18417  blssex  18418  ssblex  18419  blin2  18420  neibl  18492  blcld  18496  metss2  18503  stdbdmopn  18509  mopnex  18510  met1stc  18512  met2ndci  18513  metrest  18515  prdsxmslem2  18520  metcnp3  18531  metcnpi3  18537  metuvalOLD  18540  metuval  18541  metustexhalfOLD  18554  metustexhalf  18555  metustfbasOLD  18556  metustfbas  18557  cfilucfilOLD  18560  cfilucfil  18561  restmetu  18578  metucnOLD  18579  metucn  18580  dscopn  18582  ngptgp  18638  nlmvscnlem1  18683  nrginvrcnlem  18687  nghmcn  18740  tgioo  18788  tgqioo  18792  xrsmopn  18804  zcld  18805  recld2  18806  zdis  18808  icccmplem1  18814  icccmplem2  18815  icccmplem3  18816  reconnlem2  18819  xmetdcn2  18829  metdscn  18847  addcnlem  18855  elcncf1di  18886  icoopnst  18925  iocopnst  18926  xrhmeo  18932  cnheibor  18941  cnllycmp  18942  lebnumlem3  18949  lebnum  18950  xlebnum  18951  lebnumii  18952  elpi1i  19032  ipcnlem1  19160  lmnn  19177  iscfil3  19187  cfilres  19210  flimcfil  19227  cncmet  19236  bcthlem4  19241  bcthlem5  19242  minveclem4c  19287  minveclem2  19288  minveclem3b  19290  minveclem3  19291  minveclem4  19294  minveclem6  19296  ivthlem2  19310  ivthlem3  19311  ivth  19312  ivthle  19314  ivthle2  19315  cniccbdd  19319  elovolmr  19333  ovolunlem1  19354  ovoliunlem1  19359  ovoliunlem2  19360  ovoliun2  19363  ovolicc1  19373  iundisj  19403  iunmbl2  19412  ioombl1lem4  19416  uniioombllem2  19436  uniioombllem3  19438  uniioombllem6  19441  dyadmbllem  19452  volcn  19459  volivth  19460  vitalilem2  19462  mbfinf  19518  mbflimsup  19519  i1faddlem  19546  i1fmullem  19547  itg1addlem4  19552  i1fmulc  19556  itg1climres  19567  itg2lr  19583  itg2monolem1  19603  itg2i1fseq  19608  itg2i1fseq2  19609  itg2cnlem1  19614  itg2cnlem2  19615  limcnlp  19726  ellimc3  19727  limcflf  19729  limciun  19742  dveflem  19824  rollelem  19834  c1lip1  19842  lhop1lem  19858  evlseu  19898  ply1divex  20020  ig1peu  20055  ply1lpir  20062  elply2  20076  plyeq0lem  20090  coeeq  20107  plydivlem3  20173  plydivlem4  20174  elqaalem3  20199  qaa  20201  iaa  20203  aareccl  20204  aannenlem2  20207  aalioulem2  20211  aalioulem3  20212  aalioulem5  20214  aalioulem6  20215  aaliou  20216  aaliou2  20218  aaliou3lem8  20223  ulmshftlem  20266  ulmbdd  20275  mtestbdd  20282  iblulm  20284  abelthlem8  20316  reeff1o  20324  pilem2  20329  pilem3  20330  efif1olem2  20406  eflogeq  20457  divlogrlim  20487  efopn  20510  cxpcn3lem  20592  cxpeq  20602  angpieqvd  20633  dcubic2  20645  quart  20662  rlimcnp  20765  xrlimcnp  20768  cxplim  20771  cxploglim  20777  emcllem6  20800  ftalem1  20816  ftalem2  20817  ftalem3  20818  ftalem5  20820  ftalem7  20822  isppw2  20859  sgmnncl  20891  dvdsppwf1o  20932  musum  20937  dvdsmulf1o  20940  perfect  20976  dchrptlem1  21009  dchrptlem2  21010  dchrpt  21012  bpos1lem  21027  lgsqrlem4  21089  lgsdchrval  21092  lgsquadlem1  21099  2sqlem2  21109  mul2sq  21110  2sqlem3  21111  2sqlem9  21118  2sqlem10  21119  2sqblem  21122  dchrisumlem3  21146  dchrisum0  21175  chpdifbndlem2  21209  pntrsumbnd2  21222  pntpbnd1  21241  pntpbnd2  21242  pntpbnd  21243  pntibndlem2  21246  pntibndlem3  21247  pntleme  21263  pntlem3  21264  ostth2  21292  ostth3  21293  umgraex  21319  cusgrares  21442  usgrasscusgra  21453  eupa0  21657  eupares  21658  eupap1  21659  lpni  21728  isgrpo  21745  isgrpoi  21747  grpoinvf  21789  isgrpda  21846  isgrpod  21847  isablod  21849  opidon  21871  ghgrp  21917  isrngod  21928  cnrngo  21952  rngmgmbs4  21966  vacn  22151  nmcvcn  22152  smcnlem  22154  nmosetn0  22227  nmoolb  22233  nmobndi  22237  nmoo0  22253  nmlno0lem  22255  isblo3i  22263  blo3i  22264  blocnilem  22266  blocni  22267  ubthlem1  22333  ubthlem2  22334  ubthlem3  22335  minvecolem2  22338  minvecolem3  22339  minvecolem4c  22342  minvecolem4  22343  minvecolem5  22344  minvecolem6  22345  htthlem  22381  norm1exi  22713  occl  22767  shsel3  22778  spanval  22796  spancl  22799  shsval2i  22850  pjhthlem2  22855  ococin  22871  h1de2ctlem  23018  spansncol  23031  pjoml6i  23052  nmopsetn0  23329  nmfnsetn0  23342  nmoplb  23371  nmfnlb  23388  0cnop  23443  0cnfn  23444  idcnop  23445  nmop0  23450  nmfn0  23451  nmlnop0iALT  23459  nmopun  23478  nmcexi  23490  lnconi  23497  lnopcnbd  23500  lnfncnbd  23521  riesz3i  23526  riesz1  23529  cnlnadjlem2  23532  cnlnadjlem8  23538  cnlnadjlem9  23539  adjbd1o  23549  branmfn  23569  opsqrlem1  23604  pjnmopi  23612  strlem1  23714  stri  23721  hstri  23729  cvcon3  23748  cvnbtwn  23750  superpos  23818  shatomici  23822  atcvat4i  23861  mdsymlem2  23868  cdj1i  23897  cdj3lem2  23899  cdj3i  23905  rexunirn  23939  iundisjf  23990  elunirn2  24024  ssnnssfz  24109  iundisjfi  24113  xreceu  24129  rexdiv  24133  rhmdvdsr  24217  metidval  24246  pstmval  24251  tpr2rico  24271  rge0scvg  24296  pnfneige0  24297  qqhcn  24336  qqhucn  24337  rrhre  24348  indf1ofs  24384  gsumesum  24412  esumcst  24416  esumpcvgval  24429  dmsigagen  24488  dya2icoseg  24588  dya2iocnrect  24592  dya2iocuni  24594  sxbrsigalem2  24597  dstfrvunirn  24693  ballotlem4  24717  ballotlemic  24725  ballotlem1c  24726  ballotlemrc  24749  lgambdd  24782  subfacp1lem3  24829  erdsze2lem2  24851  cnpcon  24878  txpcon  24880  ptpcon  24881  indispcon  24882  conpcon  24883  cvxpcon  24890  cnllyscon  24893  cvmsss2  24922  cvmcov2  24923  cvmopnlem  24926  cvmfolem  24927  cvmliftlem14  24945  cvmliftlem15  24946  cvmlift2lem11  24961  cvmlift2lem12  24962  cvmlift2lem13  24963  cvmlift3lem2  24968  cvmlift3lem6  24972  cvmlift3lem9  24975  rtrclreclem.refl  25105  rtrclreclem.subset  25106  rtrclreclem.trans  25107  dedekind  25148  dedekindle  25149  ntrivcvgn0  25187  ntrivcvgmullem  25190  zprod  25224  fprod  25228  fprodntriv  25229  fprodser  25236  br8  25335  br6  25336  br4  25337  dfon2lem9  25369  trpredtr  25455  dftrpred3g  25458  frmin  25464  poseq  25475  frrlem5e  25511  elno2  25530  sltval2  25532  noreson  25536  sltres  25540  noxpsgn  25541  bdayfo  25551  nodenselem3  25559  nodenselem6  25562  nodense  25565  nobndlem2  25569  nobndlem4  25571  nobndlem6  25573  nobndlem8  25575  nobndup  25576  nobnddown  25577  nofulllem4  25581  nofulllem5  25582  fobigcup  25662  brbtwn  25750  brcgr  25751  brbtwn2  25756  axpasch  25792  axlowdimlem14  25806  axlowdim2  25811  axcontlem2  25816  axcontlem4  25818  axcontlem7  25821  axcontlem8  25822  axcontlem10  25824  axcontlem12  25826  fvtransport  25878  brcolinear  25905  brsegle  25954  seglerflx  25958  seglemin  25959  btwnsegle  25963  fvray  25987  fvline  25990  hilbert1.1  26000  elhf2  26028  0hf  26030  onsucsuccmpi  26105  limsucncmpi  26107  supaddc  26145  supadd  26146  mblfinlem  26151  mblfinlem2  26152  mblfinlem3  26153  ismblfin  26154  volsupnfl  26158  itg2addnclem  26163  itg2addnclem2  26164  itg2addnclem3  26165  itg2addnc  26166  nn0prpwlem  26223  nn0prpw  26224  opnregcld  26231  cldregopn  26232  fness  26260  ssref  26261  fneref  26262  refref  26263  fnessref  26271  refssfne  26272  finlocfin  26277  locfindis  26283  comppfsc  26285  neibastop2lem  26287  fnemeet1  26293  tailfb  26304  filnetlem4  26308  unirep  26312  cover2  26313  indexa  26333  frinfm  26335  sdclem1  26345  fdc  26347  incsequz  26350  caushft  26365  istotbnd3  26378  0totbnd  26380  sstotbnd2  26381  sstotbnd  26382  sstotbnd3  26383  isbnd2  26390  isbnd3  26391  ssbnd  26395  totbndbnd  26396  equivbnd  26397  prdsbnd  26400  prdstotbnd  26401  cntotbnd  26403  heibor1lem  26416  heiborlem1  26418  heiborlem3  26420  heiborlem6  26423  heiborlem8  26425  heibor  26428  bfplem2  26430  rrncmslem  26439  iccbnd  26447  exidres  26451  isdrngo2  26472  igenval  26569  igenidl  26571  prnc  26575  prtlem10  26612  elrfi  26646  nacsfix  26664  mzpcompact2lem  26706  eldioph  26714  diophrw  26715  eldioph2b  26719  eldioph3  26722  diophin  26729  rexrabdioph  26752  rexzrexnn0  26762  eldioph4b  26770  eldioph4i  26771  rencldnfilem  26779  irrapxlem5  26787  irrapxlem6  26788  pell1234qrdich  26822  pell14qrdich  26830  infmrgelbi  26839  pellqrex  26840  pellfundre  26842  pellfundlb  26845  pellfund14  26859  rmxyelqirr  26871  rmxynorm  26879  congrep  26936  acongrep  26943  jm2.27  26977  fnwe2lem2  27024  islssfgi  27046  pwssplit1  27064  filnm  27068  frlmup4  27129  unxpwdom3  27132  islindf4  27184  lpirlnr  27197  hbtlem2  27204  hbtlem4  27206  hbtlem5  27208  hbt  27210  dgraaub  27229  mpaaeu  27231  aaitgo  27243  rgspnval  27249  rgspncl  27250  rngunsnply  27254  psgnunilem2  27294  psgnunilem3  27295  psgneldm2i  27304  psgnvalii  27308  dvconstbi  27427  ubelsupr  27566  climsuse  27609  stoweidlem9  27633  stoweidlem14  27638  stoweidlem18  27642  stoweidlem21  27645  stoweidlem29  27653  stoweidlem34  27658  stoweidlem35  27659  stoweidlem39  27663  stoweidlem41  27665  stoweidlem45  27669  stoweidlem52  27676  stoweidlem55  27679  stoweidlem57  27681  stoweidlem60  27684  stirlinglem5  27702  stirlinglem13  27710  stirlinglem14  27711  sigarcol  27729  lshpnel2N  29480  lsatlspsn2  29487  lsatlspsn  29488  lsmsat  29503  lssatomic  29506  lcvnbtwn  29520  lfl1  29565  eqlkr  29594  lshpkrlem1  29605  lshpkrex  29613  lfl1dim  29616  lfl1dim2N  29617  lkrss2N  29664  cvrcon3b  29772  glbconN  29871  cvrat4  29937  3dim3  29963  ps-2  29972  llni  30002  llnle  30012  lplni  30026  lplnle  30034  lplnexllnN  30058  lvoli  30069  atpointN  30237  lnatexN  30273  elpaddn0  30294  pclfinN  30394  ispsubcl2N  30441  lhprelat3N  30534  4atexlemex2  30565  4atex  30570  4atex2-0aOLDN  30572  4atex2-0cOLDN  30574  lautcvr  30586  cdleme0ex1N  30717  cdleme50rnlem  31038  cdleme50ex  31053  cdlemg1cex  31082  cdlemkid5  31429  cdlemk  31468  tendoex  31469  cdleml5N  31474  cdlemm10N  31613  dihglblem2aN  31788  dihglblem2N  31789  dih1dimatlem0  31823  dihatexv  31833  dihjat1lem  31923  dvh4dimat  31933  dvh3dim2  31943  dvh3dim3N  31944  dochfl1  31971  dochkr1  31973  dochkr1OLDN  31974  lcfl8  31997  lcfrvalsnN  32036  lcfrlem9  32045  lcfrlem27  32064  lcfrlem37  32074  lcfr  32080  mapdval2N  32125  mapdval4N  32127  mapd1o  32143  mapdcv  32155  mapdspex  32163  mapdpglem23  32189  hdmap11lem2  32340  hdmap14lem2a  32365  hdmap14lem6  32371
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-rex 2680  df-v 2926
  Copyright terms: Public domain W3C validator