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

Theorem rspcev 3054
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 1630 . 2  |-  F/ x ps
2 rspcv.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
31, 2rspce 3049 1  |-  ( ( A  e.  B  /\  ps )  ->  E. x  e.  B  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360    = wceq 1653    e. wcel 1726   E.wrex 2708
This theorem is referenced by:  rspc2ev  3062  rspc3ev  3064  reu6i  3127  rspesbca  3243  wefrc  4579  wereu2  4582  onfr  4623  ordunidif  4632  onssmin  4780  onminex  4790  onuninsuci  4823  elrnmpt1s  5121  dffv2  5799  elrnrexdm  5877  eldmrexrn  5879  foco2  5892  elabrex  5988  f1elima  6012  fcofo  6024  fliftfun  6037  fliftval  6041  f1oiso2  6075  fo1st  6369  fo2nd  6370  sorpssuni  6534  sorpssint  6535  onnseq  6609  tfrlem12  6653  seqomlem2  6711  oawordeulem  6800  oaass  6807  odi  6825  omass  6826  omeulem1  6828  oen0  6832  oeordi  6833  oelim2  6841  oeeulem  6847  nnawordex  6883  nneob  6898  ecelqsg  6962  resixpfo  7103  elixpsn  7104  ixpsnf1o  7105  boxcutc  7108  snfi  7190  onfin  7300  pssnn  7330  ssnnfi  7331  dif1enOLD  7343  dif1en  7344  findcard  7350  frfi  7355  fisupg  7358  nnsdomg  7369  unfi  7377  fofinf1o  7390  pwfilem  7404  fissuni  7414  fipreima  7415  finsschain  7416  indexfi  7417  elfir  7423  inelfi  7426  fiin  7430  marypha1lem  7441  eqsup  7464  supmaxlem  7472  fisup2g  7474  fisupcl  7475  supisoex  7479  wofib  7517  wemaplem2  7519  card2inf  7526  brwdom2  7544  cnfcom3clem  7665  trcl  7667  r1ordg  7707  r1pwss  7713  tz9.12lem3  7718  tz9.12  7719  r1elwf  7725  tcrank  7813  scottex  7814  scott0  7815  isnumi  7838  onsdom  7888  fseqdom  7912  ondomen  7923  infpwfien  7948  cardaleph  7975  cardalephex  7976  infenaleph  7977  alephfplem4  7993  alephfp2  7995  dfac2  8016  ackbij1lem18  8122  ackbij1  8123  cflem  8131  cflecard  8138  cfsuc  8142  cfflb  8144  cofsmo  8154  cfsmolem  8155  coftr  8158  fin23lem7  8201  fin23lem11  8202  enfin2i  8206  fin23lem26  8210  fin23lem38  8234  isf32lem5  8242  isf34lem4  8262  isfin1-3  8271  fin1a2lem7  8291  fin1a2lem11  8295  fin1a2lem13  8297  axdc3lem2  8336  axdc3lem4  8338  ttukeylem7  8400  iunfo  8419  ficard  8445  pwcfsdom  8463  fpwwe2lem12  8521  wunex  8619  eltsk2g  8631  grur1  8700  axgroth6  8708  inaprc  8716  nqereu  8811  archnq  8862  genpnmax  8889  ltexpri  8925  prlem936  8929  reclem3pr  8931  recexpr  8933  supexpr  8936  negexsr  8982  recexsrlem  8983  recexsr  8987  supsrlem  8991  axrnegex  9042  axrrecex  9043  axpre-sup  9049  1re  9095  cnegex  9252  cnegex2  9253  recex  9659  receu  9672  fimaxre2  9961  infm3lem  9971  supmul1  9978  supmullem2  9980  supmul  9981  infmrcl  9992  cju  10001  nn2ge  10030  nominpos  10209  zdiv  10345  btwnz  10377  uzwo  10544  uzwoOLD  10545  uzinfmi  10560  ublbneg  10565  lbzbi  10569  zsupss  10570  uzsupss  10573  zq  10585  rpnnen1lem1  10605  rpnnen1lem2  10606  rpnnen1lem3  10607  rpnnen1lem4  10608  rpnnen1lem5  10609  z2ge  10789  qbtwnre  10790  qbtwnxr  10791  xralrple  10796  xrsupsslem  10890  xrinfmsslem  10891  supxrpnf  10902  icc0  10969  iccsupr  11002  flval3  11227  uzsup  11249  fsequb  11319  expnbnd  11513  expmulnbnd  11516  hashkf  11625  hashdom  11658  iswrdi  11736  shftlem  11888  shftfval  11890  sqrlem3  12055  01sqrex  12060  resqrex  12061  sqrneg  12078  abs1m  12144  rexanuz  12154  rexanre  12155  rexuz3  12157  rexuzre  12161  rexico  12162  caubnd2  12166  caubnd  12167  sqreu  12169  rlim2lt  12296  rlim3  12297  lo1bdd2  12323  lo1bddrp  12324  o1lo1  12336  climconst  12342  rlimconst  12343  rlimclim1  12344  climshftlem  12373  rlimcn2  12389  reccn2  12395  cn1lem  12396  rlimo1  12415  o1rlimmul  12417  lo1add  12425  lo1mul  12426  lo1le  12450  isercoll  12466  isercoll2  12467  caucvgrlem  12471  serf0  12479  zsum  12517  fsum  12519  fsumcvg3  12528  climcnds  12636  divrcnv  12637  infcvgaux2i  12642  mertenslem1  12666  mertenslem2  12667  ruclem12  12845  dvdsval2  12860  dvds0lem  12865  dvds1lem  12866  dvds2lem  12867  odd2np1lem  12912  odd2np1  12913  divalglem9  12926  gcdcllem3  13018  bezoutlem1  13043  qredeu  13112  exprmfct  13115  isprm5  13117  maxprmfct  13118  odzcllem  13183  opeo  13192  omeo  13193  pythagtriplem19  13212  pcprmpw2  13260  pcprmpw  13261  pockthi  13280  infpnlem2  13284  prmreclem1  13289  prmreclem5  13293  prmreclem6  13294  1arithlem4  13299  vdwapun  13347  vdwlem1  13354  vdwlem2  13355  vdwlem6  13359  vdwlem8  13361  vdwlem10  13363  vdwlem13  13366  ramz  13398  ramub1lem1  13399  elrestr  13661  imasleval  13771  mreexexlem3d  13876  mreexexlem4d  13877  iscatd  13903  poslubd  14579  fpwipodrs  14595  spwpr4  14668  ismgmid2  14718  ismndd  14724  gsumvallem1  14776  gsumval2a  14787  gsumwspan  14796  isgrpd2  14833  isgrpd  14835  imasgrp2  14938  gaorber  15090  orbsta  15095  cayleyth  15118  odf1o2  15212  pgpfi1  15234  sylow1lem3  15239  sylow1lem5  15241  pgpfi  15244  pgpssslw  15253  sylow2alem2  15257  slwhash  15263  fislw  15264  lsmelvalm  15290  pj1id  15336  efgs1b  15373  efgrelexlemb  15387  efgredeu  15389  gexex  15473  cyggeninv  15498  0cyg  15507  lt6abl  15509  eldprdi  15581  pgpfac1lem3a  15639  pgpfac1lem3  15640  pgpfac1lem5  15642  pgpfaclem1  15644  pgpfaclem3  15646  ablfaclem2  15649  dvdsrmul  15758  dvdsr01  15765  irredrmul  15817  lss1d  16044  lspf  16055  lspval  16056  lssats2  16081  lspsn  16083  lspsneq  16199  lspfixed  16205  lspsolvlem  16219  lspprat  16230  lbsextlem2  16236  lpi0  16323  lpi1  16324  aspval  16392  zlpir  16776  zcyg  16777  zncyg  16834  znf1o  16837  cygznlem3  16855  cygth  16857  frgpcyg  16859  fiinbas  17022  topbas  17042  pptbas  17077  clsval  17106  clsval2  17119  elcls  17142  neiint  17173  neips  17182  opnneissb  17183  opnssneib  17184  innei  17194  neiptopnei  17201  restbas  17227  restcld  17241  restcldi  17242  restopnb  17244  neitr  17249  restcls  17250  ordtbas2  17260  ordtopn1  17263  ordtopn2  17264  leordtval2  17281  iocpnfordt  17284  icomnfordt  17285  lecldbas  17288  pnfnei  17289  mnfnei  17290  lmconst  17330  iscnp4  17332  cncnpi  17347  cnconst2  17352  cnprest  17358  cnpdis  17362  pnrmopn  17412  nrmsep  17426  regsep2  17445  cmpcovf  17459  cncmp  17460  fincmp  17461  cmpsublem  17467  cmpsub  17468  tgcmp  17469  cmpcld  17470  uncmp  17471  hauscmplem  17474  cmpfi  17476  consubclo  17492  concompid  17499  2ndci  17516  2ndcsb  17517  2ndc1stc  17519  1stcrest  17521  2ndcctbss  17523  2ndcdisj  17524  2ndcomap  17526  2ndcsep  17527  dis2ndc  17528  restlly  17551  islly2  17552  hausllycmp  17562  cldllycmp  17563  lly1stc  17564  dislly  17565  llycmpkgen2  17587  cmpkgen  17588  1stckgenlem  17590  elptr  17610  ptbasfi  17618  neitx  17644  ptpjopn  17649  txcnp  17657  ptcnplem  17658  txlly  17673  txnlly  17674  txtube  17677  txcmplem1  17678  txcmplem2  17679  tx1stc  17687  txkgen  17689  xkococnlem  17696  txcon  17726  tgqtop  17749  qtopeu  17753  kqreglem1  17778  kqreglem2  17779  kqnrmlem1  17780  kqnrmlem2  17781  reghmph  17830  nrmhmph  17831  fbssfi  17874  opnfbas  17879  isfil2  17893  fsubbas  17904  ssfg  17909  fgss2  17911  fbasrn  17921  filuni  17922  fgtr  17927  ssufl  17955  uffix  17958  elfm  17984  elfm2  17985  elfm3  17987  imaelfm  17988  rnelfmlem  17989  rnelfm  17990  fmfnfmlem3  17993  fmfnfmlem4  17994  fmfnfm  17995  fmco  17998  ufldom  17999  hausflim  18018  flimcls  18022  hauspwpwf1  18024  flffbas  18032  txflf  18043  fclscf  18062  fclsfnflim  18064  alexsubALTlem3  18085  alexsubALTlem4  18086  alexsubALT  18087  ptcmplem2  18089  ptcmplem3  18090  ptcmplem5  18092  tmdgsum2  18131  symgtgp  18136  subgntr  18141  opnsubg  18142  ghmcnp  18149  divstgpopn  18154  tsmsfbas  18162  tsmsgsum  18173  tsmsres  18178  tsmsxplem1  18187  tsmsxp  18189  ustexsym  18250  elrnust  18259  trust  18264  utoptop  18269  restutop  18272  restutopopn  18273  ustuqtop1  18276  ustuqtop2  18277  ustuqtop4  18279  ustuqtop5  18280  utopsnneiplem  18282  utopsnnei  18284  iducn  18318  fmucnd  18327  cfilufg  18328  trcfilu  18329  neipcfilu  18331  imasdsf1olem  18408  blssps  18459  blss  18460  blssexps  18461  blssex  18462  ssblex  18463  blin2  18464  neibl  18536  blcld  18540  metss2  18547  stdbdmopn  18553  mopnex  18554  met1stc  18556  met2ndci  18557  metrest  18559  prdsxmslem2  18564  metcnp3  18575  metcnpi3  18581  metuvalOLD  18584  metuval  18585  metustexhalfOLD  18598  metustexhalf  18599  metustfbasOLD  18600  metustfbas  18601  cfilucfilOLD  18604  cfilucfil  18605  restmetu  18622  metucnOLD  18623  metucn  18624  dscopn  18626  ngptgp  18682  nlmvscnlem1  18727  nrginvrcnlem  18731  nghmcn  18784  tgioo  18832  tgqioo  18836  xrsmopn  18848  zcld  18849  recld2  18850  zdis  18852  icccmplem1  18858  icccmplem2  18859  icccmplem3  18860  reconnlem2  18863  xmetdcn2  18873  metdscn  18891  addcnlem  18899  elcncf1di  18930  icoopnst  18969  iocopnst  18970  xrhmeo  18976  cnheibor  18985  cnllycmp  18986  lebnumlem3  18993  lebnum  18994  xlebnum  18995  lebnumii  18996  elpi1i  19076  ipcnlem1  19204  lmnn  19221  iscfil3  19231  cfilres  19254  flimcfil  19271  cncmet  19280  bcthlem4  19285  bcthlem5  19286  minveclem4c  19331  minveclem2  19332  minveclem3b  19334  minveclem3  19335  minveclem4  19338  minveclem6  19340  ivthlem2  19354  ivthlem3  19355  ivth  19356  ivthle  19358  ivthle2  19359  cniccbdd  19363  elovolmr  19377  ovolunlem1  19398  ovoliunlem1  19403  ovoliunlem2  19404  ovoliun2  19407  ovolicc1  19417  iundisj  19447  iunmbl2  19456  ioombl1lem4  19460  uniioombllem2  19480  uniioombllem3  19482  uniioombllem6  19485  dyadmbllem  19496  volcn  19503  volivth  19504  vitalilem2  19506  mbfinf  19560  mbflimsup  19561  i1faddlem  19588  i1fmullem  19589  itg1addlem4  19594  i1fmulc  19598  itg1climres  19609  itg2lr  19625  itg2monolem1  19645  itg2i1fseq  19650  itg2i1fseq2  19651  itg2cnlem1  19656  itg2cnlem2  19657  limcnlp  19770  ellimc3  19771  limcflf  19773  limciun  19786  dveflem  19868  rollelem  19878  c1lip1  19886  lhop1lem  19902  evlseu  19942  ply1divex  20064  ig1peu  20099  ply1lpir  20106  elply2  20120  plyeq0lem  20134  coeeq  20151  plydivlem3  20217  plydivlem4  20218  elqaalem3  20243  qaa  20245  iaa  20247  aareccl  20248  aannenlem2  20251  aalioulem2  20255  aalioulem3  20256  aalioulem5  20258  aalioulem6  20259  aaliou  20260  aaliou2  20262  aaliou3lem8  20267  ulmshftlem  20310  ulmbdd  20319  mtestbdd  20326  iblulm  20328  abelthlem8  20360  reeff1o  20368  pilem2  20373  pilem3  20374  efif1olem2  20450  eflogeq  20501  divlogrlim  20531  efopn  20554  cxpcn3lem  20636  cxpeq  20646  angpieqvd  20677  dcubic2  20689  quart  20706  rlimcnp  20809  xrlimcnp  20812  cxplim  20815  cxploglim  20821  emcllem6  20844  ftalem1  20860  ftalem2  20861  ftalem3  20862  ftalem5  20864  ftalem7  20866  isppw2  20903  sgmnncl  20935  dvdsppwf1o  20976  musum  20981  dvdsmulf1o  20984  perfect  21020  dchrptlem1  21053  dchrptlem2  21054  dchrpt  21056  bpos1lem  21071  lgsqrlem4  21133  lgsdchrval  21136  lgsquadlem1  21143  2sqlem2  21153  mul2sq  21154  2sqlem3  21155  2sqlem9  21162  2sqlem10  21163  2sqblem  21166  dchrisumlem3  21190  dchrisum0  21219  chpdifbndlem2  21253  pntrsumbnd2  21266  pntpbnd1  21285  pntpbnd2  21286  pntpbnd  21287  pntibndlem2  21290  pntibndlem3  21291  pntleme  21307  pntlem3  21308  ostth2  21336  ostth3  21337  umgraex  21363  cusgrares  21486  usgrasscusgra  21497  eupa0  21701  eupares  21702  eupap1  21703  lpni  21772  isgrpo  21789  isgrpoi  21791  grpoinvf  21833  isgrpda  21890  isgrpod  21891  isablod  21893  opidon  21915  ghgrp  21961  isrngod  21972  cnrngo  21996  rngmgmbs4  22010  vacn  22195  nmcvcn  22196  smcnlem  22198  nmosetn0  22271  nmoolb  22277  nmobndi  22281  nmoo0  22297  nmlno0lem  22299  isblo3i  22307  blo3i  22308  blocnilem  22310  blocni  22311  ubthlem1  22377  ubthlem2  22378  ubthlem3  22379  minvecolem2  22382  minvecolem3  22383  minvecolem4c  22386  minvecolem4  22387  minvecolem5  22388  minvecolem6  22389  htthlem  22425  norm1exi  22757  occl  22811  shsel3  22822  spanval  22840  spancl  22843  shsval2i  22894  pjhthlem2  22899  ococin  22915  h1de2ctlem  23062  spansncol  23075  pjoml6i  23096  nmopsetn0  23373  nmfnsetn0  23386  nmoplb  23415  nmfnlb  23432  0cnop  23487  0cnfn  23488  idcnop  23489  nmop0  23494  nmfn0  23495  nmlnop0iALT  23503  nmopun  23522  nmcexi  23534  lnconi  23541  lnopcnbd  23544  lnfncnbd  23565  riesz3i  23570  riesz1  23573  cnlnadjlem2  23576  cnlnadjlem8  23582  cnlnadjlem9  23583  adjbd1o  23593  branmfn  23613  opsqrlem1  23648  pjnmopi  23656  strlem1  23758  stri  23765  hstri  23773  cvcon3  23792  cvnbtwn  23794  superpos  23862  shatomici  23866  atcvat4i  23905  mdsymlem2  23912  cdj1i  23941  cdj3lem2  23943  cdj3i  23949  rexunirn  23983  iundisjf  24034  elunirn2  24068  ssnnssfz  24153  iundisjfi  24157  xreceu  24173  rexdiv  24177  rhmdvdsr  24261  metidval  24290  pstmval  24295  tpr2rico  24315  rge0scvg  24340  pnfneige0  24341  qqhcn  24380  qqhucn  24381  rrhre  24392  indf1ofs  24428  gsumesum  24456  esumcst  24460  esumpcvgval  24473  dmsigagen  24532  dya2icoseg  24632  dya2iocnrect  24636  dya2iocuni  24638  sxbrsigalem2  24641  dstfrvunirn  24737  ballotlem4  24761  ballotlemic  24769  ballotlem1c  24770  ballotlemrc  24793  lgambdd  24826  subfacp1lem3  24873  erdsze2lem2  24895  cnpcon  24922  txpcon  24924  ptpcon  24925  indispcon  24926  conpcon  24927  cvxpcon  24934  cnllyscon  24937  cvmsss2  24966  cvmcov2  24967  cvmopnlem  24970  cvmfolem  24971  cvmliftlem14  24989  cvmliftlem15  24990  cvmlift2lem11  25005  cvmlift2lem12  25006  cvmlift2lem13  25007  cvmlift3lem2  25012  cvmlift3lem6  25016  cvmlift3lem9  25019  rtrclreclem.refl  25149  rtrclreclem.subset  25150  rtrclreclem.trans  25151  dedekind  25192  dedekindle  25193  ntrivcvgn0  25231  ntrivcvgmullem  25234  zprod  25268  fprod  25272  fprodntriv  25273  fprodser  25280  br8  25384  br6  25385  br4  25386  dfon2lem9  25423  trpredtr  25513  dftrpred3g  25516  frmin  25522  poseq  25533  wzel  25580  wsuclem  25581  wsuclb  25584  frrlem5e  25595  elno2  25614  sltval2  25616  noreson  25620  sltres  25624  noxpsgn  25625  bdayfo  25635  nodenselem3  25643  nodenselem6  25646  nodense  25649  nobndlem2  25653  nobndlem4  25655  nobndlem6  25657  nobndlem8  25659  nobndup  25660  nobnddown  25661  nofulllem4  25665  nofulllem5  25666  fobigcup  25750  imagesset  25803  brbtwn  25843  brcgr  25844  brbtwn2  25849  axpasch  25885  axlowdimlem14  25899  axlowdim2  25904  axcontlem2  25909  axcontlem4  25911  axcontlem7  25914  axcontlem8  25915  axcontlem10  25917  axcontlem12  25919  fvtransport  25971  brcolinear  25998  brsegle  26047  seglerflx  26051  seglemin  26052  btwnsegle  26056  fvray  26080  fvline  26083  hilbert1.1  26093  elhf2  26121  0hf  26123  onsucsuccmpi  26198  limsucncmpi  26200  supaddc  26245  supadd  26246  heicant  26253  mblfinlem1  26255  mblfinlem2  26256  mblfinlem3  26257  mblfinlem4  26258  ismblfin  26259  volsupnfl  26263  dvtanlem  26268  itg2addnclem  26270  itg2addnclem2  26271  itg2addnclem3  26272  itg2addnc  26273  ftc1anclem5  26298  ftc1anc  26302  nn0prpwlem  26339  nn0prpw  26340  opnregcld  26347  cldregopn  26348  fness  26376  ssref  26377  fneref  26378  refref  26379  fnessref  26387  refssfne  26388  finlocfin  26393  locfindis  26399  comppfsc  26401  neibastop2lem  26403  fnemeet1  26409  tailfb  26420  filnetlem4  26424  unirep  26428  cover2  26429  indexa  26449  frinfm  26451  sdclem1  26461  fdc  26463  incsequz  26466  caushft  26481  istotbnd3  26494  0totbnd  26496  sstotbnd2  26497  sstotbnd  26498  sstotbnd3  26499  isbnd2  26506  isbnd3  26507  ssbnd  26511  totbndbnd  26512  equivbnd  26513  prdsbnd  26516  prdstotbnd  26517  cntotbnd  26519  heibor1lem  26532  heiborlem1  26534  heiborlem3  26536  heiborlem6  26539  heiborlem8  26541  heibor  26544  bfplem2  26546  rrncmslem  26555  iccbnd  26563  exidres  26567  isdrngo2  26588  igenval  26685  igenidl  26687  prnc  26691  prtlem10  26728  elrfi  26762  nacsfix  26780  mzpcompact2lem  26822  eldioph  26830  diophrw  26831  eldioph2b  26835  eldioph3  26838  diophin  26845  rexrabdioph  26868  rexzrexnn0  26878  eldioph4b  26886  eldioph4i  26887  rencldnfilem  26895  irrapxlem5  26903  irrapxlem6  26904  pell1234qrdich  26938  pell14qrdich  26946  infmrgelbi  26955  pellqrex  26956  pellfundre  26958  pellfundlb  26961  pellfund14  26975  rmxyelqirr  26987  rmxynorm  26995  congrep  27052  acongrep  27059  jm2.27  27093  fnwe2lem2  27140  islssfgi  27161  pwssplit1  27179  filnm  27183  frlmup4  27244  unxpwdom3  27247  islindf4  27299  lpirlnr  27312  hbtlem2  27319  hbtlem4  27321  hbtlem5  27323  hbt  27325  dgraaub  27344  mpaaeu  27346  aaitgo  27358  rgspnval  27364  rgspncl  27365  rngunsnply  27369  psgnunilem2  27409  psgnunilem3  27410  psgneldm2i  27419  psgnvalii  27423  dvconstbi  27542  ubelsupr  27681  climsuse  27724  stoweidlem9  27748  stoweidlem14  27753  stoweidlem18  27757  stoweidlem21  27760  stoweidlem29  27768  stoweidlem34  27773  stoweidlem35  27774  stoweidlem39  27778  stoweidlem41  27780  stoweidlem45  27784  stoweidlem52  27791  stoweidlem55  27794  stoweidlem57  27796  stoweidlem60  27799  stirlinglem5  27817  stirlinglem13  27825  stirlinglem14  27826  sigarcol  27844  reumodprminv  28261  modprm0  28262  cshw1v  28310  cshwssizesame  28322  lshpnel2N  29857  lsatlspsn2  29864  lsatlspsn  29865  lsmsat  29880  lssatomic  29883  lcvnbtwn  29897  lfl1  29942  eqlkr  29971  lshpkrlem1  29982  lshpkrex  29990  lfl1dim  29993  lfl1dim2N  29994  lkrss2N  30041  cvrcon3b  30149  glbconN  30248  cvrat4  30314  3dim3  30340  ps-2  30349  llni  30379  llnle  30389  lplni  30403  lplnle  30411  lplnexllnN  30435  lvoli  30446  atpointN  30614  lnatexN  30650  elpaddn0  30671  pclfinN  30771  ispsubcl2N  30818  lhprelat3N  30911  4atexlemex2  30942  4atex  30947  4atex2-0aOLDN  30949  4atex2-0cOLDN  30951  lautcvr  30963  cdleme0ex1N  31094  cdleme50rnlem  31415  cdleme50ex  31430  cdlemg1cex  31459  cdlemkid5  31806  cdlemk  31845  tendoex  31846  cdleml5N  31851  cdlemm10N  31990  dihglblem2aN  32165  dihglblem2N  32166  dih1dimatlem0  32200  dihatexv  32210  dihjat1lem  32300  dvh4dimat  32310  dvh3dim2  32320  dvh3dim3N  32321  dochfl1  32348  dochkr1  32350  dochkr1OLDN  32351  lcfl8  32374  lcfrvalsnN  32413  lcfrlem9  32422  lcfrlem27  32441  lcfrlem37  32451  lcfr  32457  mapdval2N  32502  mapdval4N  32504  mapd1o  32520  mapdcv  32532  mapdspex  32540  mapdpglem23  32566  hdmap11lem2  32717  hdmap14lem2a  32742  hdmap14lem6  32748
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rex 2713  df-v 2960
  Copyright terms: Public domain W3C validator