Theorem ralrimiv 2434

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

Syntax hints:   → wi 4   ∈ wcel 1434  ∀wral 2349

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-4 1441  ax-17 1460

This theorem depends on definitions:  df-bi 115  df-nf 1391  df-ral 2354

This theorem is referenced by:  ralrimiva  2435  ralrimivw  2436  ralrimivv  2443  r19.27av  2493  rr19.3v  2734  rabssdv  3075  rzal  3346  trin  3893  class2seteq  3945  ralxfrALT  4225  ssorduni  4239  ordsucim  4252  onintonm  4269  issref  4737  funimaexglem  5013  poxp  5884  rdgss  6032  dom2lem  6319  supisoti  6482  ordiso2  6505  uzind  8539  zindd  8546  lbzbi  8782  icoshftf1o  9089  maxabslemval  10232  alzdvds  10399  bj-nntrans2  10905  bj-inf2vnlem1  10923