Theorem ralrimiv 2616

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 2615	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2205  ∀wral 2522

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 2527

This theorem is referenced by:  ralrimiva  2617  ralrimivw  2618  ralrimivv  2625  r19.27av  2680  rr19.3v  2959  rabssdv  3322  rzal  3611  trin  4223  class2seteq  4281  ralxfrALT  4593  ssorduni  4614  ordsucim  4627  onintonm  4644  issref  5150  funimaexglem  5444  resflem  5846  poxp  6441  rdgss  6627  dom2lem  7024  supisoti  7314  ordiso2  7339  updjud  7386  uzind  9707  zindd  9714  lbzbi  9966  icoshftf1o  10343  ccatrn  11322  ccatalpha  11326  maxabslemval  11918  xrmaxiflemval  11960  fisum0diag2  12158  alzdvds  12565  hashgcdeq  12962  ghmrn  14010  ghmpreima  14019  imasring  14307  01eq0ring  14434  islssmd  14633  tgcl  15055  distop  15076  neiuni  15152  cnpnei  15210  isxmetd  15338  fsumcncntop  15558  fsumdvdsmul  15985  uspgr2wlkeq  16486  clwwlkccatlem  16521  bj-nntrans2  16848  bj-inf2vnlem1  16866