Theorem ralimi 2533

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

Syntax hints:   -> wi 4   e. wcel 2141   A.wral 2448

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 1440  ax-gen 1442

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

This theorem is referenced by:  2ralimi  2534  ral2imi  2535  r19.26  2596  r19.29  2607  rr19.3v  2869  rr19.28v  2870  reu3  2920  uniiunlem  3236  reupick2  3413  uniss2  3825  ss2iun  3886  iineq2  3888  iunss2  3916  disjss2  3967  disjeq2  3968  disjnim  3978  repizf  4103  abnexg  4429  reusv3i  4442  tfis  4565  ssrel2  4699  issref  4991  dmmptg  5106  funco  5236  fununi  5264  fun11uni  5266  funimaexglem  5279  fnmpt  5322  fun11iun  5461  mpteqb  5584  chfnrn  5604  dffo5  5642  ffvresb  5656  fmptcof  5660  dfmptg  5672  mpo2eqb  5959  ralrnmpo  5964  rexrnmpo  5965  fnmpo  6178  mpoexxg  6186  smores  6268  riinerm  6582  ixpm  6704  difinfinf  7074  exmidontriimlem1  7185  onntri13  7202  onntri24  7206  cc4f  7218  cc4n  7220  cauappcvgprlemdisj  7600  caucvgsrlemasr  7739  caucvgsr  7751  suplocsr  7758  rexuz3  10941  recvguniq  10946  cau3lem  11065  caubnd2  11068  rexanre  11171  climi2  11238  climi0  11239  climcaucn  11301  ndvdssub  11876  gcdsupex  11899  gcdsupcl  11900  bezoutlemmo  11948  mgmidmo  12612  eltg2b  12769  neipsm  12869  lmcvg  12932  txlm  12994  metrest  13221  mulcncflem  13305  bj-charfunbi  13768  bj-indint  13888  bj-indind  13889  bj-bdfindis  13904  setindis  13924  bdsetindis  13926