Theorem ralrimi 2577

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

Syntax hints:   → wi 4  ∀wal 1371  Ⅎwnf 1483   ∈ wcel 2176  ∀wral 2484

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 1470  ax-gen 1472  ax-4 1533

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-ral 2489

This theorem is referenced by:  ralrimiv  2578  reximdai  2604  r19.12  2612  rexlimd  2620  rexlimd2  2621  r19.29af2  2646  r19.37  2658  ralidm  3561  iineq2d  3947  mpteq2da  4133  onintonm  4565  mpteqb  5670  fmptdf  5737  eusvobj2  5930  tfri3  6453  mapxpen  6945  fodjuomnilemdc  7246  cc3  7380  zsupcllemstep  10372  fimaxre2  11538  fprodcllemf  11924  fprodap0f  11947  fprodle  11951  bezoutlemmain  12319  bezoutlemzz  12323  exmidunben  12797  mulcncf  15080  limccnp2lem  15148