Theorem ralrimiv 2605

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

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

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2516

This theorem is referenced by:  ralrimiva  2606  ralrimivw  2607  ralrimivv  2614  r19.27av  2669  rr19.3v  2946  rabssdv  3308  rzal  3594  trin  4202  class2seteq  4259  ralxfrALT  4570  ssorduni  4591  ordsucim  4604  onintonm  4621  issref  5126  funimaexglem  5420  resflem  5819  poxp  6406  rdgss  6592  dom2lem  6988  supisoti  7252  ordiso2  7277  updjud  7324  uzind  9635  zindd  9642  lbzbi  9894  icoshftf1o  10270  ccatrn  11235  ccatalpha  11239  maxabslemval  11831  xrmaxiflemval  11873  fisum0diag2  12071  alzdvds  12478  hashgcdeq  12875  ghmrn  13907  ghmpreima  13916  imasring  14141  01eq0ring  14267  islssmd  14438  tgcl  14858  distop  14879  neiuni  14955  cnpnei  15013  isxmetd  15141  fsumcncntop  15361  fsumdvdsmul  15788  uspgr2wlkeq  16289  clwwlkccatlem  16324  bj-nntrans2  16651  bj-inf2vnlem1  16669