Theorem ralimi 2527

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 2525	1 |- ( A. x e. A ph -> A. x e. A ps )

Syntax hints:   -> wi 4   e. wcel 2135   A.wral 2442

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

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

This theorem is referenced by:  2ralimi  2528  ral2imi  2529  r19.26  2590  r19.29  2601  rr19.3v  2860  rr19.28v  2861  reu3  2911  uniiunlem  3226  reupick2  3403  uniss2  3814  ss2iun  3875  iineq2  3877  iunss2  3905  disjss2  3956  disjeq2  3957  disjnim  3967  repizf  4092  abnexg  4418  reusv3i  4431  tfis  4554  ssrel2  4688  issref  4980  dmmptg  5095  funco  5222  fununi  5250  fun11uni  5252  funimaexglem  5265  fnmpt  5308  fun11iun  5447  mpteqb  5570  chfnrn  5590  dffo5  5628  ffvresb  5642  fmptcof  5646  dfmptg  5658  mpo2eqb  5942  ralrnmpo  5947  rexrnmpo  5948  fnmpo  6162  mpoexxg  6170  smores  6251  riinerm  6565  ixpm  6687  difinfinf  7057  exmidontriimlem1  7168  onntri13  7185  onntri24  7189  cc4f  7201  cc4n  7203  cauappcvgprlemdisj  7583  caucvgsrlemasr  7722  caucvgsr  7734  suplocsr  7741  rexuz3  10918  recvguniq  10923  cau3lem  11042  caubnd2  11045  rexanre  11148  climi2  11215  climi0  11216  climcaucn  11278  ndvdssub  11852  gcdsupex  11875  gcdsupcl  11876  bezoutlemmo  11924  eltg2b  12595  neipsm  12695  lmcvg  12758  txlm  12820  metrest  13047  mulcncflem  13131  bj-charfunbi  13528  bj-indint  13648  bj-indind  13649  bj-bdfindis  13664  setindis  13684  bdsetindis  13686