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

Theorem rspcev 3039
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 1629 . 2  |-  F/ x ps
2 rspcv.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
31, 2rspce 3034 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 1652    e. wcel 1725   E.wrex 2693
This theorem is referenced by:  rspc2ev  3047  rspc3ev  3049  reu6i  3112  rspesbca  3228  wefrc  4563  wereu2  4566  onfr  4607  ordunidif  4616  onssmin  4763  onminex  4773  onuninsuci  4806  elrnmpt1s  5104  dffv2  5782  elrnrexdm  5860  eldmrexrn  5862  foco2  5875  elabrex  5971  f1elima  5995  fcofo  6007  fliftfun  6020  fliftval  6024  f1oiso2  6058  fo1st  6352  fo2nd  6353  sorpssuni  6517  sorpssint  6518  onnseq  6592  tfrlem12  6636  seqomlem2  6694  oawordeulem  6783  oaass  6790  odi  6808  omass  6809  omeulem1  6811  oen0  6815  oeordi  6816  oelim2  6824  oeeulem  6830  nnawordex  6866  nneob  6881  ecelqsg  6945  resixpfo  7086  elixpsn  7087  ixpsnf1o  7088  boxcutc  7091  snfi  7173  onfin  7283  pssnn  7313  ssnnfi  7314  dif1enOLD  7326  dif1en  7327  findcard  7333  frfi  7338  fisupg  7341  nnsdomg  7352  unfi  7360  fofinf1o  7373  pwfilem  7387  fissuni  7397  fipreima  7398  finsschain  7399  indexfi  7400  elfir  7406  inelfi  7409  fiin  7413  marypha1lem  7424  eqsup  7445  supmaxlem  7453  fisup2g  7455  fisupcl  7456  supisoex  7460  wofib  7498  wemaplem2  7500  card2inf  7507  brwdom2  7525  cnfcom3clem  7646  trcl  7648  r1ordg  7688  r1pwss  7694  tz9.12lem3  7699  tz9.12  7700  r1elwf  7706  tcrank  7792  scottex  7793  scott0  7794  isnumi  7817  onsdom  7867  fseqdom  7891  ondomen  7902  infpwfien  7927  cardaleph  7954  cardalephex  7955  infenaleph  7956  alephfplem4  7972  alephfp2  7974  dfac2  7995  ackbij1lem18  8101  ackbij1  8102  cflem  8110  cflecard  8117  cfsuc  8121  cfflb  8123  cofsmo  8133  cfsmolem  8134  coftr  8137  fin23lem7  8180  fin23lem11  8181  enfin2i  8185  fin23lem26  8189  fin23lem38  8213  isf32lem5  8221  isf34lem4  8241  isfin1-3  8250  fin1a2lem7  8270  fin1a2lem11  8274  fin1a2lem13  8276  axdc3lem2  8315  axdc3lem4  8317  ttukeylem7  8379  iunfo  8398  ficard  8424  pwcfsdom  8442  fpwwe2lem12  8500  wunex  8598  eltsk2g  8610  grur1  8679  axgroth6  8687  inaprc  8695  nqereu  8790  archnq  8841  genpnmax  8868  ltexpri  8904  prlem936  8908  reclem3pr  8910  recexpr  8912  supexpr  8915  negexsr  8961  recexsrlem  8962  recexsr  8966  supsrlem  8970  axrnegex  9021  axrrecex  9022  axpre-sup  9028  1re  9074  cnegex  9231  cnegex2  9232  recex  9638  receu  9651  fimaxre2  9940  infm3lem  9950  supmul1  9957  supmullem2  9959  supmul  9960  infmrcl  9971  cju  9980  nn2ge  10009  nominpos  10188  zdiv  10324  btwnz  10356  uzwo  10523  uzwoOLD  10524  uzinfmi  10539  ublbneg  10544  lbzbi  10548  zsupss  10549  uzsupss  10552  zq  10564  rpnnen1lem1  10584  rpnnen1lem2  10585  rpnnen1lem3  10586  rpnnen1lem4  10587  rpnnen1lem5  10588  z2ge  10768  qbtwnre  10769  qbtwnxr  10770  xralrple  10775  xrsupsslem  10869  xrinfmsslem  10870  supxrpnf  10881  icc0  10948  iccsupr  10981  flval3  11205  uzsup  11227  fsequb  11297  expnbnd  11491  expmulnbnd  11494  hashkf  11603  hashdom  11636  iswrdi  11714  shftlem  11866  shftfval  11868  sqrlem3  12033  01sqrex  12038  resqrex  12039  sqrneg  12056  abs1m  12122  rexanuz  12132  rexanre  12133  rexuz3  12135  rexuzre  12139  rexico  12140  caubnd2  12144  caubnd  12145  sqreu  12147  rlim2lt  12274  rlim3  12275  lo1bdd2  12301  lo1bddrp  12302  o1lo1  12314  climconst  12320  rlimconst  12321  rlimclim1  12322  climshftlem  12351  rlimcn2  12367  reccn2  12373  cn1lem  12374  rlimo1  12393  o1rlimmul  12395  lo1add  12403  lo1mul  12404  lo1le  12428  isercoll  12444  isercoll2  12445  caucvgrlem  12449  serf0  12457  zsum  12495  fsum  12497  fsumcvg3  12506  climcnds  12614  divrcnv  12615  infcvgaux2i  12620  mertenslem1  12644  mertenslem2  12645  ruclem12  12823  dvdsval2  12838  dvds0lem  12843  dvds1lem  12844  dvds2lem  12845  odd2np1lem  12890  odd2np1  12891  divalglem9  12904  gcdcllem3  12996  bezoutlem1  13021  qredeu  13090  exprmfct  13093  isprm5  13095  maxprmfct  13096  odzcllem  13161  opeo  13170  omeo  13171  pythagtriplem19  13190  pcprmpw2  13238  pcprmpw  13239  pockthi  13258  infpnlem2  13262  prmreclem1  13267  prmreclem5  13271  prmreclem6  13272  1arithlem4  13277  vdwapun  13325  vdwlem1  13332  vdwlem2  13333  vdwlem6  13337  vdwlem8  13339  vdwlem10  13341  vdwlem13  13344  ramz  13376  ramub1lem1  13377  elrestr  13639  imasleval  13749  mreexexlem3d  13854  mreexexlem4d  13855  iscatd  13881  poslubd  14557  fpwipodrs  14573  spwpr4  14646  ismgmid2  14696  ismndd  14702  gsumvallem1  14754  gsumval2a  14765  gsumwspan  14774  isgrpd2  14811  isgrpd  14813  imasgrp2  14916  gaorber  15068  orbsta  15073  cayleyth  15096  odf1o2  15190  pgpfi1  15212  sylow1lem3  15217  sylow1lem5  15219  pgpfi  15222  pgpssslw  15231  sylow2alem2  15235  slwhash  15241  fislw  15242  lsmelvalm  15268  pj1id  15314  efgs1b  15351  efgrelexlemb  15365  efgredeu  15367  gexex  15451  cyggeninv  15476  0cyg  15485  lt6abl  15487  eldprdi  15559  pgpfac1lem3a  15617  pgpfac1lem3  15618  pgpfac1lem5  15620  pgpfaclem1  15622  pgpfaclem3  15624  ablfaclem2  15627  dvdsrmul  15736  dvdsr01  15743  irredrmul  15795  lss1d  16022  lspf  16033  lspval  16034  lssats2  16059  lspsn  16061  lspsneq  16177  lspfixed  16183  lspsolvlem  16197  lspprat  16208  lbsextlem2  16214  lpi0  16301  lpi1  16302  aspval  16370  zlpir  16754  zcyg  16755  zncyg  16812  znf1o  16815  cygznlem3  16833  cygth  16835  frgpcyg  16837  fiinbas  17000  topbas  17020  pptbas  17055  clsval  17084  clsval2  17097  elcls  17120  neiint  17151  neips  17160  opnneissb  17161  opnssneib  17162  innei  17172  neiptopnei  17179  restbas  17205  restcld  17219  restcldi  17220  restopnb  17222  neitr  17227  restcls  17228  ordtbas2  17238  ordtopn1  17241  ordtopn2  17242  leordtval2  17259  iocpnfordt  17262  icomnfordt  17263  lecldbas  17266  pnfnei  17267  mnfnei  17268  lmconst  17308  iscnp4  17310  cncnpi  17325  cnconst2  17330  cnprest  17336  cnpdis  17340  pnrmopn  17390  nrmsep  17404  regsep2  17423  cmpcovf  17437  cncmp  17438  fincmp  17439  cmpsublem  17445  cmpsub  17446  tgcmp  17447  cmpcld  17448  uncmp  17449  hauscmplem  17452  cmpfi  17454  consubclo  17470  concompid  17477  2ndci  17494  2ndcsb  17495  2ndc1stc  17497  1stcrest  17499  2ndcctbss  17501  2ndcdisj  17502  2ndcomap  17504  2ndcsep  17505  dis2ndc  17506  restlly  17529  islly2  17530  hausllycmp  17540  cldllycmp  17541  lly1stc  17542  dislly  17543  llycmpkgen2  17565  cmpkgen  17566  1stckgenlem  17568  elptr  17588  ptbasfi  17596  neitx  17622  ptpjopn  17627  txcnp  17635  ptcnplem  17636  txlly  17651  txnlly  17652  txtube  17655  txcmplem1  17656  txcmplem2  17657  tx1stc  17665  txkgen  17667  xkococnlem  17674  txcon  17704  tgqtop  17727  qtopeu  17731  kqreglem1  17756  kqreglem2  17757  kqnrmlem1  17758  kqnrmlem2  17759  reghmph  17808  nrmhmph  17809  fbssfi  17852  opnfbas  17857  isfil2  17871  fsubbas  17882  ssfg  17887  fgss2  17889  fbasrn  17899  filuni  17900  fgtr  17905  ssufl  17933  uffix  17936  elfm  17962  elfm2  17963  elfm3  17965  imaelfm  17966  rnelfmlem  17967  rnelfm  17968  fmfnfmlem3  17971  fmfnfmlem4  17972  fmfnfm  17973  fmco  17976  ufldom  17977  hausflim  17996  flimcls  18000  hauspwpwf1  18002  flffbas  18010  txflf  18021  fclscf  18040  fclsfnflim  18042  alexsubALTlem3  18063  alexsubALTlem4  18064  alexsubALT  18065  ptcmplem2  18067  ptcmplem3  18068  ptcmplem5  18070  tmdgsum2  18109  symgtgp  18114  subgntr  18119  opnsubg  18120  ghmcnp  18127  divstgpopn  18132  tsmsfbas  18140  tsmsgsum  18151  tsmsres  18156  tsmsxplem1  18165  tsmsxp  18167  ustexsym  18228  elrnust  18237  trust  18242  utoptop  18247  restutop  18250  restutopopn  18251  ustuqtop1  18254  ustuqtop2  18255  ustuqtop4  18257  ustuqtop5  18258  utopsnneiplem  18260  utopsnnei  18262  iducn  18296  fmucnd  18305  cfilufg  18306  trcfilu  18307  neipcfilu  18309  imasdsf1olem  18386  blssps  18437  blss  18438  blssexps  18439  blssex  18440  ssblex  18441  blin2  18442  neibl  18514  blcld  18518  metss2  18525  stdbdmopn  18531  mopnex  18532  met1stc  18534  met2ndci  18535  metrest  18537  prdsxmslem2  18542  metcnp3  18553  metcnpi3  18559  metuvalOLD  18562  metuval  18563  metustexhalfOLD  18576  metustexhalf  18577  metustfbasOLD  18578  metustfbas  18579  cfilucfilOLD  18582  cfilucfil  18583  restmetu  18600  metucnOLD  18601  metucn  18602  dscopn  18604  ngptgp  18660  nlmvscnlem1  18705  nrginvrcnlem  18709  nghmcn  18762  tgioo  18810  tgqioo  18814  xrsmopn  18826  zcld  18827  recld2  18828  zdis  18830  icccmplem1  18836  icccmplem2  18837  icccmplem3  18838  reconnlem2  18841  xmetdcn2  18851  metdscn  18869  addcnlem  18877  elcncf1di  18908  icoopnst  18947  iocopnst  18948  xrhmeo  18954  cnheibor  18963  cnllycmp  18964  lebnumlem3  18971  lebnum  18972  xlebnum  18973  lebnumii  18974  elpi1i  19054  ipcnlem1  19182  lmnn  19199  iscfil3  19209  cfilres  19232  flimcfil  19249  cncmet  19258  bcthlem4  19263  bcthlem5  19264  minveclem4c  19309  minveclem2  19310  minveclem3b  19312  minveclem3  19313  minveclem4  19316  minveclem6  19318  ivthlem2  19332  ivthlem3  19333  ivth  19334  ivthle  19336  ivthle2  19337  cniccbdd  19341  elovolmr  19355  ovolunlem1  19376  ovoliunlem1  19381  ovoliunlem2  19382  ovoliun2  19385  ovolicc1  19395  iundisj  19425  iunmbl2  19434  ioombl1lem4  19438  uniioombllem2  19458  uniioombllem3  19460  uniioombllem6  19463  dyadmbllem  19474  volcn  19481  volivth  19482  vitalilem2  19484  mbfinf  19540  mbflimsup  19541  i1faddlem  19568  i1fmullem  19569  itg1addlem4  19574  i1fmulc  19578  itg1climres  19589  itg2lr  19605  itg2monolem1  19625  itg2i1fseq  19630  itg2i1fseq2  19631  itg2cnlem1  19636  itg2cnlem2  19637  limcnlp  19748  ellimc3  19749  limcflf  19751  limciun  19764  dveflem  19846  rollelem  19856  c1lip1  19864  lhop1lem  19880  evlseu  19920  ply1divex  20042  ig1peu  20077  ply1lpir  20084  elply2  20098  plyeq0lem  20112  coeeq  20129  plydivlem3  20195  plydivlem4  20196  elqaalem3  20221  qaa  20223  iaa  20225  aareccl  20226  aannenlem2  20229  aalioulem2  20233  aalioulem3  20234  aalioulem5  20236  aalioulem6  20237  aaliou  20238  aaliou2  20240  aaliou3lem8  20245  ulmshftlem  20288  ulmbdd  20297  mtestbdd  20304  iblulm  20306  abelthlem8  20338  reeff1o  20346  pilem2  20351  pilem3  20352  efif1olem2  20428  eflogeq  20479  divlogrlim  20509  efopn  20532  cxpcn3lem  20614  cxpeq  20624  angpieqvd  20655  dcubic2  20667  quart  20684  rlimcnp  20787  xrlimcnp  20790  cxplim  20793  cxploglim  20799  emcllem6  20822  ftalem1  20838  ftalem2  20839  ftalem3  20840  ftalem5  20842  ftalem7  20844  isppw2  20881  sgmnncl  20913  dvdsppwf1o  20954  musum  20959  dvdsmulf1o  20962  perfect  20998  dchrptlem1  21031  dchrptlem2  21032  dchrpt  21034  bpos1lem  21049  lgsqrlem4  21111  lgsdchrval  21114  lgsquadlem1  21121  2sqlem2  21131  mul2sq  21132  2sqlem3  21133  2sqlem9  21140  2sqlem10  21141  2sqblem  21144  dchrisumlem3  21168  dchrisum0  21197  chpdifbndlem2  21231  pntrsumbnd2  21244  pntpbnd1  21263  pntpbnd2  21264  pntpbnd  21265  pntibndlem2  21268  pntibndlem3  21269  pntleme  21285  pntlem3  21286  ostth2  21314  ostth3  21315  umgraex  21341  cusgrares  21464  usgrasscusgra  21475  eupa0  21679  eupares  21680  eupap1  21681  lpni  21750  isgrpo  21767  isgrpoi  21769  grpoinvf  21811  isgrpda  21868  isgrpod  21869  isablod  21871  opidon  21893  ghgrp  21939  isrngod  21950  cnrngo  21974  rngmgmbs4  21988  vacn  22173  nmcvcn  22174  smcnlem  22176  nmosetn0  22249  nmoolb  22255  nmobndi  22259  nmoo0  22275  nmlno0lem  22277  isblo3i  22285  blo3i  22286  blocnilem  22288  blocni  22289  ubthlem1  22355  ubthlem2  22356  ubthlem3  22357  minvecolem2  22360  minvecolem3  22361  minvecolem4c  22364  minvecolem4  22365  minvecolem5  22366  minvecolem6  22367  htthlem  22403  norm1exi  22735  occl  22789  shsel3  22800  spanval  22818  spancl  22821  shsval2i  22872  pjhthlem2  22877  ococin  22893  h1de2ctlem  23040  spansncol  23053  pjoml6i  23074  nmopsetn0  23351  nmfnsetn0  23364  nmoplb  23393  nmfnlb  23410  0cnop  23465  0cnfn  23466  idcnop  23467  nmop0  23472  nmfn0  23473  nmlnop0iALT  23481  nmopun  23500  nmcexi  23512  lnconi  23519  lnopcnbd  23522  lnfncnbd  23543  riesz3i  23548  riesz1  23551  cnlnadjlem2  23554  cnlnadjlem8  23560  cnlnadjlem9  23561  adjbd1o  23571  branmfn  23591  opsqrlem1  23626  pjnmopi  23634  strlem1  23736  stri  23743  hstri  23751  cvcon3  23770  cvnbtwn  23772  superpos  23840  shatomici  23844  atcvat4i  23883  mdsymlem2  23890  cdj1i  23919  cdj3lem2  23921  cdj3i  23927  rexunirn  23961  iundisjf  24012  elunirn2  24046  ssnnssfz  24131  iundisjfi  24135  xreceu  24151  rexdiv  24155  rhmdvdsr  24239  metidval  24268  pstmval  24273  tpr2rico  24293  rge0scvg  24318  pnfneige0  24319  qqhcn  24358  qqhucn  24359  rrhre  24370  indf1ofs  24406  gsumesum  24434  esumcst  24438  esumpcvgval  24451  dmsigagen  24510  dya2icoseg  24610  dya2iocnrect  24614  dya2iocuni  24616  sxbrsigalem2  24619  dstfrvunirn  24715  ballotlem4  24739  ballotlemic  24747  ballotlem1c  24748  ballotlemrc  24771  lgambdd  24804  subfacp1lem3  24851  erdsze2lem2  24873  cnpcon  24900  txpcon  24902  ptpcon  24903  indispcon  24904  conpcon  24905  cvxpcon  24912  cnllyscon  24915  cvmsss2  24944  cvmcov2  24945  cvmopnlem  24948  cvmfolem  24949  cvmliftlem14  24967  cvmliftlem15  24968  cvmlift2lem11  24983  cvmlift2lem12  24984  cvmlift2lem13  24985  cvmlift3lem2  24990  cvmlift3lem6  24994  cvmlift3lem9  24997  rtrclreclem.refl  25127  rtrclreclem.subset  25128  rtrclreclem.trans  25129  dedekind  25170  dedekindle  25171  ntrivcvgn0  25210  ntrivcvgmullem  25213  zprod  25247  fprod  25251  fprodntriv  25252  fprodser  25259  br8  25363  br6  25364  br4  25365  dfon2lem9  25397  trpredtr  25483  dftrpred3g  25486  frmin  25492  poseq  25503  frrlem5e  25539  elno2  25558  sltval2  25560  noreson  25564  sltres  25568  noxpsgn  25569  bdayfo  25579  nodenselem3  25587  nodenselem6  25590  nodense  25593  nobndlem2  25597  nobndlem4  25599  nobndlem6  25601  nobndlem8  25603  nobndup  25604  nobnddown  25605  nofulllem4  25609  nofulllem5  25610  fobigcup  25690  imagesset  25743  brbtwn  25781  brcgr  25782  brbtwn2  25787  axpasch  25823  axlowdimlem14  25837  axlowdim2  25842  axcontlem2  25847  axcontlem4  25849  axcontlem7  25852  axcontlem8  25853  axcontlem10  25855  axcontlem12  25857  fvtransport  25909  brcolinear  25936  brsegle  25985  seglerflx  25989  seglemin  25990  btwnsegle  25994  fvray  26018  fvline  26021  hilbert1.1  26031  elhf2  26059  0hf  26061  onsucsuccmpi  26136  limsucncmpi  26138  supaddc  26179  supadd  26180  mblfinlem  26185  mblfinlem2  26186  mblfinlem3  26187  ismblfin  26188  volsupnfl  26192  itg2addnclem  26197  itg2addnclem2  26198  itg2addnclem3  26199  itg2addnc  26200  nn0prpwlem  26257  nn0prpw  26258  opnregcld  26265  cldregopn  26266  fness  26294  ssref  26295  fneref  26296  refref  26297  fnessref  26305  refssfne  26306  finlocfin  26311  locfindis  26317  comppfsc  26319  neibastop2lem  26321  fnemeet1  26327  tailfb  26338  filnetlem4  26342  unirep  26346  cover2  26347  indexa  26367  frinfm  26369  sdclem1  26379  fdc  26381  incsequz  26384  caushft  26399  istotbnd3  26412  0totbnd  26414  sstotbnd2  26415  sstotbnd  26416  sstotbnd3  26417  isbnd2  26424  isbnd3  26425  ssbnd  26429  totbndbnd  26430  equivbnd  26431  prdsbnd  26434  prdstotbnd  26435  cntotbnd  26437  heibor1lem  26450  heiborlem1  26452  heiborlem3  26454  heiborlem6  26457  heiborlem8  26459  heibor  26462  bfplem2  26464  rrncmslem  26473  iccbnd  26481  exidres  26485  isdrngo2  26506  igenval  26603  igenidl  26605  prnc  26609  prtlem10  26646  elrfi  26680  nacsfix  26698  mzpcompact2lem  26740  eldioph  26748  diophrw  26749  eldioph2b  26753  eldioph3  26756  diophin  26763  rexrabdioph  26786  rexzrexnn0  26796  eldioph4b  26804  eldioph4i  26805  rencldnfilem  26813  irrapxlem5  26821  irrapxlem6  26822  pell1234qrdich  26856  pell14qrdich  26864  infmrgelbi  26873  pellqrex  26874  pellfundre  26876  pellfundlb  26879  pellfund14  26893  rmxyelqirr  26905  rmxynorm  26913  congrep  26970  acongrep  26977  jm2.27  27011  fnwe2lem2  27058  islssfgi  27080  pwssplit1  27098  filnm  27102  frlmup4  27163  unxpwdom3  27166  islindf4  27218  lpirlnr  27231  hbtlem2  27238  hbtlem4  27240  hbtlem5  27242  hbt  27244  dgraaub  27263  mpaaeu  27265  aaitgo  27277  rgspnval  27283  rgspncl  27284  rngunsnply  27288  psgnunilem2  27328  psgnunilem3  27329  psgneldm2i  27338  psgnvalii  27342  dvconstbi  27461  ubelsupr  27600  climsuse  27643  stoweidlem9  27667  stoweidlem14  27672  stoweidlem18  27676  stoweidlem21  27679  stoweidlem29  27687  stoweidlem34  27692  stoweidlem35  27693  stoweidlem39  27697  stoweidlem41  27699  stoweidlem45  27703  stoweidlem52  27710  stoweidlem55  27713  stoweidlem57  27715  stoweidlem60  27718  stirlinglem5  27736  stirlinglem13  27744  stirlinglem14  27745  sigarcol  27763  lshpnel2N  29514  lsatlspsn2  29521  lsatlspsn  29522  lsmsat  29537  lssatomic  29540  lcvnbtwn  29554  lfl1  29599  eqlkr  29628  lshpkrlem1  29639  lshpkrex  29647  lfl1dim  29650  lfl1dim2N  29651  lkrss2N  29698  cvrcon3b  29806  glbconN  29905  cvrat4  29971  3dim3  29997  ps-2  30006  llni  30036  llnle  30046  lplni  30060  lplnle  30068  lplnexllnN  30092  lvoli  30103  atpointN  30271  lnatexN  30307  elpaddn0  30328  pclfinN  30428  ispsubcl2N  30475  lhprelat3N  30568  4atexlemex2  30599  4atex  30604  4atex2-0aOLDN  30606  4atex2-0cOLDN  30608  lautcvr  30620  cdleme0ex1N  30751  cdleme50rnlem  31072  cdleme50ex  31087  cdlemg1cex  31116  cdlemkid5  31463  cdlemk  31502  tendoex  31503  cdleml5N  31508  cdlemm10N  31647  dihglblem2aN  31822  dihglblem2N  31823  dih1dimatlem0  31857  dihatexv  31867  dihjat1lem  31957  dvh4dimat  31967  dvh3dim2  31977  dvh3dim3N  31978  dochfl1  32005  dochkr1  32007  dochkr1OLDN  32008  lcfl8  32031  lcfrvalsnN  32070  lcfrlem9  32079  lcfrlem27  32098  lcfrlem37  32108  lcfr  32114  mapdval2N  32159  mapdval4N  32161  mapd1o  32177  mapdcv  32189  mapdspex  32197  mapdpglem23  32223  hdmap11lem2  32374  hdmap14lem2a  32399  hdmap14lem6  32405
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2411
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2417  df-cleq 2423  df-clel 2426  df-nfc 2555  df-rex 2698  df-v 2945
  Copyright terms: Public domain W3C validator