Theorem ralrimiv 2562

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

Syntax hints:   → wi 4   ∈ wcel 2160  ∀wral 2468

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 2473

This theorem is referenced by:  ralrimiva  2563  ralrimivw  2564  ralrimivv  2571  r19.27av  2625  rr19.3v  2891  rabssdv  3250  rzal  3535  trin  4126  class2seteq  4181  ralxfrALT  4485  ssorduni  4504  ordsucim  4517  onintonm  4534  issref  5029  funimaexglem  5318  resflem  5701  poxp  6258  rdgss  6409  dom2lem  6799  supisoti  7040  ordiso2  7065  updjud  7112  uzind  9395  zindd  9402  lbzbi  9648  icoshftf1o  10023  maxabslemval  11252  xrmaxiflemval  11293  fisum0diag2  11490  alzdvds  11895  hashgcdeq  12274  ghmrn  13213  ghmpreima  13222  imasring  13431  01eq0ring  13553  islssmd  13692  tgcl  14041  distop  14062  neiuni  14138  cnpnei  14196  isxmetd  14324  fsumcncntop  14533  bj-nntrans2  15182  bj-inf2vnlem1  15200