Theorem ralrimi 2603

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 1570	. 2 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))
4		df-ral 2515	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))
5	3, 4	sylibr 134	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4  ∀wal 1395  Ⅎwnf 1508   ∈ wcel 2202  ∀wral 2510

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 1495  ax-gen 1497  ax-4 1558

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-ral 2515

This theorem is referenced by:  ralrimiv  2604  reximdai  2630  r19.12  2639  rexlimd  2647  rexlimd2  2648  r19.29af2  2673  r19.37  2685  ralidm  3595  iineq2d  3990  mpteq2da  4178  onintonm  4615  mpteqb  5737  fmptdf  5804  eusvobj2  6004  tfri3  6533  mapxpen  7034  fodjuomnilemdc  7343  cc3  7487  zsupcllemstep  10489  fimaxre2  11788  fprodcllemf  12175  fprodap0f  12198  fprodle  12202  bezoutlemmain  12570  bezoutlemzz  12574  exmidunben  13048  mulcncf  15334  limccnp2lem  15402  lfgrnloopen  15986