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

Theorem ralimi 2819
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 2817 1  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1758   A.wral 2799
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603
This theorem depends on definitions:  df-bi 185  df-ral 2804
This theorem is referenced by:  ral2imiOLD  2821  r19.26  2955  r19.29  2963  rr19.3v  3208  rr19.28v  3209  reu3  3256  uniiunlem  3551  reupick2  3747  uniss2  4235  ss2iun  4297  iineq2  4299  iunss2  4326  disjss2  4376  disjeq2  4377  reusv2lem5  4608  reusv3i  4610  ssrel2  5041  issref  5322  dmmptg  5446  fununi  5595  fnmpt  5648  mpteqb  5900  chfnrn  5926  dffo5  5972  ffvresb  5986  fmptcof  5989  mpt22eqb  6312  ralrnmpt2  6318  tfis  6578  fun11uni  6644  fun11iun  6650  zfrep6  6658  fnmpt2  6755  mpt2exxg  6760  frxp  6795  smores  6926  riiner  7286  ixpn0  7408  boxriin  7418  unifi2  7715  wemaplem2  7875  xpwdomg  7914  rankonidlem  8149  acni3  8331  dfac5  8412  dfac12lem2  8427  kmlem6  8438  kmlem8  8440  kmlem13  8445  cfsmolem  8553  fin23lem40  8634  isf32lem2  8637  fin1a2s  8697  hsmexlem2  8710  hsmex3  8717  axcc4  8722  domtriomlem  8725  dcomex  8730  ac6num  8762  iundom  8820  unirnfdomd  8845  konigthlem  8846  iunctb  8852  gch3  8957  wununi  8987  wunpw  8988  wunpr  8990  eltsk2g  9032  tskpwss  9033  tskpw  9034  grupw  9076  gruurn  9079  intgru  9095  grothpw  9107  grothpwex  9108  grothomex  9110  axgroth3  9112  suplem1pr  9335  supexpr  9337  supsr  9393  fimaxre3  10393  xrsupexmnf  11381  xrinfmexpnf  11382  rexanre  12955  rexuz3  12957  cau3lem  12963  caubnd2  12966  caubnd  12967  rlim0  13107  rlim0lt  13108  climi2  13110  climi0  13111  climrlim2  13146  rlimres  13157  o1rlimmul  13217  caurcvg  13275  caurcvg2  13276  caucvg  13277  caucvgb  13278  sumeq2  13292  ndvdssub  13732  gcdcllem1  13816  vdwnnlem1  14177  imasaddfnlem  14588  catidex  14734  catlid  14743  catrid  14744  catcocl  14745  catpropd  14770  subcidcl  14876  funcid  14902  setcepi  15078  tsrss  15515  mgmidmo  15540  gsumval2  15635  issubg2  15818  gagrpid  15934  gaass  15937  dprdcntz  16617  dprddisj  16618  abveq0  17037  abvmul  17040  abvtri  17041  psgndiflemB  18158  phllmhm  18189  ipcj  18191  ipeq0  18195  mdetmul  18564  eltg2b  18699  iincld  18778  iuncld  18784  isclo2  18827  neips  18852  neipeltop  18868  lmcvg  19001  t1t0  19087  hauscmplem  19144  bwth  19148  1stcelcls  19200  ptuni2  19284  pttopon  19304  ptcld  19321  ptcnplem  19329  txtube  19348  txlm  19356  xkococnlem  19367  fbun  19548  isfil2  19564  ptcmplem4  19762  tmdcn2  19795  ustssel  19915  isucn2  19989  ucncn  19995  xmeteq0  20048  xmettri2  20050  metrest  20234  tngngp  20375  iscau4  20925  cmetcaulem  20934  caussi  20943  volfiniun  21164  iunmbl  21170  voliun  21171  mbfdm  21242  itg2seq  21356  itg2i1fseqle  21368  itg2i1fseq2  21370  iblcnlem  21402  limcresi  21496  limciun  21505  rolle  21598  ulmss  21998  rlimcnp  22495  midf  23269  colinearalg  23328  axpasch  23359  axeuclid  23381  axcontlem2  23383  axcontlem4  23385  axcontlem7  23388  axcontlem8  23389  nbgraf1olem1  23522  isgrpo  23855  grpoidinv  23867  grpoideu  23868  grpoidval  23875  grpoidinv2  23877  opidon  23981  exidu1  23985  grpomndo  24005  rngoideu  24043  rngodi  24044  rngodir  24045  rngoass  24046  rngoueqz  24089  vcid  24101  vcdi  24102  vcdir  24103  vcass  24104  nvs  24222  nvz  24229  nvtri  24230  ajmoi  24431  adjmo  25408  cnlnssadj  25656  mdbr3  25873  mdbr4  25874  mdsl1i  25897  dmdbr6ati  25999  dmdbr7ati  26000  disjunsn  26107  fnmptf  26148  xrge0infss  26224  hasheuni  26699  sigaclcu2  26728  prsiga  26739  measvunilem  26791  cntmeas  26805  signsply0  27116  cvmsdisj  27323  cvmshmeo  27324  cvmliftlem15  27351  cvmlift2lem12  27367  untangtr  27529  prodeq2  27591  elpotr  27758  dfon2lem7  27766  dfon2lem8  27767  tfisg  27829  wfisg  27834  frinsg  27870  poseq  27878  heicant  28594  ovoliunnfl  28601  voliunnfl  28603  volsupnfl  28604  opnrebl2  28684  fnemeet2  28756  fnejoin1  28757  fnejoin2  28758  frinfm  28797  caushft  28825  sstotbnd3  28843  prdstotbnd  28861  heibor1lem  28876  bfplem2  28890  rngohomadd  28943  rngohommul  28944  idladdcl  28987  idllmulcl  28988  idlrmulcl  28989  ispridl2  29006  mpt2bi123f  29143  iineq12f  29145  mptbi12f  29147  lerabdioph  29311  ltrabdioph  29314  nerabdioph  29315  dvdsrabdioph  29316  rencldnfi  29328  dford3  29545  ralbidar  29869  rexbidar  29870  stoweidlem60  30023  usgfiregdegfi  30696  1to3vfriendship  30768  frconngra  30781  frgraregorufr0  30813  usgreghash2spot  30830  mpt2exxg2  30896  fsuppmapnn0fiublem  30966  fsuppmapnn0fiub  30967  fsuppmapnn0fiubex  30968  mptnn0fsuppd  30971  scmatid  31081  pmatcollpw2lem  31284  bnj1498  32404  pmapglbx  33771  ltrnnid  34138  cdlemefrs32fva  34402
  Copyright terms: Public domain W3C validator