Theorem ralrimia 3265

Description: Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). (Contributed by Glauco Siliprandi, 23-Oct-2021.)

Hypotheses

Ref	Expression
ralrimia.1	⊢ Ⅎ𝑥𝜑
ralrimia.2	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓)

Assertion

Ref	Expression
ralrimia	⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Proof of Theorem ralrimia

Step	Hyp	Ref	Expression
1		ralrimia.1	. 2 ⊢ Ⅎ𝑥𝜑
2		ralrimia.2	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓)
3	2	ex 418	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))
4	1, 3	ralrimi 3264	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  Ⅎwnf 1816   ∈ wcel 2147  ∀wral 3080

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-12 2216

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-ral 3081

This theorem is used by:  ralimdaa  3267  iineq2d  4978  funcnvmpt  7015  fompt  7139  rnmptssd  7145  foresf1o  33169  vieta  34279  reff  34538  omssubadd  34999  srepdflem2  36085  srepdf  36086  mh-inf3f1  37506  ss2iundf  44849  ismnushort  45475  modelaxreplem3  46163  ssrabdf  46333  ss2rabdf  46368  iunssdf  46374  dmmptdff  46439  axccd  46444  dmmptdf2  46448  rnmptbd2lem  46463  rnmptssdf  46469  rnmptbdlem  46470  ralrnmpt3  46474  rnmptssbi  46475  fconst7  46479  fmptdff  46486  rnmptssdff  46490  infleinf2  46627  unb2ltle  46628  uzublem  46643  cvgcaule  46704  climinf3  46929  limsupequzlem  46935  limsupre3uzlem  46948  climisp  46959  climrescn  46961  climxrrelem  46962  climxrre  46963  climxlim2lem  47058  dvnprodlem1  47159  fourierdlem113  47432  saliunclf  47535  meaiuninc3v  47697  preimageiingt  47933  preimaleiinlt  47934  fsupdm  48055  finfdm  48059  iinfssc  50374  iinfsubc  50375