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

Theorem ralimi 2796
Description: Inference quantifying both antecedent and consequent, with strong hypothesis. (Contributed by NM, 4-Mar-1997.)
Hypothesis
Ref Expression
ralimi.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
ralimi  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ps )

Proof of Theorem ralimi
StepHypRef Expression
1 ralimi.1 . . 3  |-  ( ph  ->  ps )
21a1i 11 . 2  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
32ralimia 2794 1  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1904   A.wral 2756
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690
This theorem depends on definitions:  df-bi 190  df-ral 2761
This theorem is referenced by:  r19.26  2904  r19.29  2912  rr19.3v  3168  rr19.28v  3169  reu3  3216  uniiunlem  3503  reupick2  3720  uniss2  4222  ss2iun  4285  iineq2  4287  iunss2  4314  disjss2  4369  disjeq2  4370  reusv2lem5  4606  reusv3i  4608  ssrel2  4930  issref  5219  dmmptg  5339  wfisg  5422  fununi  5659  fnmptf  5710  fnmpt  5714  mpteqb  5979  chfnrn  6008  fvn0ssdmfun  6028  dffo5  6054  ffvresb  6070  fmptcof  6073  mpt22eqb  6424  ralrnmpt2  6430  tfis  6700  fun11uni  6766  fun11iun  6772  zfrep6  6780  fnmpt2  6880  mpt2exxg  6886  frxp  6925  smores  7089  riiner  7454  ixpn0  7572  boxriin  7582  unifi2  7882  wemaplem2  8080  xpwdomg  8118  rankonidlem  8317  acni3  8496  dfac5  8577  dfac12lem2  8592  kmlem6  8603  kmlem8  8605  kmlem13  8610  cfsmolem  8718  fin23lem40  8799  isf32lem2  8802  fin1a2s  8862  hsmexlem2  8875  hsmex3  8882  axcc4  8887  domtriomlem  8890  dcomex  8895  ac6num  8927  iundom  8985  unirnfdomd  9010  konigthlem  9011  iunctb  9017  gch3  9119  wununi  9149  wunpw  9150  wunpr  9152  eltsk2g  9194  tskpwss  9195  tskpw  9196  grupw  9238  gruurn  9241  intgru  9257  grothpw  9269  grothpwex  9270  grothomex  9272  axgroth3  9274  suplem1pr  9495  supexpr  9497  supsr  9554  fimaxre3  10575  xrsupexmnf  11615  xrinfmexpnf  11616  fsuppmapnn0fiublem  12240  fsuppmapnn0fiub  12241  fsuppmapnn0fiubex  12242  mptnn0fsuppd  12248  rexanre  13486  rexuz3  13488  cau3lem  13494  caubnd2  13497  caubnd  13498  rlim0  13649  rlim0lt  13650  climi2  13652  climi0  13653  climrlim2  13688  rlimres  13699  o1rlimmul  13759  caurcvg  13819  caurcvgOLD  13820  caurcvg2  13821  caucvg  13822  caucvgb  13823  sumeq2  13837  prodeq2  14045  ndvdssub  14467  gcdcllem1  14552  coprmproddvdslem  14758  vdwnnlem1  15024  imasaddfnlem  15512  catidex  15658  catlid  15667  catrid  15668  catcocl  15669  catpropd  15692  subcidcl  15827  funcid  15853  setcepi  16061  tsrss  16547  mgmidmo  16580  gsumval2  16601  isnmnd  16618  issubg2  16910  gagrpid  17026  gaass  17029  dprdcntz  17718  dprddisj  17719  abveq0  18132  abvmul  18135  abvtri  18136  psgndiflemB  19245  phllmhm  19276  ipcj  19278  ipeq0  19282  mdetmul  19725  pmatcollpw2lem  19878  eltg2b  20051  iincld  20131  iuncld  20137  isclo2  20181  neips  20206  neipeltop  20222  lmcvg  20355  t1t0  20441  hauscmplem  20498  bwth  20502  1stcelcls  20553  ptuni2  20668  pttopon  20688  ptcld  20705  ptcnplem  20713  txtube  20732  txlm  20740  xkococnlem  20751  fbun  20933  isfil2  20949  ptcmplem4  21148  tmdcn2  21182  ustssel  21298  isucn2  21372  ucncn  21378  xmeteq0  21431  xmettri2  21433  metrest  21617  tngngp  21740  iscau4  22327  cmetcaulem  22336  caussi  22345  volfiniun  22579  iunmbl  22585  voliun  22586  mbfdm  22663  itg2seq  22779  itg2i1fseqle  22791  itg2i1fseq2  22793  iblcnlem  22825  limcresi  22919  limciun  22928  rolle  23021  ulmss  23431  rlimcnp  23970  midf  24897  colinearalg  25019  axpasch  25050  axeuclid  25072  axcontlem2  25074  axcontlem4  25076  axcontlem7  25079  axcontlem8  25080  nbgraf1olem1  25248  usgfiregdegfi  25718  1to3vfriendship  25815  frconngra  25828  frgraregorufr0  25859  usgreghash2spot  25876  isgrpo  26005  grpoidinv  26017  grpoideu  26018  grpoidval  26025  grpoidinv2  26027  opidonOLD  26131  exidu1  26135  grpomndo  26155  rngoideu  26193  rngodi  26194  rngodir  26195  rngoass  26196  rngoueqz  26239  vcid  26251  vcdi  26252  vcdir  26253  vcass  26254  nvs  26372  nvz  26379  nvtri  26380  ajmoi  26581  adjmo  27566  cnlnssadj  27814  mdbr3  28031  mdbr4  28032  mdsl1i  28055  dmdbr6ati  28157  dmdbr7ati  28158  disjunsn  28281  xrge0infssOLD  28416  hasheuni  28980  sigaclcu2  29016  prsiga  29027  measvunilem  29108  cntmeas  29122  omssubadd  29201  omssubaddOLD  29205  signsply0  29512  bnj1498  29942  cvmsdisj  30065  cvmshmeo  30066  cvmliftlem15  30093  cvmlift2lem12  30109  untangtr  30413  elpotr  30498  dfon2lem7  30506  dfon2lem8  30507  tfisg  30528  frinsg  30554  poseq  30562  opnrebl2  31048  fnemeet2  31094  fnejoin1  31095  fnejoin2  31096  ptrecube  32004  poimirlem25  32029  poimirlem26  32030  poimirlem27  32031  poimirlem30  32034  poimirlem31  32035  poimirlem32  32036  heicant  32039  ovoliunnfl  32046  voliunnfl  32048  volsupnfl  32049  frinfm  32126  caushft  32154  sstotbnd3  32172  prdstotbnd  32190  heibor1lem  32205  bfplem2  32219  rngohomadd  32272  rngohommul  32273  idladdcl  32316  idllmulcl  32317  idlrmulcl  32318  ispridl2  32335  mpt2bi123f  32470  iineq12f  32472  mptbi12f  32474  pmapglbx  33405  ltrnnid  33772  cdlemefrs32fva  34038  lerabdioph  35719  ltrabdioph  35722  nerabdioph  35723  dvdsrabdioph  35724  rencldnfi  35735  dford3  35954  pwelg  36235  pwinfi2  36237  ss2iundf  36322  ralbidar  36868  rexbidar  36869  stoweidlem60  38033  bgoldbtbndlem2  39046  bgoldbtbndlem4  39048  fusgrregdegfi  39775  0grrgr  39785  rusgr1vtxlem  39791  1wlkvtxeledg  39878  lfgriswlk  39880  lfgr1wlknloop  39881  1wlkdlem3  39884  1wlkdlem4  39885  eulercrct  40154  mpt2exxg2  40627
  Copyright terms: Public domain W3C validator