Theorem ralimi 2469

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 9	. 2 |- ( x e. A -> ( ph -> ps ) )
3	2	ralimia 2467	1 |- ( A. x e. A ph -> A. x e. A ps )

Syntax hints:   -> wi 4   e. wcel 1463   A.wral 2390

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408

This theorem depends on definitions:  df-bi 116  df-ral 2395

This theorem is referenced by:  2ralimi  2470  ral2imi  2471  r19.26  2532  r19.29  2543  rr19.3v  2793  rr19.28v  2794  reu3  2843  uniiunlem  3151  reupick2  3328  uniss2  3733  ss2iun  3794  iineq2  3796  iunss2  3824  disjss2  3875  disjeq2  3876  disjnim  3886  repizf  4004  abnexg  4327  reusv3i  4340  tfis  4457  ssrel2  4589  issref  4879  dmmptg  4994  funco  5121  fununi  5149  fun11uni  5151  funimaexglem  5164  fnmpt  5207  fun11iun  5344  mpteqb  5465  chfnrn  5485  dffo5  5523  ffvresb  5537  fmptcof  5541  dfmptg  5553  mpo2eqb  5834  ralrnmpo  5839  rexrnmpo  5840  fnmpo  6054  mpoexxg  6062  smores  6143  riinerm  6456  ixpm  6578  difinfinf  6938  cauappcvgprlemdisj  7407  caucvgsrlemasr  7532  caucvgsr  7544  rexuz3  10654  recvguniq  10659  cau3lem  10778  caubnd2  10781  rexanre  10884  climi2  10949  climi0  10950  climcaucn  11012  ndvdssub  11475  gcdsupex  11494  gcdsupcl  11495  bezoutlemmo  11540  eltg2b  12066  neipsm  12166  lmcvg  12228  txlm  12290  metrest  12495  mulcncflem  12576  bj-indint  12819  bj-indind  12820  bj-bdfindis  12835  setindis  12855  bdsetindis  12857