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

Syntax hints:   → wi 4   ∈ wcel 2209  ∀wral 2528

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579

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

This theorem is referenced by:  ralrimiva  2623  ralrimivw  2624  ralrimivv  2631  r19.27av  2686  rr19.3v  2965  rabssdv  3328  rzal  3622  trin  4234  class2seteq  4295  ralxfrALT  4608  ssorduni  4629  ordsucim  4642  onintonm  4659  issref  5165  funimaexglem  5459  resflem  5863  poxp  6458  rdgss  6644  dom2lem  7048  supisoti  7340  ordiso2  7365  updjud  7412  uzind  9736  zindd  9743  lbzbi  9995  icoshftf1o  10372  ccatrn  11355  ccatalpha  11359  maxabslemval  11952  xrmaxiflemval  11994  fisum0diag2  12192  alzdvds  12599  hashgcdeq  12996  ghmrn  14037  ghmpreima  14046  imasring  14342  01eq0ring  14469  islssmd  14668  tgcl  15088  distop  15109  neiuni  15185  cnpnei  15243  isxmetd  15371  fsumcncntop  15591  fsumdvdsmul  16019  uspgr2wlkeq  16520  clwwlkccatlem  16555  bj-nntrans2  16892  bj-inf2vnlem1  16910