Theorem ralrimiv 2604

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

Syntax hints:   → wi 4   ∈ wcel 2202  ∀wral 2510

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-ral 2515

This theorem is referenced by:  ralrimiva  2605  ralrimivw  2606  ralrimivv  2613  r19.27av  2668  rr19.3v  2945  rabssdv  3307  rzal  3592  trin  4197  class2seteq  4253  ralxfrALT  4564  ssorduni  4585  ordsucim  4598  onintonm  4615  issref  5119  funimaexglem  5413  resflem  5811  poxp  6397  rdgss  6549  dom2lem  6945  supisoti  7209  ordiso2  7234  updjud  7281  uzind  9591  zindd  9598  lbzbi  9850  icoshftf1o  10226  ccatrn  11190  ccatalpha  11194  maxabslemval  11786  xrmaxiflemval  11828  fisum0diag2  12026  alzdvds  12433  hashgcdeq  12830  ghmrn  13862  ghmpreima  13871  imasring  14096  01eq0ring  14222  islssmd  14392  tgcl  14807  distop  14828  neiuni  14904  cnpnei  14962  isxmetd  15090  fsumcncntop  15310  fsumdvdsmul  15734  uspgr2wlkeq  16235  clwwlkccatlem  16270  bj-nntrans2  16598  bj-inf2vnlem1  16616