Theorem ralrimiv 2569

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

Syntax hints:   → wi 4   ∈ wcel 2167  ∀wral 2475

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-ral 2480

This theorem is referenced by:  ralrimiva  2570  ralrimivw  2571  ralrimivv  2578  r19.27av  2632  rr19.3v  2903  rabssdv  3264  rzal  3549  trin  4142  class2seteq  4197  ralxfrALT  4503  ssorduni  4524  ordsucim  4537  onintonm  4554  issref  5053  funimaexglem  5342  resflem  5729  poxp  6299  rdgss  6450  dom2lem  6840  supisoti  7085  ordiso2  7110  updjud  7157  uzind  9456  zindd  9463  lbzbi  9709  icoshftf1o  10085  maxabslemval  11392  xrmaxiflemval  11434  fisum0diag2  11631  alzdvds  12038  hashgcdeq  12435  ghmrn  13465  ghmpreima  13474  imasring  13698  01eq0ring  13823  islssmd  13993  tgcl  14408  distop  14429  neiuni  14505  cnpnei  14563  isxmetd  14691  fsumcncntop  14911  fsumdvdsmul  15335  bj-nntrans2  15706  bj-inf2vnlem1  15724