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  3612  iineq2d  4013  mpteq2da  4201  onintonm  4641  mpteqb  5770  fmptdf  5836  eusvobj2  6038  tfri3  6600  mapxpen  7103  fodjuomnilemdc  7437  cc3  7584  zsupcllemstep  10593  fimaxre2  11916  fprodcllemf  12303  fprodap0f  12326  fprodle  12330  bezoutlemmain  12698  bezoutlemzz  12702  exmidunben  13194  mulcncf  15490  limccnp2lem  15558  lfgrnloopen  16145