Theorem ralrimi 2456

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

Syntax hints:   → wi 4  ∀wal 1294  Ⅎwnf 1401   ∈ wcel 1445  ∀wral 2370

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-4 1452

This theorem depends on definitions:  df-bi 116  df-nf 1402  df-ral 2375

This theorem is referenced by:  ralrimiv  2457  reximdai  2483  r19.12  2491  rexlimd  2499  rexlimd2  2500  r19.29af2  2522  r19.37  2533  ralidm  3402  iineq2d  3772  mpteq2da  3949  onintonm  4362  mpteqb  5429  fmptdf  5494  eusvobj2  5676  tfri3  6170  mapxpen  6644  fodjuomnilemdc  6887  fimaxre2  10789  zsupcllemstep  11383  bezoutlemmain  11429  bezoutlemzz  11433