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

Theorem ralimi 2618
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 10 . 2  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
32ralimia 2616 1  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684   A.wral 2543
This theorem is referenced by:  ral2imi  2619  r19.26  2675  r19.29  2683  rr19.3v  2909  rr19.28v  2910  reu3  2955  uniiunlem  3260  reupick2  3454  uniss2  3858  ss2iun  3920  iineq2  3922  iunss2  3947  disjss2  3996  disjeq2  3997  reusv2lem5  4539  reusv3i  4541  tfis  4645  issref  5056  dmmptg  5170  fununi  5316  fun11uni  5318  fnmpt  5370  fun11iun  5493  mpteqb  5614  chfnrn  5636  dffo5  5677  ffvresb  5690  fmptcof  5692  zfrep6  5748  mpt22eqb  5953  ralrnmpt2  5958  fnmpt2  6192  mpt2exxg  6195  frxp  6225  smores  6369  riiner  6732  ixpn0  6848  boxriin  6858  unifi2  7146  wemaplem2  7262  xpwdomg  7299  rankonidlem  7500  acni3  7674  dfac5  7755  dfac12lem2  7770  kmlem6  7781  kmlem8  7783  kmlem13  7788  cfsmolem  7896  fin23lem40  7977  isf32lem2  7980  fin1a2s  8040  hsmexlem2  8053  hsmex3  8060  axcc4  8065  domtriomlem  8068  dcomex  8073  ac6num  8106  iundom  8164  unirnfdomd  8189  konigthlem  8190  iunctb  8196  gch3  8302  wununi  8328  wunpw  8329  wunpr  8331  eltsk2g  8373  tskpwss  8374  tskpw  8375  grupw  8417  gruurn  8420  intgru  8436  grothpw  8448  grothpwex  8449  grothomex  8451  axgroth3  8453  suplem1pr  8676  supexpr  8678  supsr  8734  fimaxre3  9703  xrsupexmnf  10623  xrinfmexpnf  10624  rexanre  11830  rexuz3  11832  cau3lem  11838  caubnd2  11841  caubnd  11842  rlim0  11982  rlim0lt  11983  climi2  11985  climi0  11986  climrlim2  12021  rlimres  12032  o1rlimmul  12092  caurcvg  12149  caurcvg2  12150  caucvg  12151  caucvgb  12152  sumeq2  12167  ndvdssub  12606  gcdcllem1  12690  vdwnnlem1  13042  imasaddfnlem  13430  catidex  13576  catlid  13585  catrid  13586  catcocl  13587  catpropd  13612  subcidcl  13718  funcid  13744  setcepi  13920  tsrss  14332  laspwcl  14343  lanfwcl  14344  mgmidmo  14370  gsumval2  14460  issubg2  14636  gagrpid  14748  gaass  14751  dprdcntz  15243  dprddisj  15244  abveq0  15591  abvmul  15594  abvtri  15595  phllmhm  16536  ipcj  16538  ipeq0  16542  eltg2b  16697  iincld  16776  iuncld  16782  isclo2  16825  neips  16850  lmcvg  16992  t1t0  17076  hauscmplem  17133  1stcelcls  17187  ptuni2  17271  pttopon  17291  ptcld  17307  ptcnplem  17315  txtube  17334  txlm  17342  xkococnlem  17353  fbun  17535  isfil2  17551  ptcmplem4  17749  tmdcn2  17772  xmeteq0  17903  xmettri2  17905  metrest  18070  tngngp  18170  iscau4  18705  cmetcaulem  18714  caussi  18723  volfiniun  18904  iunmbl  18910  voliun  18911  mbfdm  18983  itg2seq  19097  itg2i1fseqle  19109  itg2i1fseq2  19111  iblcnlem  19143  limcresi  19235  limciun  19244  rolle  19337  ulmss  19774  rlimcnp  20260  isgrpo  20863  grpoidinv  20875  grpoideu  20876  grpoidval  20883  grpoidinv2  20885  opidon  20989  exidu1  20993  grpomndo  21013  rngoideu  21051  rngodi  21052  rngodir  21053  rngoass  21054  rngoueqz  21097  vcid  21107  vcdi  21108  vcdir  21109  vcass  21110  nvs  21228  nvz  21235  nvtri  21236  ajmoi  21437  adjmo  22412  cnlnssadj  22660  mdbr3  22877  mdbr4  22878  mdsl1i  22901  dmdbr6ati  23003  dmdbr7ati  23004  fnmptf  23227  hasheuni  23453  sigaclcu2  23481  prsiga  23492  measvunilem  23540  cntmeas  23553  cvmsdisj  23801  cvmshmeo  23802  cvmliftlem15  23829  cvmlift2lem12  23845  untangtr  24060  elpotr  24137  dfon2lem7  24145  dfon2lem8  24146  tfisg  24204  wfisg  24209  frinsg  24245  poseq  24253  colinearalg  24538  axpasch  24569  axeuclid  24591  axcontlem2  24593  axcontlem4  24595  axcontlem7  24598  axcontlem8  24599  domfldrefc  25057  ranfldrefc  25058  domintrefb  25063  celsor  25111  ab2rexexg2  25121  domintrefc  25125  mapmapmap  25148  dstr  25171  labs1  25188  labs2  25190  prodeq3  25309  fprodadd  25352  fprodsub  25379  fldax3  25430  fldax4  25431  fldax5  25432  vecax3  25455  vecax4  25456  vecax5  25457  vecax6  25458  glmrngo  25482  svli2  25484  basexre  25522  intopcoaconlem3b  25538  intopcoaconb  25540  intopcoaconc  25541  altretop  25600  imonclem  25813  iepiclem  25823  tartarmap  25888  fnckleb  26046  opnrebl2  26236  fnemeet2  26316  fnejoin1  26317  fnejoin2  26318  frinfm  26416  caushft  26477  sstotbnd3  26500  prdstotbnd  26518  heibor1lem  26533  bfplem2  26547  rngohomadd  26600  rngohommul  26601  idladdcl  26644  idllmulcl  26645  idlrmulcl  26646  ispridl2  26663  lerabdioph  26886  ltrabdioph  26889  nerabdioph  26890  dvdsrabdioph  26891  rencldnfi  26904  dford3  27121  ralbidar  27648  rexbidar  27649  stoweidlem7  27756  stoweidlem60  27809  1to3vfriendship  28186  bnj1498  29091  pmapglbx  29958  ltrnnid  30325  cdlemefrs32fva  30589
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544
This theorem depends on definitions:  df-bi 177  df-ral 2548
  Copyright terms: Public domain W3C validator