Theorem ralimi 2570

Description: Inference quantifying both antecedent and consequent, with strong hypothesis. (Contributed by NM, 4-Mar-1997.)

Hypothesis

Ref	Expression
ralimi.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ralimi	⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Proof of Theorem ralimi

Step	Hyp	Ref	Expression
1		ralimi.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	a1i 9	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))
3	2	ralimia 2568	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2177  ∀wral 2485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1471  ax-gen 1473

This theorem depends on definitions:  df-bi 117  df-ral 2490

This theorem is referenced by:  2ralimi  2571  ral2imi  2572  r19.26  2633  r19.29  2644  rr19.3v  2916  rr19.28v  2917  reu3  2967  uniiunlem  3286  reupick2  3463  uniss2  3886  ss2iun  3947  iineq2  3949  iunss2  3977  disjss2  4029  disjeq2  4030  disjnim  4040  repizf  4167  abnexg  4500  reusv3i  4513  tfis  4638  ssrel2  4772  issref  5073  dmmptg  5188  funco  5319  fununi  5350  fun11uni  5352  funimaexglem  5365  fnmpt  5411  fun11iun  5554  mpteqb  5682  chfnrn  5703  dffo5  5741  ffvresb  5755  fmptcof  5759  dfmptg  5771  mpo2eqb  6067  ralrnmpo  6072  rexrnmpo  6073  uchoice  6235  fnmpo  6300  mpoexxg  6308  smores  6390  riinerm  6707  ixpm  6829  difinfinf  7217  nninfwlpoimlemginf  7292  exmidontriimlem1  7348  onntri13  7365  onntri24  7369  cc4f  7396  cc4n  7398  cauappcvgprlemdisj  7779  caucvgsrlemasr  7918  caucvgsr  7930  suplocsr  7937  rexuz3  11371  recvguniq  11376  cau3lem  11495  caubnd2  11498  rexanre  11601  climi2  11669  climi0  11670  climcaucn  11732  ndvdssub  12311  gcdsupex  12348  gcdsupcl  12349  bezoutlemmo  12397  ptex  13166  mgmidmo  13274  issubg2m  13595  eltg2b  14596  neipsm  14696  lmcvg  14759  txlm  14821  metrest  15048  mulcncflem  15149  bj-charfunbi  15881  bj-indint  16001  bj-indind  16002  bj-bdfindis  16017  setindis  16037  bdsetindis  16039  neap0mkv  16143