Theorem ralrimi 2601

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

Syntax hints:   → wi 4  ∀wal 1393  Ⅎwnf 1506   ∈ wcel 2200  ∀wral 2508

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 1493  ax-gen 1495  ax-4 1556

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513

This theorem is referenced by:  ralrimiv  2602  reximdai  2628  r19.12  2637  rexlimd  2645  rexlimd2  2646  r19.29af2  2671  r19.37  2683  ralidm  3593  iineq2d  3988  mpteq2da  4176  onintonm  4613  mpteqb  5733  fmptdf  5800  eusvobj2  5999  tfri3  6528  mapxpen  7029  fodjuomnilemdc  7334  cc3  7477  zsupcllemstep  10479  fimaxre2  11778  fprodcllemf  12164  fprodap0f  12187  fprodle  12191  bezoutlemmain  12559  bezoutlemzz  12563  exmidunben  13037  mulcncf  15322  limccnp2lem  15390  lfgrnloopen  15972