Theorem ralrimiv 2622

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ∀wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579

This proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533

This theorem is used by:  ralrimiva  2623  ralrimivw  2624  ralrimivv  2631  r19.27av  2686  rr19.3v  2965  rabssdv  3328  rzal  3625  trin  4239  class2seteq  4300  ralxfrALT  4613  ssorduni  4634  ordsucim  4647  onintonm  4664  issref  5170  funimaexglem  5464  resflem  5872  poxp  6468  rdgss  6654  dom2lem  7058  supisoti  7350  ordiso2  7375  updjud  7422  uzind  9757  zindd  9764  lbzbi  10016  icoshftf1o  10393  ccatrn  11377  ccatalpha  11381  maxabslemval  11974  xrmaxiflemval  12016  fisum0diag2  12214  alzdvds  12621  hashgcdeq  13018  ghmrn  14060  ghmpreima  14069  imasring  14369  01eq0ring  14496  islssmd  14696  tgcl  15165  distop  15186  neiuni  15262  cnpnei  15320  isxmetd  15448  fsumcncntop  15668  fsumdvdsmul  16105  uspgr2wlkeq  16606  clwwlkccatlem  16641  bj-nntrans2  16978  bj-inf2vnlem1  16996