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

Theorem rspcev 3058
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 3053 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 1727   E.wrex 2712
This theorem is referenced by:  rspc2ev  3066  rspc3ev  3068  reu6i  3131  rspesbca  3257  wefrc  4605  wereu2  4608  onfr  4649  ordunidif  4658  onssmin  4806  onminex  4816  onuninsuci  4849  elrnmpt1s  5147  dffv2  5825  elrnrexdm  5903  eldmrexrn  5905  foco2  5918  elabrex  6014  f1elima  6038  fcofo  6050  fliftfun  6063  fliftval  6067  f1oiso2  6101  fo1st  6395  fo2nd  6396  sorpssuni  6560  sorpssint  6561  onnseq  6635  tfrlem12  6679  seqomlem2  6737  oawordeulem  6826  oaass  6833  odi  6851  omass  6852  omeulem1  6854  oen0  6858  oeordi  6859  oelim2  6867  oeeulem  6873  nnawordex  6909  nneob  6924  ecelqsg  6988  resixpfo  7129  elixpsn  7130  ixpsnf1o  7131  boxcutc  7134  snfi  7216  onfin  7326  pssnn  7356  ssnnfi  7357  dif1enOLD  7369  dif1en  7370  findcard  7376  frfi  7381  fisupg  7384  nnsdomg  7395  unfi  7403  fofinf1o  7416  pwfilem  7430  fissuni  7440  fipreima  7441  finsschain  7442  indexfi  7443  elfir  7449  inelfi  7452  fiin  7456  marypha1lem  7467  eqsup  7490  supmaxlem  7498  fisup2g  7500  fisupcl  7501  supisoex  7505  wofib  7543  wemaplem2  7545  card2inf  7552  brwdom2  7570  cnfcom3clem  7691  trcl  7693  r1ordg  7733  r1pwss  7739  tz9.12lem3  7744  tz9.12  7745  r1elwf  7751  tcrank  7839  scottex  7840  scott0  7841  isnumi  7864  onsdom  7914  fseqdom  7938  ondomen  7949  infpwfien  7974  cardaleph  8001  cardalephex  8002  infenaleph  8003  alephfplem4  8019  alephfp2  8021  dfac2  8042  ackbij1lem18  8148  ackbij1  8149  cflem  8157  cflecard  8164  cfsuc  8168  cfflb  8170  cofsmo  8180  cfsmolem  8181  coftr  8184  fin23lem7  8227  fin23lem11  8228  enfin2i  8232  fin23lem26  8236  fin23lem38  8260  isf32lem5  8268  isf34lem4  8288  isfin1-3  8297  fin1a2lem7  8317  fin1a2lem11  8321  fin1a2lem13  8323  axdc3lem2  8362  axdc3lem4  8364  ttukeylem7  8426  iunfo  8445  ficard  8471  pwcfsdom  8489  fpwwe2lem12  8547  wunex  8645  eltsk2g  8657  grur1  8726  axgroth6  8734  inaprc  8742  nqereu  8837  archnq  8888  genpnmax  8915  ltexpri  8951  prlem936  8955  reclem3pr  8957  recexpr  8959  supexpr  8962  negexsr  9008  recexsrlem  9009  recexsr  9013  supsrlem  9017  axrnegex  9068  axrrecex  9069  axpre-sup  9075  1re  9121  cnegex  9278  cnegex2  9279  recex  9685  receu  9698  fimaxre2  9987  infm3lem  9997  supmul1  10004  supmullem2  10006  supmul  10007  infmrcl  10018  cju  10027  nn2ge  10056  nominpos  10235  zdiv  10371  btwnz  10403  uzwo  10570  uzwoOLD  10571  uzinfmi  10586  ublbneg  10591  lbzbi  10595  zsupss  10596  uzsupss  10599  zq  10611  rpnnen1lem1  10631  rpnnen1lem2  10632  rpnnen1lem3  10633  rpnnen1lem4  10634  rpnnen1lem5  10635  z2ge  10815  qbtwnre  10816  qbtwnxr  10817  xralrple  10822  xrsupsslem  10916  xrinfmsslem  10917  supxrpnf  10928  icc0  10995  iccsupr  11028  flval3  11253  uzsup  11275  fsequb  11345  expnbnd  11539  expmulnbnd  11542  hashkf  11651  hashdom  11684  iswrdi  11762  shftlem  11914  shftfval  11916  sqrlem3  12081  01sqrex  12086  resqrex  12087  sqrneg  12104  abs1m  12170  rexanuz  12180  rexanre  12181  rexuz3  12183  rexuzre  12187  rexico  12188  caubnd2  12192  caubnd  12193  sqreu  12195  rlim2lt  12322  rlim3  12323  lo1bdd2  12349  lo1bddrp  12350  o1lo1  12362  climconst  12368  rlimconst  12369  rlimclim1  12370  climshftlem  12399  rlimcn2  12415  reccn2  12421  cn1lem  12422  rlimo1  12441  o1rlimmul  12443  lo1add  12451  lo1mul  12452  lo1le  12476  isercoll  12492  isercoll2  12493  caucvgrlem  12497  serf0  12505  zsum  12543  fsum  12545  fsumcvg3  12554  climcnds  12662  divrcnv  12663  infcvgaux2i  12668  mertenslem1  12692  mertenslem2  12693  ruclem12  12871  dvdsval2  12886  dvds0lem  12891  dvds1lem  12892  dvds2lem  12893  odd2np1lem  12938  odd2np1  12939  divalglem9  12952  gcdcllem3  13044  bezoutlem1  13069  qredeu  13138  exprmfct  13141  isprm5  13143  maxprmfct  13144  odzcllem  13209  opeo  13218  omeo  13219  pythagtriplem19  13238  pcprmpw2  13286  pcprmpw  13287  pockthi  13306  infpnlem2  13310  prmreclem1  13315  prmreclem5  13319  prmreclem6  13320  1arithlem4  13325  vdwapun  13373  vdwlem1  13380  vdwlem2  13381  vdwlem6  13385  vdwlem8  13387  vdwlem10  13389  vdwlem13  13392  ramz  13424  ramub1lem1  13425  elrestr  13687  imasleval  13797  mreexexlem3d  13902  mreexexlem4d  13903  iscatd  13929  poslubd  14605  fpwipodrs  14621  spwpr4  14694  ismgmid2  14744  ismndd  14750  gsumvallem1  14802  gsumval2a  14813  gsumwspan  14822  isgrpd2  14859  isgrpd  14861  imasgrp2  14964  gaorber  15116  orbsta  15121  cayleyth  15144  odf1o2  15238  pgpfi1  15260  sylow1lem3  15265  sylow1lem5  15267  pgpfi  15270  pgpssslw  15279  sylow2alem2  15283  slwhash  15289  fislw  15290  lsmelvalm  15316  pj1id  15362  efgs1b  15399  efgrelexlemb  15413  efgredeu  15415  gexex  15499  cyggeninv  15524  0cyg  15533  lt6abl  15535  eldprdi  15607  pgpfac1lem3a  15665  pgpfac1lem3  15666  pgpfac1lem5  15668  pgpfaclem1  15670  pgpfaclem3  15672  ablfaclem2  15675  dvdsrmul  15784  dvdsr01  15791  irredrmul  15843  lss1d  16070  lspf  16081  lspval  16082  lssats2  16107  lspsn  16109  lspsneq  16225  lspfixed  16231  lspsolvlem  16245  lspprat  16256  lbsextlem2  16262  lpi0  16349  lpi1  16350  aspval  16418  zlpir  16802  zcyg  16803  zncyg  16860  znf1o  16863  cygznlem3  16881  cygth  16883  frgpcyg  16885  fiinbas  17048  topbas  17068  pptbas  17103  clsval  17132  clsval2  17145  elcls  17168  neiint  17199  neips  17208  opnneissb  17209  opnssneib  17210  innei  17220  neiptopnei  17227  restbas  17253  restcld  17267  restcldi  17268  restopnb  17270  neitr  17275  restcls  17276  ordtbas2  17286  ordtopn1  17289  ordtopn2  17290  leordtval2  17307  iocpnfordt  17310  icomnfordt  17311  lecldbas  17314  pnfnei  17315  mnfnei  17316  lmconst  17356  iscnp4  17358  cncnpi  17373  cnconst2  17378  cnprest  17384  cnpdis  17388  pnrmopn  17438  nrmsep  17452  regsep2  17471  cmpcovf  17485  cncmp  17486  fincmp  17487  cmpsublem  17493  cmpsub  17494  tgcmp  17495  cmpcld  17496  uncmp  17497  hauscmplem  17500  cmpfi  17502  consubclo  17518  concompid  17525  2ndci  17542  2ndcsb  17543  2ndc1stc  17545  1stcrest  17547  2ndcctbss  17549  2ndcdisj  17550  2ndcomap  17552  2ndcsep  17553  dis2ndc  17554  restlly  17577  islly2  17578  hausllycmp  17588  cldllycmp  17589  lly1stc  17590  dislly  17591  llycmpkgen2  17613  cmpkgen  17614  1stckgenlem  17616  elptr  17636  ptbasfi  17644  neitx  17670  ptpjopn  17675  txcnp  17683  ptcnplem  17684  txlly  17699  txnlly  17700  txtube  17703  txcmplem1  17704  txcmplem2  17705  tx1stc  17713  txkgen  17715  xkococnlem  17722  txcon  17752  tgqtop  17775  qtopeu  17779  kqreglem1  17804  kqreglem2  17805  kqnrmlem1  17806  kqnrmlem2  17807  reghmph  17856  nrmhmph  17857  fbssfi  17900  opnfbas  17905  isfil2  17919  fsubbas  17930  ssfg  17935  fgss2  17937  fbasrn  17947  filuni  17948  fgtr  17953  ssufl  17981  uffix  17984  elfm  18010  elfm2  18011  elfm3  18013  imaelfm  18014  rnelfmlem  18015  rnelfm  18016  fmfnfmlem3  18019  fmfnfmlem4  18020  fmfnfm  18021  fmco  18024  ufldom  18025  hausflim  18044  flimcls  18048  hauspwpwf1  18050  flffbas  18058  txflf  18069  fclscf  18088  fclsfnflim  18090  alexsubALTlem3  18111  alexsubALTlem4  18112  alexsubALT  18113  ptcmplem2  18115  ptcmplem3  18116  ptcmplem5  18118  tmdgsum2  18157  symgtgp  18162  subgntr  18167  opnsubg  18168  ghmcnp  18175  divstgpopn  18180  tsmsfbas  18188  tsmsgsum  18199  tsmsres  18204  tsmsxplem1  18213  tsmsxp  18215  ustexsym  18276  elrnust  18285  trust  18290  utoptop  18295  restutop  18298  restutopopn  18299  ustuqtop1  18302  ustuqtop2  18303  ustuqtop4  18305  ustuqtop5  18306  utopsnneiplem  18308  utopsnnei  18310  iducn  18344  fmucnd  18353  cfilufg  18354  trcfilu  18355  neipcfilu  18357  imasdsf1olem  18434  blssps  18485  blss  18486  blssexps  18487  blssex  18488  ssblex  18489  blin2  18490  neibl  18562  blcld  18566  metss2  18573  stdbdmopn  18579  mopnex  18580  met1stc  18582  met2ndci  18583  metrest  18585  prdsxmslem2  18590  metcnp3  18601  metcnpi3  18607  metuvalOLD  18610  metuval  18611  metustexhalfOLD  18624  metustexhalf  18625  metustfbasOLD  18626  metustfbas  18627  cfilucfilOLD  18630  cfilucfil  18631  restmetu  18648  metucnOLD  18649  metucn  18650  dscopn  18652  ngptgp  18708  nlmvscnlem1  18753  nrginvrcnlem  18757  nghmcn  18810  tgioo  18858  tgqioo  18862  xrsmopn  18874  zcld  18875  recld2  18876  zdis  18878  icccmplem1  18884  icccmplem2  18885  icccmplem3  18886  reconnlem2  18889  xmetdcn2  18899  metdscn  18917  addcnlem  18925  elcncf1di  18956  icoopnst  18995  iocopnst  18996  xrhmeo  19002  cnheibor  19011  cnllycmp  19012  lebnumlem3  19019  lebnum  19020  xlebnum  19021  lebnumii  19022  elpi1i  19102  ipcnlem1  19230  lmnn  19247  iscfil3  19257  cfilres  19280  flimcfil  19297  cncmet  19306  bcthlem4  19311  bcthlem5  19312  minveclem4c  19357  minveclem2  19358  minveclem3b  19360  minveclem3  19361  minveclem4  19364  minveclem6  19366  ivthlem2  19380  ivthlem3  19381  ivth  19382  ivthle  19384  ivthle2  19385  cniccbdd  19389  elovolmr  19403  ovolunlem1  19424  ovoliunlem1  19429  ovoliunlem2  19430  ovoliun2  19433  ovolicc1  19443  iundisj  19473  iunmbl2  19482  ioombl1lem4  19486  uniioombllem2  19506  uniioombllem3  19508  uniioombllem6  19511  dyadmbllem  19522  volcn  19529  volivth  19530  vitalilem2  19532  mbfinf  19586  mbflimsup  19587  i1faddlem  19614  i1fmullem  19615  itg1addlem4  19620  i1fmulc  19624  itg1climres  19635  itg2lr  19651  itg2monolem1  19671  itg2i1fseq  19676  itg2i1fseq2  19677  itg2cnlem1  19682  itg2cnlem2  19683  limcnlp  19796  ellimc3  19797  limcflf  19799  limciun  19812  dveflem  19894  rollelem  19904  c1lip1  19912  lhop1lem  19928  evlseu  19968  ply1divex  20090  ig1peu  20125  ply1lpir  20132  elply2  20146  plyeq0lem  20160  coeeq  20177  plydivlem3  20243  plydivlem4  20244  elqaalem3  20269  qaa  20271  iaa  20273  aareccl  20274  aannenlem2  20277  aalioulem2  20281  aalioulem3  20282  aalioulem5  20284  aalioulem6  20285  aaliou  20286  aaliou2  20288  aaliou3lem8  20293  ulmshftlem  20336  ulmbdd  20345  mtestbdd  20352  iblulm  20354  abelthlem8  20386  reeff1o  20394  pilem2  20399  pilem3  20400  efif1olem2  20476  eflogeq  20527  divlogrlim  20557  efopn  20580  cxpcn3lem  20662  cxpeq  20672  angpieqvd  20703  dcubic2  20715  quart  20732  rlimcnp  20835  xrlimcnp  20838  cxplim  20841  cxploglim  20847  emcllem6  20870  ftalem1  20886  ftalem2  20887  ftalem3  20888  ftalem5  20890  ftalem7  20892  isppw2  20929  sgmnncl  20961  dvdsppwf1o  21002  musum  21007  dvdsmulf1o  21010  perfect  21046  dchrptlem1  21079  dchrptlem2  21080  dchrpt  21082  bpos1lem  21097  lgsqrlem4  21159  lgsdchrval  21162  lgsquadlem1  21169  2sqlem2  21179  mul2sq  21180  2sqlem3  21181  2sqlem9  21188  2sqlem10  21189  2sqblem  21192  dchrisumlem3  21216  dchrisum0  21245  chpdifbndlem2  21279  pntrsumbnd2  21292  pntpbnd1  21311  pntpbnd2  21312  pntpbnd  21313  pntibndlem2  21316  pntibndlem3  21317  pntleme  21333  pntlem3  21334  ostth2  21362  ostth3  21363  umgraex  21389  cusgrares  21512  usgrasscusgra  21523  eupa0  21727  eupares  21728  eupap1  21729  lpni  21798  isgrpo  21815  isgrpoi  21817  grpoinvf  21859  isgrpda  21916  isgrpod  21917  isablod  21919  opidon  21941  ghgrp  21987  isrngod  21998  cnrngo  22022  rngmgmbs4  22036  vacn  22221  nmcvcn  22222  smcnlem  22224  nmosetn0  22297  nmoolb  22303  nmobndi  22307  nmoo0  22323  nmlno0lem  22325  isblo3i  22333  blo3i  22334  blocnilem  22336  blocni  22337  ubthlem1  22403  ubthlem2  22404  ubthlem3  22405  minvecolem2  22408  minvecolem3  22409  minvecolem4c  22412  minvecolem4  22413  minvecolem5  22414  minvecolem6  22415  htthlem  22451  norm1exi  22783  occl  22837  shsel3  22848  spanval  22866  spancl  22869  shsval2i  22920  pjhthlem2  22925  ococin  22941  h1de2ctlem  23088  spansncol  23101  pjoml6i  23122  nmopsetn0  23399  nmfnsetn0  23412  nmoplb  23441  nmfnlb  23458  0cnop  23513  0cnfn  23514  idcnop  23515  nmop0  23520  nmfn0  23521  nmlnop0iALT  23529  nmopun  23548  nmcexi  23560  lnconi  23567  lnopcnbd  23570  lnfncnbd  23591  riesz3i  23596  riesz1  23599  cnlnadjlem2  23602  cnlnadjlem8  23608  cnlnadjlem9  23609  adjbd1o  23619  branmfn  23639  opsqrlem1  23674  pjnmopi  23682  strlem1  23784  stri  23791  hstri  23799  cvcon3  23818  cvnbtwn  23820  superpos  23888  shatomici  23892  atcvat4i  23931  mdsymlem2  23938  cdj1i  23967  cdj3lem2  23969  cdj3i  23975  rexunirn  24009  iundisjf  24060  elunirn2  24094  ssnnssfz  24179  iundisjfi  24183  xreceu  24199  rexdiv  24203  rhmdvdsr  24287  metidval  24316  pstmval  24321  tpr2rico  24341  rge0scvg  24366  pnfneige0  24367  qqhcn  24406  qqhucn  24407  rrhre  24418  indf1ofs  24454  gsumesum  24482  esumcst  24486  esumpcvgval  24499  dmsigagen  24558  dya2icoseg  24658  dya2iocnrect  24662  dya2iocuni  24664  sxbrsigalem2  24667  dstfrvunirn  24763  ballotlem4  24787  ballotlemic  24795  ballotlem1c  24796  ballotlemrc  24819  lgambdd  24852  subfacp1lem3  24899  erdsze2lem2  24921  cnpcon  24948  txpcon  24950  ptpcon  24951  indispcon  24952  conpcon  24953  cvxpcon  24960  cnllyscon  24963  cvmsss2  24992  cvmcov2  24993  cvmopnlem  24996  cvmfolem  24997  cvmliftlem14  25015  cvmliftlem15  25016  cvmlift2lem11  25031  cvmlift2lem12  25032  cvmlift2lem13  25033  cvmlift3lem2  25038  cvmlift3lem6  25042  cvmlift3lem9  25045  rtrclreclem.refl  25175  rtrclreclem.subset  25176  rtrclreclem.trans  25177  dedekind  25218  dedekindle  25219  ntrivcvgn0  25257  ntrivcvgmullem  25260  zprod  25294  fprod  25298  fprodntriv  25299  fprodser  25306  br8  25410  br6  25411  br4  25412  dfon2lem9  25449  trpredtr  25539  dftrpred3g  25542  frmin  25548  poseq  25559  wzel  25606  wsuclem  25607  wsuclb  25610  frrlem5e  25621  elno2  25640  sltval2  25642  noreson  25646  sltres  25650  noxpsgn  25651  bdayfo  25661  nodenselem3  25669  nodenselem6  25672  nodense  25675  nobndlem2  25679  nobndlem4  25681  nobndlem6  25683  nobndlem8  25685  nobndup  25686  nobnddown  25687  nofulllem4  25691  nofulllem5  25692  fobigcup  25776  imagesset  25829  brbtwn  25869  brcgr  25870  brbtwn2  25875  axpasch  25911  axlowdimlem14  25925  axlowdim2  25930  axcontlem2  25935  axcontlem4  25937  axcontlem7  25940  axcontlem8  25941  axcontlem10  25943  axcontlem12  25945  fvtransport  25997  brcolinear  26024  brsegle  26073  seglerflx  26077  seglemin  26078  btwnsegle  26082  fvray  26106  fvline  26109  hilbert1.1  26119  elhf2  26147  0hf  26149  onsucsuccmpi  26224  limsucncmpi  26226  supaddc  26269  supadd  26270  heicant  26277  mblfinlem1  26279  mblfinlem2  26280  mblfinlem3  26281  mblfinlem4  26282  ismblfin  26283  volsupnfl  26287  dvtanlem  26292  itg2addnclem  26294  itg2addnclem2  26295  itg2addnclem3  26296  itg2addnc  26297  ftc1anclem5  26322  ftc1anc  26326  nn0prpwlem  26363  nn0prpw  26364  opnregcld  26371  cldregopn  26372  fness  26400  ssref  26401  fneref  26402  refref  26403  fnessref  26411  refssfne  26412  finlocfin  26417  locfindis  26423  comppfsc  26425  neibastop2lem  26427  fnemeet1  26433  tailfb  26444  filnetlem4  26448  unirep  26452  cover2  26453  indexa  26473  frinfm  26475  sdclem1  26485  fdc  26487  incsequz  26490  caushft  26505  istotbnd3  26518  0totbnd  26520  sstotbnd2  26521  sstotbnd  26522  sstotbnd3  26523  isbnd2  26530  isbnd3  26531  ssbnd  26535  totbndbnd  26536  equivbnd  26537  prdsbnd  26540  prdstotbnd  26541  cntotbnd  26543  heibor1lem  26556  heiborlem1  26558  heiborlem3  26560  heiborlem6  26563  heiborlem8  26565  heibor  26568  bfplem2  26570  rrncmslem  26579  iccbnd  26587  exidres  26591  isdrngo2  26612  igenval  26709  igenidl  26711  prnc  26715  prtlem10  26752  elrfi  26786  nacsfix  26804  mzpcompact2lem  26846  eldioph  26854  diophrw  26855  eldioph2b  26859  eldioph3  26862  diophin  26869  rexrabdioph  26892  rexzrexnn0  26902  eldioph4b  26910  eldioph4i  26911  rencldnfilem  26919  irrapxlem5  26927  irrapxlem6  26928  pell1234qrdich  26962  pell14qrdich  26970  infmrgelbi  26979  pellqrex  26980  pellfundre  26982  pellfundlb  26985  pellfund14  26999  rmxyelqirr  27011  rmxynorm  27019  congrep  27076  acongrep  27083  jm2.27  27117  fnwe2lem2  27164  islssfgi  27185  pwssplit1  27203  filnm  27207  frlmup4  27268  unxpwdom3  27271  islindf4  27323  lpirlnr  27336  hbtlem2  27343  hbtlem4  27345  hbtlem5  27347  hbt  27349  dgraaub  27368  mpaaeu  27370  aaitgo  27382  rgspnval  27388  rgspncl  27389  rngunsnply  27393  psgnunilem2  27433  psgnunilem3  27434  psgneldm2i  27443  psgnvalii  27447  dvconstbi  27566  ubelsupr  27705  climsuse  27748  stoweidlem9  27772  stoweidlem14  27777  stoweidlem18  27781  stoweidlem21  27784  stoweidlem29  27792  stoweidlem34  27797  stoweidlem35  27798  stoweidlem39  27802  stoweidlem41  27804  stoweidlem45  27808  stoweidlem52  27815  stoweidlem55  27818  stoweidlem57  27820  stoweidlem60  27823  stirlinglem5  27841  stirlinglem13  27849  stirlinglem14  27850  sigarcol  27868  reumodprminv  28285  modprm0  28286  cshw1v  28334  cshwssizesame  28346  lshpnel2N  29881  lsatlspsn2  29888  lsatlspsn  29889  lsmsat  29904  lssatomic  29907  lcvnbtwn  29921  lfl1  29966  eqlkr  29995  lshpkrlem1  30006  lshpkrex  30014  lfl1dim  30017  lfl1dim2N  30018  lkrss2N  30065  cvrcon3b  30173  glbconN  30272  cvrat4  30338  3dim3  30364  ps-2  30373  llni  30403  llnle  30413  lplni  30427  lplnle  30435  lplnexllnN  30459  lvoli  30470  atpointN  30638  lnatexN  30674  elpaddn0  30695  pclfinN  30795  ispsubcl2N  30842  lhprelat3N  30935  4atexlemex2  30966  4atex  30971  4atex2-0aOLDN  30973  4atex2-0cOLDN  30975  lautcvr  30987  cdleme0ex1N  31118  cdleme50rnlem  31439  cdleme50ex  31454  cdlemg1cex  31483  cdlemkid5  31830  cdlemk  31869  tendoex  31870  cdleml5N  31875  cdlemm10N  32014  dihglblem2aN  32189  dihglblem2N  32190  dih1dimatlem0  32224  dihatexv  32234  dihjat1lem  32324  dvh4dimat  32334  dvh3dim2  32344  dvh3dim3N  32345  dochfl1  32372  dochkr1  32374  dochkr1OLDN  32375  lcfl8  32398  lcfrvalsnN  32437  lcfrlem9  32446  lcfrlem27  32465  lcfrlem37  32475  lcfr  32481  mapdval2N  32526  mapdval4N  32528  mapd1o  32544  mapdcv  32556  mapdspex  32564  mapdpglem23  32590  hdmap11lem2  32741  hdmap14lem2a  32766  hdmap14lem6  32772
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 1668  ax-8 1689  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423
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 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-rex 2717  df-v 2964
  Copyright terms: Public domain W3C validator