Theorem ralimi 2378

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	⊢ (∀x ∈ A φ → ∀x ∈ A ψ)

Proof of Theorem ralimi

Step	Hyp	Ref	Expression
1		ralimi.1	. . 3 ⊢ (φ → ψ)
2	1	a1i 9	. 2 ⊢ (x ∈ A → (φ → ψ))
3	2	ralimia 2376	1 ⊢ (∀x ∈ A φ → ∀x ∈ A ψ)

Syntax hints:   → wi 4   ∈ wcel 1390  ∀wral 2300

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335

This theorem depends on definitions:  df-bi 110  df-ral 2305

This theorem is referenced by:  ral2imi  2379  r19.26  2435  r19.29  2444  rr19.3v  2676  rr19.28v  2677  reu3  2725  uniiunlem  3022  reupick2  3217  uniss2  3602  ss2iun  3663  iineq2  3665  iunss2  3693  disjss2  3739  disjeq2  3740  repizf  3864  reusv3i  4157  tfis  4249  ssrel2  4373  issref  4650  dmmptg  4761  funco  4883  fununi  4910  fun11uni  4912  funimaexglem  4925  fnmpt  4968  fun11iun  5090  mpteqb  5204  chfnrn  5221  dffo5  5259  ffvresb  5271  fmptcof  5274  dfmptg  5285  mpt22eqb  5552  ralrnmpt2  5557  rexrnmpt2  5558  fnmpt2  5770  mpt2exxg  5775  smores  5848  riinerm  6115  cauappcvgprlemdisj  6623  bj-indint  9390  bj-indind  9391  bj-bdfindis  9407  setindis  9427  bdsetindis  9429