Theorem ralrimiv 2542

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

Syntax hints:   → wi 4   ∈ wcel 2141  ∀wral 2448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-ral 2453

This theorem is referenced by:  ralrimiva  2543  ralrimivw  2544  ralrimivv  2551  r19.27av  2605  rr19.3v  2869  rabssdv  3227  rzal  3511  trin  4095  class2seteq  4147  ralxfrALT  4450  ssorduni  4469  ordsucim  4482  onintonm  4499  issref  4991  funimaexglem  5279  resflem  5657  poxp  6208  rdgss  6359  dom2lem  6746  supisoti  6983  ordiso2  7008  updjud  7055  uzind  9310  zindd  9317  lbzbi  9562  icoshftf1o  9935  maxabslemval  11159  xrmaxiflemval  11200  fisum0diag2  11397  alzdvds  11801  hashgcdeq  12180  tgcl  12779  distop  12800  neiuni  12876  cnpnei  12934  isxmetd  13062  fsumcncntop  13271  bj-nntrans2  13909  bj-inf2vnlem1  13927