Theorem ralrimiv 2614

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

Syntax hints:   → wi 4   ∈ wcel 2203  ∀wral 2520

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2525

This theorem is referenced by:  ralrimiva  2615  ralrimivw  2616  ralrimivv  2623  r19.27av  2678  rr19.3v  2956  rabssdv  3318  rzal  3607  trin  4218  class2seteq  4276  ralxfrALT  4588  ssorduni  4609  ordsucim  4622  onintonm  4639  issref  5145  funimaexglem  5439  resflem  5841  poxp  6428  rdgss  6614  dom2lem  7011  supisoti  7301  ordiso2  7326  updjud  7373  uzind  9689  zindd  9696  lbzbi  9948  icoshftf1o  10324  ccatrn  11297  ccatalpha  11301  maxabslemval  11893  xrmaxiflemval  11935  fisum0diag2  12133  alzdvds  12540  hashgcdeq  12937  ghmrn  13974  ghmpreima  13983  imasring  14208  01eq0ring  14334  islssmd  14507  tgcl  14929  distop  14950  neiuni  15026  cnpnei  15084  isxmetd  15212  fsumcncntop  15432  fsumdvdsmul  15859  uspgr2wlkeq  16360  clwwlkccatlem  16395  bj-nntrans2  16722  bj-inf2vnlem1  16740