Theorem ralrimia 3236

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 412	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))
4	1, 3	ralrimi 3235	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∧ wa 395  Ⅎwnf 1785   ∈ wcel 2114  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-nf 1786  df-ral 3053

This theorem is referenced by:  funcnvmpt  6944  fompt  7065  vieta  33738  ss2iundf  43967  ismnushort  44609  modelaxreplem3  45288  ssrabdf  45426  ss2rabdf  45461  iunssdf  45467  rnmptssd  45507  dmmptdff  45534  axccd  45540  dmmptdf2  45544  rnmptbd2lem  45559  rnmptssdf  45565  rnmptbdlem  45566  ralrnmpt3  45570  rnmptssbi  45571  fconst7  45575  fmptdff  45582  rnmptssdff  45586  infleinf2  45725  unb2ltle  45726  uzublem  45741  cvgcaule  45802  climinf3  46027  limsupequzlem  46033  limsupre3uzlem  46046  climisp  46057  climrescn  46059  climxrrelem  46060  climxrre  46061  climxlim2lem  46156  dvnprodlem1  46257  saliunclf  46633  meaiuninc3v  46795  preimageiingt  47031  preimaleiinlt  47032  fsupdm  47153  finfdm  47157  iinfssc  49369  iinfsubc  49370