Theorem ralrimi 2615

Description: Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 10-Oct-1999.)

Hypotheses

Ref	Expression
ralrimi.1	⊢ Ⅎ𝑥𝜑
ralrimi.2	⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))

Assertion

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

Proof of Theorem ralrimi

Step	Hyp	Ref	Expression
1		ralrimi.1	. . 3 ⊢ Ⅎ𝑥𝜑
2		ralrimi.2	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))
3	1, 2	alrimi 1571	. 2 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))
4		df-ral 2527	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))
5	3, 4	sylibr 134	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4  ∀wal 1396  Ⅎwnf 1509   ∈ wcel 2205  ∀wral 2522

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 1496  ax-gen 1498  ax-4 1559

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2527

This theorem is referenced by:  ralrimiv  2616  reximdai  2642  r19.12  2651  rexlimd  2659  rexlimd2  2660  r19.29af2  2685  r19.37  2697  ralidm  3614  iineq2d  4016  mpteq2da  4204  onintonm  4644  mpteqb  5773  fmptdf  5839  eusvobj2  6044  funimass4f  6332  tfri3  6611  mapxpen  7114  fodjuomnilemdc  7448  cc3  7598  zsupcllemstep  10614  fimaxre2  11940  fprodcllemf  12327  fprodap0f  12350  fprodle  12354  bezoutlemmain  12722  bezoutlemzz  12726  exmidunben  13264  mulcncf  15602  limccnp2lem  15670  lfgrnloopen  16257