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

Theorem ralimi 2780
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 2778 1  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1886   A.wral 2736
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681
This theorem depends on definitions:  df-bi 189  df-ral 2741
This theorem is referenced by:  ral2imiOLD  2782  r19.26  2916  r19.29  2924  rr19.3v  3179  rr19.28v  3180  reu3  3227  uniiunlem  3516  reupick2  3728  uniss2  4229  ss2iun  4293  iineq2  4295  iunss2  4322  disjss2  4375  disjeq2  4376  reusv2lem5  4607  reusv3i  4609  ssrel2  4924  issref  5212  dmmptg  5331  wfisg  5414  fununi  5647  fnmptf  5698  fnmpt  5702  mpteqb  5962  chfnrn  5991  fvn0ssdmfun  6011  dffo5  6037  ffvresb  6052  fmptcof  6055  mpt22eqb  6402  ralrnmpt2  6408  tfis  6678  fun11uni  6744  fun11iun  6750  zfrep6  6758  fnmpt2  6858  mpt2exxg  6864  frxp  6903  smores  7068  riiner  7433  ixpn0  7551  boxriin  7561  unifi2  7861  wemaplem2  8059  xpwdomg  8097  rankonidlem  8296  acni3  8475  dfac5  8556  dfac12lem2  8571  kmlem6  8582  kmlem8  8584  kmlem13  8589  cfsmolem  8697  fin23lem40  8778  isf32lem2  8781  fin1a2s  8841  hsmexlem2  8854  hsmex3  8861  axcc4  8866  domtriomlem  8869  dcomex  8874  ac6num  8906  iundom  8964  unirnfdomd  8989  konigthlem  8990  iunctb  8996  gch3  9098  wununi  9128  wunpw  9129  wunpr  9131  eltsk2g  9173  tskpwss  9174  tskpw  9175  grupw  9217  gruurn  9220  intgru  9236  grothpw  9248  grothpwex  9249  grothomex  9251  axgroth3  9253  suplem1pr  9474  supexpr  9476  supsr  9533  fimaxre3  10550  xrsupexmnf  11587  xrinfmexpnf  11588  fsuppmapnn0fiublem  12199  fsuppmapnn0fiub  12200  fsuppmapnn0fiubex  12201  mptnn0fsuppd  12207  rexanre  13402  rexuz3  13404  cau3lem  13410  caubnd2  13413  caubnd  13414  rlim0  13565  rlim0lt  13566  climi2  13568  climi0  13569  climrlim2  13604  rlimres  13615  o1rlimmul  13675  caurcvg  13735  caurcvgOLD  13736  caurcvg2  13737  caucvg  13738  caucvgb  13739  sumeq2  13753  prodeq2  13961  ndvdssub  14381  gcdcllem1  14466  coprmproddvdslem  14672  vdwnnlem1  14938  imasaddfnlem  15427  catidex  15573  catlid  15582  catrid  15583  catcocl  15584  catpropd  15607  subcidcl  15742  funcid  15768  setcepi  15976  tsrss  16462  mgmidmo  16495  gsumval2  16516  isnmnd  16533  issubg2  16825  gagrpid  16941  gaass  16944  dprdcntz  17633  dprddisj  17634  abveq0  18047  abvmul  18050  abvtri  18051  psgndiflemB  19161  phllmhm  19192  ipcj  19194  ipeq0  19198  mdetmul  19641  pmatcollpw2lem  19794  eltg2b  19967  iincld  20047  iuncld  20053  isclo2  20097  neips  20122  neipeltop  20138  lmcvg  20271  t1t0  20357  hauscmplem  20414  bwth  20418  1stcelcls  20469  ptuni2  20584  pttopon  20604  ptcld  20621  ptcnplem  20629  txtube  20648  txlm  20656  xkococnlem  20667  fbun  20848  isfil2  20864  ptcmplem4  21063  tmdcn2  21097  ustssel  21213  isucn2  21287  ucncn  21293  xmeteq0  21346  xmettri2  21348  metrest  21532  tngngp  21655  iscau4  22242  cmetcaulem  22251  caussi  22260  volfiniun  22493  iunmbl  22499  voliun  22500  mbfdm  22577  itg2seq  22693  itg2i1fseqle  22705  itg2i1fseq2  22707  iblcnlem  22739  limcresi  22833  limciun  22842  rolle  22935  ulmss  23345  rlimcnp  23884  midf  24811  colinearalg  24933  axpasch  24964  axeuclid  24986  axcontlem2  24988  axcontlem4  24990  axcontlem7  24993  axcontlem8  24994  nbgraf1olem1  25162  usgfiregdegfi  25632  1to3vfriendship  25729  frconngra  25742  frgraregorufr0  25773  usgreghash2spot  25790  isgrpo  25917  grpoidinv  25929  grpoideu  25930  grpoidval  25937  grpoidinv2  25939  opidonOLD  26043  exidu1  26047  grpomndo  26067  rngoideu  26105  rngodi  26106  rngodir  26107  rngoass  26108  rngoueqz  26151  vcid  26163  vcdi  26164  vcdir  26165  vcass  26166  nvs  26284  nvz  26291  nvtri  26292  ajmoi  26493  adjmo  27478  cnlnssadj  27726  mdbr3  27943  mdbr4  27944  mdsl1i  27967  dmdbr6ati  28069  dmdbr7ati  28070  disjunsn  28197  xrge0infssOLD  28334  hasheuni  28899  sigaclcu2  28935  prsiga  28946  measvunilem  29027  cntmeas  29041  omssubadd  29121  omssubaddOLD  29125  signsply0  29433  bnj1498  29863  cvmsdisj  29986  cvmshmeo  29987  cvmliftlem15  30014  cvmlift2lem12  30030  untangtr  30334  elpotr  30420  dfon2lem7  30428  dfon2lem8  30429  tfisg  30450  frinsg  30476  poseq  30484  opnrebl2  30970  fnemeet2  31016  fnejoin1  31017  fnejoin2  31018  ptrecube  31933  poimirlem25  31958  poimirlem26  31959  poimirlem27  31960  poimirlem30  31963  poimirlem31  31964  poimirlem32  31965  heicant  31968  ovoliunnfl  31975  voliunnfl  31977  volsupnfl  31978  frinfm  32055  caushft  32083  sstotbnd3  32101  prdstotbnd  32119  heibor1lem  32134  bfplem2  32148  rngohomadd  32201  rngohommul  32202  idladdcl  32245  idllmulcl  32246  idlrmulcl  32247  ispridl2  32264  mpt2bi123f  32399  iineq12f  32401  mptbi12f  32403  pmapglbx  33328  ltrnnid  33695  cdlemefrs32fva  33961  lerabdioph  35642  ltrabdioph  35645  nerabdioph  35646  dvdsrabdioph  35647  rencldnfi  35658  dford3  35877  pwelg  36158  pwinfi2  36160  ss2iundf  36245  ralbidar  36792  rexbidar  36793  stoweidlem60  37915  bgoldbtbndlem2  38895  bgoldbtbndlem4  38897  fusgrregdegfi  39569  0grrgr  39579  rusgr1vtxlem  39585  mpt2exxg2  40106
  Copyright terms: Public domain W3C validator