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  7269  ordiso2  7294  updjud  7341  uzind  9652  zindd  9659  lbzbi  9911  icoshftf1o  10287  ccatrn  11252  ccatalpha  11256  maxabslemval  11848  xrmaxiflemval  11890  fisum0diag2  12088  alzdvds  12495  hashgcdeq  12892  ghmrn  13924  ghmpreima  13933  imasring  14158  01eq0ring  14284  islssmd  14455  tgcl  14875  distop  14896  neiuni  14972  cnpnei  15030  isxmetd  15158  fsumcncntop  15378  fsumdvdsmul  15805  uspgr2wlkeq  16306  clwwlkccatlem  16341  bj-nntrans2  16668  bj-inf2vnlem1  16686