Theorem ralrimi 2621

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1400  Ⅎwnf 1513   ∈ wcel 2209  ∀wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563

This proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533

This theorem is used by:  ralrimiv  2622  reximdai  2648  r19.12  2657  rexlimd  2665  rexlimd2  2666  r19.29af2  2691  r19.37  2703  ralidm  3628  iineq2d  4032  mpteq2da  4222  onintonm  4666  mpteqb  5799  fmptdf  5868  eusvobj2  6074  funimass4f  6363  tfri3  6642  mapxpen  7153  fodjuomnilemdc  7491  cc3  7641  zsupcllemstep  10680  fimaxre2  12017  fprodcllemf  12406  fprodap0f  12429  fprodle  12433  bezoutlemmain  12801  bezoutlemzz  12805  exmidunben  13376  gsumsnfdcmn  14258  mulcncf  15846  limccnp2lem  15914  lfgrnloopen  16591