Theorem ralrimiv 2566

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

Syntax hints:   → wi 4   ∈ wcel 2164  ∀wral 2472

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2477

This theorem is referenced by:  ralrimiva  2567  ralrimivw  2568  ralrimivv  2575  r19.27av  2629  rr19.3v  2899  rabssdv  3259  rzal  3544  trin  4137  class2seteq  4192  ralxfrALT  4498  ssorduni  4519  ordsucim  4532  onintonm  4549  issref  5048  funimaexglem  5337  resflem  5722  poxp  6285  rdgss  6436  dom2lem  6826  supisoti  7069  ordiso2  7094  updjud  7141  uzind  9428  zindd  9435  lbzbi  9681  icoshftf1o  10057  maxabslemval  11352  xrmaxiflemval  11393  fisum0diag2  11590  alzdvds  11996  hashgcdeq  12377  ghmrn  13327  ghmpreima  13336  imasring  13560  01eq0ring  13685  islssmd  13855  tgcl  14232  distop  14253  neiuni  14329  cnpnei  14387  isxmetd  14515  fsumcncntop  14724  bj-nntrans2  15444  bj-inf2vnlem1  15462