Theorem ralrimiv 2622

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ∀wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579

This proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533

This theorem is used by:  ralrimiva  2623  ralrimivw  2624  ralrimivv  2631  r19.27av  2686  rr19.3v  2965  rabssdv  3328  rzal  3625  trin  4239  class2seteq  4300  ralxfrALT  4613  ssorduni  4634  ordsucim  4647  onintonm  4664  issref  5170  funimaexglem  5464  resflem  5872  poxp  6468  rdgss  6654  dom2lem  7058  supisoti  7351  ordiso2  7376  updjud  7423  uzind  9762  zindd  9769  lbzbi  10026  icoshftf1o  10404  ccatrn  11393  ccatalpha  11397  maxabslemval  11991  xrmaxiflemval  12035  fisum0diag2  12233  alzdvds  12640  hashgcdeq  13041  ghmrn  14113  ghmpreima  14122  cntz2ss  14162  imasring  14453  01eq0ring  14580  islssmd  14780  tgcl  15256  distop  15277  neiuni  15353  cnpnei  15411  isxmetd  15539  fsumcncntop  15759  fsumdvdsmul  16246  uspgr2wlkeq  16772  clwwlkccatlem  16807  bj-nntrans2  17144  bj-inf2vnlem1  17162