Theorem ralrimi 2613

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

Syntax hints:   → wi 4  ∀wal 1396  Ⅎwnf 1509   ∈ wcel 2203  ∀wral 2520

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 2525

This theorem is referenced by:  ralrimiv  2614  reximdai  2640  r19.12  2649  rexlimd  2657  rexlimd2  2658  r19.29af2  2683  r19.37  2695  ralidm  3609  iineq2d  4010  mpteq2da  4198  onintonm  4638  mpteqb  5767  fmptdf  5833  eusvobj2  6035  tfri3  6597  mapxpen  7100  fodjuomnilemdc  7434  cc3  7578  zsupcllemstep  10585  fimaxre2  11905  fprodcllemf  12292  fprodap0f  12315  fprodle  12319  bezoutlemmain  12687  bezoutlemzz  12691  exmidunben  13166  mulcncf  15460  limccnp2lem  15528  lfgrnloopen  16115