Theorem ralimi 2952

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

Step	Hyp	Ref	Expression
1		ralimi.1	. . 3 |- ( ph -> ps )
2	1	a1i 11	. 2 |- ( x e. A -> ( ph -> ps ) )
3	2	ralimia 2950	1 |- ( A. x e. A ph -> A. x e. A ps )

Syntax hints:   -> wi 4   e. wcel 1990   A.wral 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737

This theorem depends on definitions:  df-bi 197  df-ral 2917

This theorem is referenced by:  2ralimi  2953  r19.26  3064  r19.29  3072  rr19.3v  3345  rr19.28v  3346  reu3  3396  uniiunlem  3691  reupick2  3913  uniss2  4470  ss2iun  4536  iineq2  4538  iunss2  4565  disjss2  4623  disjeq2  4624  reusv2lem5  4873  issref  5509  dmmptg  5632  wfisg  5715  fununi  5964  fnmptf  6016  fnmpt  6020  mpteqb  6299  chfnrn  6328  fvn0ssdmfun  6350  dffo5  6376  ffvresb  6394  fmptcof  6397  mpt22eqb  6769  ralrnmpt2  6775  abnexg  6964  tfis  7054  fun11uni  7120  fun11iun  7126  zfrep6  7134  mpt2exxg  7244  el2mpt2csbcl  7250  frxp  7287  smores  7449  riiner  7820  ixpn0  7940  boxriin  7950  unifi2  8256  wemaplem2  8452  rankonidlem  8691  acni3  8870  dfac5  8951  dfac12lem2  8966  kmlem6  8977  kmlem8  8979  kmlem13  8984  cfsmolem  9092  fin23lem40  9173  isf32lem2  9176  fin1a2s  9236  hsmexlem2  9249  hsmex3  9256  axcc4  9261  domtriomlem  9264  dcomex  9269  ac6num  9301  iundom  9364  unirnfdomd  9389  konigthlem  9390  iunctb  9396  gch3  9498  wununi  9528  wunpw  9529  wunpr  9531  eltsk2g  9573  tskpwss  9574  tskpw  9575  grupw  9617  gruurn  9620  intgru  9636  grothpw  9648  grothpwex  9649  grothomex  9651  axgroth3  9653  suplem1pr  9874  supexpr  9876  supsr  9933  fimaxre3  10970  xrsupexmnf  12135  xrinfmexpnf  12136  fsuppmapnn0fiublem  12789  fsuppmapnn0fiub  12790  fsuppmapnn0fiubOLD  12791  fsuppmapnn0fiubex  12792  mptnn0fsuppd  12798  rexanre  14086  rexuz3  14088  cau3lem  14094  caubnd2  14097  caubnd  14098  rlim0  14239  rlim0lt  14240  climi2  14242  climi0  14243  climrlim2  14278  rlimres  14289  o1rlimmul  14349  caurcvg  14407  caurcvg2  14408  caucvg  14409  caucvgb  14410  sumeq2  14424  prodeq2  14644  ndvdssub  15133  gcdcllem1  15221  coprmproddvdslem  15376  vdwnnlem1  15699  imasaddfnlem  16188  catidex  16335  catlid  16344  catrid  16345  catcocl  16346  catpropd  16369  subcidcl  16504  funcid  16530  setcepi  16738  tsrss  17223  mgmidmo  17259  gsumval2  17280  isnmnd  17298  issubg2  17609  gagrpid  17727  gaass  17730  dprdcntz  18407  dprddisj  18408  abveq0  18826  abvmul  18829  abvtri  18830  psgndiflemB  19946  phllmhm  19977  ipcj  19979  ipeq0  19983  mdetmul  20429  pmatcollpw2lem  20582  eltg2b  20763  iincld  20843  iuncld  20849  isclo2  20892  neips  20917  neipeltop  20933  lmcvg  21066  t1t0  21152  hauscmplem  21209  bwth  21213  1stcelcls  21264  ptuni2  21379  pttopon  21399  ptcld  21416  ptcnplem  21424  txtube  21443  txlm  21451  xkococnlem  21462  fbun  21644  isfil2  21660  ptcmplem4  21859  ustssel  22009  isucn2  22083  ucncn  22089  metrest  22329  tngngp  22458  tngngp3  22460  ncvsi  22951  iscau4  23077  cmetcaulem  23086  caussi  23095  volfiniun  23315  iunmbl  23321  voliun  23322  mbfdm  23395  itg2seq  23509  itg2i1fseqle  23521  itg2i1fseq2  23523  iblcnlem  23555  limcresi  23649  limciun  23658  rolle  23753  ulmss  24151  rlimcnp  24692  colinearalg  25790  axpasch  25821  axeuclid  25843  axcontlem2  25845  axcontlem4  25847  axcontlem7  25850  axcontlem8  25851  fusgrregdegfi  26465  0grrgr  26476  rusgr1vtxlem  26483  wlkvtxeledg  26519  wlkdlem3  26581  wlkdlem4  26582  lfgriswlk  26585  lfgrwlknloop  26586  eulercrct  27102  1to3vfriendship  27145  frgrregorufr0  27188  isgrpo  27351  grpoidinv  27362  grpoideu  27363  grpoidval  27367  grpoidinv2  27369  vcidOLD  27419  vcdi  27420  vcdir  27421  vcass  27422  nvs  27518  nvz  27524  nvtri  27525  mdbr3  29156  mdbr4  29157  mdsl1i  29180  dmdbr6ati  29282  dmdbr7ati  29283  disjunsn  29407  hasheuni  30147  sigaclcu2  30183  prsiga  30194  measvunilem  30275  cntmeas  30289  omssubadd  30362  signsply0  30628  bnj1498  31129  cvmsdisj  31252  cvmshmeo  31253  cvmliftlem15  31280  cvmlift2lem12  31296  untangtr  31591  elpotr  31686  dfon2lem7  31694  dfon2lem8  31695  tfisg  31716  frinsg  31742  poseq  31750  opnrebl2  32316  fnemeet2  32362  fnejoin1  32363  fnejoin2  32364  dfgcd3  33170  ptrecube  33409  poimirlem25  33434  poimirlem26  33435  poimirlem27  33436  poimirlem30  33439  poimirlem31  33440  poimirlem32  33441  heicant  33444  ovoliunnfl  33451  voliunnfl  33453  volsupnfl  33454  frinfm  33530  caushft  33557  sstotbnd3  33575  prdstotbnd  33593  heibor1lem  33608  bfplem2  33622  opidonOLD  33651  exidu1  33655  grpomndo  33674  rngoideu  33702  rngodi  33703  rngodir  33704  rngoass  33705  rngoueqz  33739  idladdcl  33818  idllmulcl  33819  idlrmulcl  33820  mpt2bi123f  33971  iineq12f  33973  mptbi12f  33975  pmapglbx  35055  ltrnnid  35422  cdlemefrs32fva  35688  lerabdioph  37369  ltrabdioph  37372  nerabdioph  37373  dvdsrabdioph  37374  rencldnfi  37385  dford3  37595  pwelg  37865  pwinfi2  37867  ss2iundf  37951  neik0imk0p  38334  gneispace  38432  gneispace0nelrn  38438  ralbidar  38649  rexbidar  38650  uzubico2  39797  climuzlem  39975  xlimxrre  40057  bgoldbtbndlem2  41694  bgoldbtbndlem4  41696  mpt2exxg2  42116  iunord  42422