Theorem ralrimiv 2504

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 1508	. 2 ⊢ Ⅎ𝑥𝜑
2		ralrimiv.1	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))
3	1, 2	ralrimi 2503	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∈ wcel 1480  ∀wral 2416

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 1423  ax-gen 1425  ax-4 1487  ax-17 1506

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-ral 2421

This theorem is referenced by:  ralrimiva  2505  ralrimivw  2506  ralrimivv  2513  r19.27av  2567  rr19.3v  2823  rabssdv  3177  rzal  3460  trin  4036  class2seteq  4087  ralxfrALT  4388  ssorduni  4403  ordsucim  4416  onintonm  4433  issref  4921  funimaexglem  5206  resflem  5584  poxp  6129  rdgss  6280  dom2lem  6666  supisoti  6897  ordiso2  6920  updjud  6967  uzind  9162  zindd  9169  lbzbi  9408  icoshftf1o  9774  maxabslemval  10980  xrmaxiflemval  11019  fisum0diag2  11216  alzdvds  11552  hashgcdeq  11904  tgcl  12233  distop  12254  neiuni  12330  cnpnei  12388  isxmetd  12516  fsumcncntop  12725  bj-nntrans2  13150  bj-inf2vnlem1  13168