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

Theorem rspcev 3012
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 3007 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 2667
This theorem is referenced by:  rspc2ev  3020  rspc3ev  3022  reu6i  3085  rspesbca  3201  wefrc  4536  wereu2  4539  onfr  4580  ordunidif  4589  onssmin  4736  onminex  4746  onuninsuci  4779  elrnmpt1s  5077  dffv2  5755  elrnrexdm  5833  eldmrexrn  5835  foco2  5848  elabrex  5944  f1elima  5968  fcofo  5980  fliftfun  5993  fliftval  5997  f1oiso2  6031  fo1st  6325  fo2nd  6326  sorpssuni  6490  sorpssint  6491  onnseq  6565  tfrlem12  6609  seqomlem2  6667  oawordeulem  6756  oaass  6763  odi  6781  omass  6782  omeulem1  6784  oen0  6788  oeordi  6789  oelim2  6797  oeeulem  6803  nnawordex  6839  nneob  6854  ecelqsg  6918  resixpfo  7059  elixpsn  7060  ixpsnf1o  7061  boxcutc  7064  snfi  7146  onfin  7256  pssnn  7286  ssnnfi  7287  dif1enOLD  7299  dif1en  7300  findcard  7306  frfi  7311  fisupg  7314  nnsdomg  7325  unfi  7333  fofinf1o  7346  pwfilem  7359  fissuni  7369  fipreima  7370  finsschain  7371  indexfi  7372  elfir  7378  inelfi  7381  fiin  7385  marypha1lem  7396  eqsup  7417  supmaxlem  7425  fisup2g  7427  fisupcl  7428  supisoex  7432  wofib  7470  wemaplem2  7472  card2inf  7479  brwdom2  7497  cnfcom3clem  7618  trcl  7620  r1ordg  7660  r1pwss  7666  tz9.12lem3  7671  tz9.12  7672  r1elwf  7678  tcrank  7764  scottex  7765  scott0  7766  isnumi  7789  onsdom  7839  fseqdom  7863  ondomen  7874  infpwfien  7899  cardaleph  7926  cardalephex  7927  infenaleph  7928  alephfplem4  7944  alephfp2  7946  dfac2  7967  ackbij1lem18  8073  ackbij1  8074  cflem  8082  cflecard  8089  cfsuc  8093  cfflb  8095  cofsmo  8105  cfsmolem  8106  coftr  8109  fin23lem7  8152  fin23lem11  8153  enfin2i  8157  fin23lem26  8161  fin23lem38  8185  isf32lem5  8193  isf34lem4  8213  isfin1-3  8222  fin1a2lem7  8242  fin1a2lem11  8246  fin1a2lem13  8248  axdc3lem2  8287  axdc3lem4  8289  ttukeylem7  8351  iunfo  8370  ficard  8396  pwcfsdom  8414  fpwwe2lem12  8472  wunex  8570  eltsk2g  8582  grur1  8651  axgroth6  8659  inaprc  8667  nqereu  8762  archnq  8813  genpnmax  8840  ltexpri  8876  prlem936  8880  reclem3pr  8882  recexpr  8884  supexpr  8887  negexsr  8933  recexsrlem  8934  recexsr  8938  supsrlem  8942  axrnegex  8993  axrrecex  8994  axpre-sup  9000  1re  9046  cnegex  9203  cnegex2  9204  recex  9610  receu  9623  fimaxre2  9912  infm3lem  9922  supmul1  9929  supmullem2  9931  supmul  9932  infmrcl  9943  cju  9952  nn2ge  9981  nominpos  10160  zdiv  10296  btwnz  10328  uzwo  10495  uzwoOLD  10496  uzinfmi  10511  ublbneg  10516  lbzbi  10520  zsupss  10521  uzsupss  10524  zq  10536  rpnnen1lem1  10556  rpnnen1lem2  10557  rpnnen1lem3  10558  rpnnen1lem4  10559  rpnnen1lem5  10560  z2ge  10740  qbtwnre  10741  qbtwnxr  10742  xralrple  10747  xrsupsslem  10841  xrinfmsslem  10842  supxrpnf  10853  icc0  10920  iccsupr  10953  flval3  11177  uzsup  11199  fsequb  11269  expnbnd  11463  expmulnbnd  11466  hashkf  11575  hashdom  11608  iswrdi  11686  shftlem  11838  shftfval  11840  sqrlem3  12005  01sqrex  12010  resqrex  12011  sqrneg  12028  abs1m  12094  rexanuz  12104  rexanre  12105  rexuz3  12107  rexuzre  12111  rexico  12112  caubnd2  12116  caubnd  12117  sqreu  12119  rlim2lt  12246  rlim3  12247  lo1bdd2  12273  lo1bddrp  12274  o1lo1  12286  climconst  12292  rlimconst  12293  rlimclim1  12294  climshftlem  12323  rlimcn2  12339  reccn2  12345  cn1lem  12346  rlimo1  12365  o1rlimmul  12367  lo1add  12375  lo1mul  12376  lo1le  12400  isercoll  12416  isercoll2  12417  caucvgrlem  12421  serf0  12429  zsum  12467  fsum  12469  fsumcvg3  12478  climcnds  12586  divrcnv  12587  infcvgaux2i  12592  mertenslem1  12616  mertenslem2  12617  ruclem12  12795  dvdsval2  12810  dvds0lem  12815  dvds1lem  12816  dvds2lem  12817  odd2np1lem  12862  odd2np1  12863  divalglem9  12876  gcdcllem3  12968  bezoutlem1  12993  qredeu  13062  exprmfct  13065  isprm5  13067  maxprmfct  13068  odzcllem  13133  opeo  13142  omeo  13143  pythagtriplem19  13162  pcprmpw2  13210  pcprmpw  13211  pockthi  13230  infpnlem2  13234  prmreclem1  13239  prmreclem5  13243  prmreclem6  13244  1arithlem4  13249  vdwapun  13297  vdwlem1  13304  vdwlem2  13305  vdwlem6  13309  vdwlem8  13311  vdwlem10  13313  vdwlem13  13316  ramz  13348  ramub1lem1  13349  elrestr  13611  imasleval  13721  mreexexlem3d  13826  mreexexlem4d  13827  iscatd  13853  poslubd  14529  fpwipodrs  14545  spwpr4  14618  ismgmid2  14668  ismndd  14674  gsumvallem1  14726  gsumval2a  14737  gsumwspan  14746  isgrpd2  14783  isgrpd  14785  imasgrp2  14888  gaorber  15040  orbsta  15045  cayleyth  15068  odf1o2  15162  pgpfi1  15184  sylow1lem3  15189  sylow1lem5  15191  pgpfi  15194  pgpssslw  15203  sylow2alem2  15207  slwhash  15213  fislw  15214  lsmelvalm  15240  pj1id  15286  efgs1b  15323  efgrelexlemb  15337  efgredeu  15339  gexex  15423  cyggeninv  15448  0cyg  15457  lt6abl  15459  eldprdi  15531  pgpfac1lem3a  15589  pgpfac1lem3  15590  pgpfac1lem5  15592  pgpfaclem1  15594  pgpfaclem3  15596  ablfaclem2  15599  dvdsrmul  15708  dvdsr01  15715  irredrmul  15767  lss1d  15994  lspf  16005  lspval  16006  lssats2  16031  lspsn  16033  lspsneq  16149  lspfixed  16155  lspsolvlem  16169  lspprat  16180  lbsextlem2  16186  lpi0  16273  lpi1  16274  aspval  16342  zlpir  16726  zcyg  16727  zncyg  16784  znf1o  16787  cygznlem3  16805  cygth  16807  frgpcyg  16809  fiinbas  16972  topbas  16992  pptbas  17027  clsval  17056  clsval2  17069  elcls  17092  neiint  17123  neips  17132  opnneissb  17133  opnssneib  17134  innei  17144  neiptopnei  17151  restbas  17176  restcld  17190  restcldi  17191  restopnb  17193  neitr  17198  restcls  17199  ordtbas2  17209  ordtopn1  17212  ordtopn2  17213  leordtval2  17230  iocpnfordt  17233  icomnfordt  17234  lecldbas  17237  pnfnei  17238  mnfnei  17239  lmconst  17279  iscnp4  17281  cncnpi  17296  cnconst2  17301  cnprest  17307  cnpdis  17311  pnrmopn  17361  nrmsep  17375  regsep2  17394  cmpcovf  17408  cncmp  17409  fincmp  17410  cmpsublem  17416  cmpsub  17417  tgcmp  17418  cmpcld  17419  uncmp  17420  hauscmplem  17423  cmpfi  17425  consubclo  17440  concompid  17447  2ndci  17464  2ndcsb  17465  2ndc1stc  17467  1stcrest  17469  2ndcctbss  17471  2ndcdisj  17472  2ndcomap  17474  2ndcsep  17475  dis2ndc  17476  restlly  17499  islly2  17500  hausllycmp  17510  cldllycmp  17511  lly1stc  17512  dislly  17513  llycmpkgen2  17535  cmpkgen  17536  1stckgenlem  17538  elptr  17558  ptbasfi  17566  neitx  17592  ptpjopn  17597  txcnp  17605  ptcnplem  17606  txlly  17621  txnlly  17622  txtube  17625  txcmplem1  17626  txcmplem2  17627  tx1stc  17635  txkgen  17637  xkococnlem  17644  txcon  17674  tgqtop  17697  qtopeu  17701  kqreglem1  17726  kqreglem2  17727  kqnrmlem1  17728  kqnrmlem2  17729  reghmph  17778  nrmhmph  17779  fbssfi  17822  opnfbas  17827  isfil2  17841  fsubbas  17852  ssfg  17857  fgss2  17859  fbasrn  17869  filuni  17870  fgtr  17875  ssufl  17903  uffix  17906  elfm  17932  elfm2  17933  elfm3  17935  imaelfm  17936  rnelfmlem  17937  rnelfm  17938  fmfnfmlem3  17941  fmfnfmlem4  17942  fmfnfm  17943  fmco  17946  ufldom  17947  hausflim  17966  flimcls  17970  hauspwpwf1  17972  flffbas  17980  txflf  17991  fclscf  18010  fclsfnflim  18012  alexsubALTlem3  18033  alexsubALTlem4  18034  alexsubALT  18035  ptcmplem2  18037  ptcmplem3  18038  ptcmplem5  18040  tmdgsum2  18079  symgtgp  18084  subgntr  18089  opnsubg  18090  ghmcnp  18097  divstgpopn  18102  tsmsfbas  18110  tsmsgsum  18121  tsmsres  18126  tsmsxplem1  18135  tsmsxp  18137  ustexsym  18198  elrnust  18207  trust  18212  utoptop  18217  restutop  18220  restutopopn  18221  ustuqtop1  18224  ustuqtop2  18225  ustuqtop4  18227  ustuqtop5  18228  utopsnneiplem  18230  utopsnnei  18232  iducn  18266  fmucnd  18275  cfilufg  18276  trcfilu  18277  neipcfilu  18279  imasdsf1olem  18356  blssps  18407  blss  18408  blssexps  18409  blssex  18410  ssblex  18411  blin2  18412  neibl  18484  blcld  18488  metss2  18495  stdbdmopn  18501  mopnex  18502  met1stc  18504  met2ndci  18505  metrest  18507  prdsxmslem2  18512  metcnp3  18523  metcnpi3  18529  metuvalOLD  18532  metuval  18533  metustexhalfOLD  18546  metustexhalf  18547  metustfbasOLD  18548  metustfbas  18549  cfilucfilOLD  18552  cfilucfil  18553  restmetu  18570  metucnOLD  18571  metucn  18572  dscopn  18574  ngptgp  18630  nlmvscnlem1  18675  nrginvrcnlem  18679  nghmcn  18732  tgioo  18780  tgqioo  18784  xrsmopn  18796  zcld  18797  recld2  18798  zdis  18800  icccmplem1  18806  icccmplem2  18807  icccmplem3  18808  reconnlem2  18811  xmetdcn2  18821  metdscn  18839  addcnlem  18847  elcncf1di  18878  icoopnst  18917  iocopnst  18918  xrhmeo  18924  cnheibor  18933  cnllycmp  18934  lebnumlem3  18941  lebnum  18942  xlebnum  18943  lebnumii  18944  elpi1i  19024  ipcnlem1  19152  lmnn  19169  iscfil3  19179  cfilres  19202  flimcfil  19219  cncmet  19228  bcthlem4  19233  bcthlem5  19234  minveclem4c  19279  minveclem2  19280  minveclem3b  19282  minveclem3  19283  minveclem4  19286  minveclem6  19288  ivthlem2  19302  ivthlem3  19303  ivth  19304  ivthle  19306  ivthle2  19307  cniccbdd  19311  elovolmr  19325  ovolunlem1  19346  ovoliunlem1  19351  ovoliunlem2  19352  ovoliun2  19355  ovolicc1  19365  iundisj  19395  iunmbl2  19404  ioombl1lem4  19408  uniioombllem2  19428  uniioombllem3  19430  uniioombllem6  19433  dyadmbllem  19444  volcn  19451  volivth  19452  vitalilem2  19454  mbfinf  19510  mbflimsup  19511  i1faddlem  19538  i1fmullem  19539  itg1addlem4  19544  i1fmulc  19548  itg1climres  19559  itg2lr  19575  itg2monolem1  19595  itg2i1fseq  19600  itg2i1fseq2  19601  itg2cnlem1  19606  itg2cnlem2  19607  limcnlp  19718  ellimc3  19719  limcflf  19721  limciun  19734  dveflem  19816  rollelem  19826  c1lip1  19834  lhop1lem  19850  evlseu  19890  ply1divex  20012  ig1peu  20047  ply1lpir  20054  elply2  20068  plyeq0lem  20082  coeeq  20099  plydivlem3  20165  plydivlem4  20166  elqaalem3  20191  qaa  20193  iaa  20195  aareccl  20196  aannenlem2  20199  aalioulem2  20203  aalioulem3  20204  aalioulem5  20206  aalioulem6  20207  aaliou  20208  aaliou2  20210  aaliou3lem8  20215  ulmshftlem  20258  ulmbdd  20267  mtestbdd  20274  iblulm  20276  abelthlem8  20308  reeff1o  20316  pilem2  20321  pilem3  20322  efif1olem2  20398  eflogeq  20449  divlogrlim  20479  efopn  20502  cxpcn3lem  20584  cxpeq  20594  angpieqvd  20625  dcubic2  20637  quart  20654  rlimcnp  20757  xrlimcnp  20760  cxplim  20763  cxploglim  20769  emcllem6  20792  ftalem1  20808  ftalem2  20809  ftalem3  20810  ftalem5  20812  ftalem7  20814  isppw2  20851  sgmnncl  20883  dvdsppwf1o  20924  musum  20929  dvdsmulf1o  20932  perfect  20968  dchrptlem1  21001  dchrptlem2  21002  dchrpt  21004  bpos1lem  21019  lgsqrlem4  21081  lgsdchrval  21084  lgsquadlem1  21091  2sqlem2  21101  mul2sq  21102  2sqlem3  21103  2sqlem9  21110  2sqlem10  21111  2sqblem  21114  dchrisumlem3  21138  dchrisum0  21167  chpdifbndlem2  21201  pntrsumbnd2  21214  pntpbnd1  21233  pntpbnd2  21234  pntpbnd  21235  pntibndlem2  21238  pntibndlem3  21239  pntleme  21255  pntlem3  21256  ostth2  21284  ostth3  21285  umgraex  21311  cusgrares  21434  usgrasscusgra  21445  eupa0  21649  eupares  21650  eupap1  21651  lpni  21720  isgrpo  21737  isgrpoi  21739  grpoinvf  21781  isgrpda  21838  isgrpod  21839  isablod  21841  opidon  21863  ghgrp  21909  isrngod  21920  cnrngo  21944  rngmgmbs4  21958  vacn  22143  nmcvcn  22144  smcnlem  22146  nmosetn0  22219  nmoolb  22225  nmobndi  22229  nmoo0  22245  nmlno0lem  22247  isblo3i  22255  blo3i  22256  blocnilem  22258  blocni  22259  ubthlem1  22325  ubthlem2  22326  ubthlem3  22327  minvecolem2  22330  minvecolem3  22331  minvecolem4c  22334  minvecolem4  22335  minvecolem5  22336  minvecolem6  22337  htthlem  22373  norm1exi  22705  occl  22759  shsel3  22770  spanval  22788  spancl  22791  shsval2i  22842  pjhthlem2  22847  ococin  22863  h1de2ctlem  23010  spansncol  23023  pjoml6i  23044  nmopsetn0  23321  nmfnsetn0  23334  nmoplb  23363  nmfnlb  23380  0cnop  23435  0cnfn  23436  idcnop  23437  nmop0  23442  nmfn0  23443  nmlnop0iALT  23451  nmopun  23470  nmcexi  23482  lnconi  23489  lnopcnbd  23492  lnfncnbd  23513  riesz3i  23518  riesz1  23521  cnlnadjlem2  23524  cnlnadjlem8  23530  cnlnadjlem9  23531  adjbd1o  23541  branmfn  23561  opsqrlem1  23596  pjnmopi  23604  strlem1  23706  stri  23713  hstri  23721  cvcon3  23740  cvnbtwn  23742  superpos  23810  shatomici  23814  atcvat4i  23853  mdsymlem2  23860  cdj1i  23889  cdj3lem2  23891  cdj3i  23897  rexunirn  23931  iundisjf  23982  elunirn2  24016  ssnnssfz  24101  iundisjfi  24105  xreceu  24121  rexdiv  24125  rhmdvdsr  24209  metidval  24238  pstmval  24243  tpr2rico  24263  rge0scvg  24288  pnfneige0  24289  qqhcn  24328  qqhucn  24329  rrhre  24340  indf1ofs  24376  gsumesum  24404  esumcst  24408  esumpcvgval  24421  dmsigagen  24480  dya2icoseg  24580  dya2iocnrect  24584  dya2iocuni  24586  sxbrsigalem2  24589  dstfrvunirn  24685  ballotlem4  24709  ballotlemic  24717  ballotlem1c  24718  ballotlemrc  24741  lgambdd  24774  subfacp1lem3  24821  erdsze2lem2  24843  cnpcon  24870  txpcon  24872  ptpcon  24873  indispcon  24874  conpcon  24875  cvxpcon  24882  cnllyscon  24885  cvmsss2  24914  cvmcov2  24915  cvmopnlem  24918  cvmfolem  24919  cvmliftlem14  24937  cvmliftlem15  24938  cvmlift2lem11  24953  cvmlift2lem12  24954  cvmlift2lem13  24955  cvmlift3lem2  24960  cvmlift3lem6  24964  cvmlift3lem9  24967  rtrclreclem.refl  25097  rtrclreclem.subset  25098  rtrclreclem.trans  25099  dedekind  25140  dedekindle  25141  ntrivcvgn0  25179  ntrivcvgmullem  25182  zprod  25216  fprod  25220  fprodntriv  25221  fprodser  25228  br8  25327  br6  25328  br4  25329  dfon2lem9  25361  trpredtr  25447  dftrpred3g  25450  frmin  25456  poseq  25467  frrlem5e  25503  elno2  25522  sltval2  25524  noreson  25528  sltres  25532  noxpsgn  25533  bdayfo  25543  nodenselem3  25551  nodenselem6  25554  nodense  25557  nobndlem2  25561  nobndlem4  25563  nobndlem6  25565  nobndlem8  25567  nobndup  25568  nobnddown  25569  nofulllem4  25573  nofulllem5  25574  fobigcup  25654  brbtwn  25742  brcgr  25743  brbtwn2  25748  axpasch  25784  axlowdimlem14  25798  axlowdim2  25803  axcontlem2  25808  axcontlem4  25810  axcontlem7  25813  axcontlem8  25814  axcontlem10  25816  axcontlem12  25818  fvtransport  25870  brcolinear  25897  brsegle  25946  seglerflx  25950  seglemin  25951  btwnsegle  25955  fvray  25979  fvline  25982  hilbert1.1  25992  elhf2  26020  0hf  26022  onsucsuccmpi  26097  limsucncmpi  26099  supaddc  26137  supadd  26138  mblfinlem  26143  mblfinlem2  26144  mblfinlem3  26145  ismblfin  26146  volsupnfl  26150  itg2addnclem  26155  itg2addnclem2  26156  itg2addnclem3  26157  itg2addnc  26158  nn0prpwlem  26215  nn0prpw  26216  opnregcld  26223  cldregopn  26224  fness  26252  ssref  26253  fneref  26254  refref  26255  fnessref  26263  refssfne  26264  finlocfin  26269  locfindis  26275  comppfsc  26277  neibastop2lem  26279  fnemeet1  26285  tailfb  26296  filnetlem4  26300  unirep  26304  cover2  26305  indexa  26325  frinfm  26327  sdclem1  26337  fdc  26339  incsequz  26342  caushft  26357  istotbnd3  26370  0totbnd  26372  sstotbnd2  26373  sstotbnd  26374  sstotbnd3  26375  isbnd2  26382  isbnd3  26383  ssbnd  26387  totbndbnd  26388  equivbnd  26389  prdsbnd  26392  prdstotbnd  26393  cntotbnd  26395  heibor1lem  26408  heiborlem1  26410  heiborlem3  26412  heiborlem6  26415  heiborlem8  26417  heibor  26420  bfplem2  26422  rrncmslem  26431  iccbnd  26439  exidres  26443  isdrngo2  26464  igenval  26561  igenidl  26563  prnc  26567  prtlem10  26604  elrfi  26638  nacsfix  26656  mzpcompact2lem  26698  eldioph  26706  diophrw  26707  eldioph2b  26711  eldioph3  26714  diophin  26721  rexrabdioph  26744  rexzrexnn0  26754  eldioph4b  26762  eldioph4i  26763  rencldnfilem  26771  irrapxlem5  26779  irrapxlem6  26780  pell1234qrdich  26814  pell14qrdich  26822  infmrgelbi  26831  pellqrex  26832  pellfundre  26834  pellfundlb  26837  pellfund14  26851  rmxyelqirr  26863  rmxynorm  26871  congrep  26928  acongrep  26935  jm2.27  26969  fnwe2lem2  27016  islssfgi  27038  pwssplit1  27056  filnm  27060  frlmup4  27121  unxpwdom3  27124  islindf4  27176  lpirlnr  27189  hbtlem2  27196  hbtlem4  27198  hbtlem5  27200  hbt  27202  dgraaub  27221  mpaaeu  27223  aaitgo  27235  rgspnval  27241  rgspncl  27242  rngunsnply  27246  psgnunilem2  27286  psgnunilem3  27287  psgneldm2i  27296  psgnvalii  27300  dvconstbi  27419  ubelsupr  27558  climsuse  27601  stoweidlem9  27625  stoweidlem14  27630  stoweidlem18  27634  stoweidlem21  27637  stoweidlem29  27645  stoweidlem34  27650  stoweidlem35  27651  stoweidlem39  27655  stoweidlem41  27657  stoweidlem45  27661  stoweidlem52  27668  stoweidlem55  27671  stoweidlem57  27673  stoweidlem60  27676  stirlinglem5  27694  stirlinglem13  27702  stirlinglem14  27703  sigarcol  27721  lshpnel2N  29468  lsatlspsn2  29475  lsatlspsn  29476  lsmsat  29491  lssatomic  29494  lcvnbtwn  29508  lfl1  29553  eqlkr  29582  lshpkrlem1  29593  lshpkrex  29601  lfl1dim  29604  lfl1dim2N  29605  lkrss2N  29652  cvrcon3b  29760  glbconN  29859  cvrat4  29925  3dim3  29951  ps-2  29960  llni  29990  llnle  30000  lplni  30014  lplnle  30022  lplnexllnN  30046  lvoli  30057  atpointN  30225  lnatexN  30261  elpaddn0  30282  pclfinN  30382  ispsubcl2N  30429  lhprelat3N  30522  4atexlemex2  30553  4atex  30558  4atex2-0aOLDN  30560  4atex2-0cOLDN  30562  lautcvr  30574  cdleme0ex1N  30705  cdleme50rnlem  31026  cdleme50ex  31041  cdlemg1cex  31070  cdlemkid5  31417  cdlemk  31456  tendoex  31457  cdleml5N  31462  cdlemm10N  31601  dihglblem2aN  31776  dihglblem2N  31777  dih1dimatlem0  31811  dihatexv  31821  dihjat1lem  31911  dvh4dimat  31921  dvh3dim2  31931  dvh3dim3N  31932  dochfl1  31959  dochkr1  31961  dochkr1OLDN  31962  lcfl8  31985  lcfrvalsnN  32024  lcfrlem9  32033  lcfrlem27  32052  lcfrlem37  32062  lcfr  32068  mapdval2N  32113  mapdval4N  32115  mapd1o  32131  mapdcv  32143  mapdspex  32151  mapdpglem23  32177  hdmap11lem2  32328  hdmap14lem2a  32353  hdmap14lem6  32359
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 2385
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 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rex 2672  df-v 2918
  Copyright terms: Public domain W3C validator