Theorem ralrimiv 2578

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

Syntax hints:   → wi 4   ∈ wcel 2176  ∀wral 2484

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-ral 2489

This theorem is referenced by:  ralrimiva  2579  ralrimivw  2580  ralrimivv  2587  r19.27av  2641  rr19.3v  2912  rabssdv  3273  rzal  3558  trin  4152  class2seteq  4207  ralxfrALT  4514  ssorduni  4535  ordsucim  4548  onintonm  4565  issref  5065  funimaexglem  5357  resflem  5744  poxp  6318  rdgss  6469  dom2lem  6863  supisoti  7112  ordiso2  7137  updjud  7184  uzind  9484  zindd  9491  lbzbi  9737  icoshftf1o  10113  ccatrn  11065  maxabslemval  11519  xrmaxiflemval  11561  fisum0diag2  11758  alzdvds  12165  hashgcdeq  12562  ghmrn  13593  ghmpreima  13602  imasring  13826  01eq0ring  13951  islssmd  14121  tgcl  14536  distop  14557  neiuni  14633  cnpnei  14691  isxmetd  14819  fsumcncntop  15039  fsumdvdsmul  15463  bj-nntrans2  15892  bj-inf2vnlem1  15910