Theorem ralrimiv 2536

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Nov-1994.)

Hypothesis

Ref	Expression
ralrimiv.1	⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))

Assertion

Ref	Expression
ralrimiv	⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem ralrimiv

Step	Hyp	Ref	Expression
1		nfv 1515	. 2 ⊢ Ⅎ𝑥𝜑
2		ralrimiv.1	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))
3	1, 2	ralrimi 2535	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2135  ∀wral 2442

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1434  ax-gen 1436  ax-4 1497  ax-17 1513

This theorem depends on definitions:  df-bi 116  df-nf 1448  df-ral 2447

This theorem is referenced by:  ralrimiva  2537  ralrimivw  2538  ralrimivv  2545  r19.27av  2599  rr19.3v  2860  rabssdv  3217  rzal  3501  trin  4084  class2seteq  4136  ralxfrALT  4439  ssorduni  4458  ordsucim  4471  onintonm  4488  issref  4980  funimaexglem  5265  resflem  5643  poxp  6191  rdgss  6342  dom2lem  6729  supisoti  6966  ordiso2  6991  updjud  7038  uzind  9293  zindd  9300  lbzbi  9545  icoshftf1o  9918  maxabslemval  11136  xrmaxiflemval  11177  fisum0diag2  11374  alzdvds  11777  hashgcdeq  12148  tgcl  12605  distop  12626  neiuni  12702  cnpnei  12760  isxmetd  12888  fsumcncntop  13097  bj-nntrans2  13669  bj-inf2vnlem1  13687