![]() |
Mathbox for Glauco Siliprandi |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > 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 402 | . 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓)) |
4 | 1, 3 | ralrimi 3136 | 1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 385 Ⅎwnf 1879 ∈ wcel 2157 ∀wral 3087 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-12 2213 |
This theorem depends on definitions: df-bi 199 df-an 386 df-ex 1876 df-nf 1880 df-ral 3092 |
This theorem is referenced by: ralimda 40071 funimaeq 40196 ralrnmpt3 40209 rnmptssbi 40212 fconst7 40219 infleinf2 40372 unb2ltle 40373 uzublem 40388 climinf3 40680 limsupequzlem 40686 limsupre3uzlem 40699 climisp 40710 climrescn 40712 climxrrelem 40713 climxrre 40714 climxlim2lem 40803 meaiuninc3v 41432 |
Copyright terms: Public domain | W3C validator |