![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ralrimia | Structured version Visualization version GIF version |
Description: Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
Ref | Expression |
---|---|
ralrimia.1 | ⊢ Ⅎ𝑥𝜑 |
ralrimia.2 | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓) |
Ref | Expression |
---|---|
ralrimia | ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralrimia.1 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | ralrimia.2 | . . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓) | |
3 | 2 | ex 411 | . 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓)) |
4 | 1, 3 | ralrimi 3244 | 1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 Ⅎwnf 1777 ∈ wcel 2098 ∀wral 3050 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-12 2166 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-nf 1778 df-ral 3051 |
This theorem is referenced by: fompt 7131 ss2iundf 43263 ismnushort 43912 ssrabdf 44653 iunssdf 44698 rnmptssd 44740 dmmptdff 44767 axccd 44773 dmmptdf2 44777 mpteq12daOLD 44788 rnmptbd2lem 44794 rnmptssdf 44800 rnmptbdlem 44801 ralrnmpt3 44805 rnmptssbi 44807 fconst7 44811 fmptdff 44818 rnmptssdff 44822 infleinf2 44966 unb2ltle 44967 uzublem 44982 cvgcaule 45044 climinf3 45274 limsupequzlem 45280 limsupre3uzlem 45293 climisp 45304 climrescn 45306 climxrrelem 45307 climxrre 45308 climxlim2lem 45403 saliunclf 45880 meaiuninc3v 46042 fsupdm 46400 finfdm 46404 |
Copyright terms: Public domain | W3C validator |