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 413 | . 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓)) |
4 | 1, 3 | ralrimi 3213 | 1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 Ⅎwnf 1775 ∈ wcel 2105 ∀wral 3135 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-12 2167 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-nf 1776 df-ral 3140 |
This theorem is referenced by: ralimda 41282 rnmptssd 41334 rnmpt0 41359 dmmptdf 41364 axccd 41371 dmmptdf2 41379 mpteq12da 41389 rnmptbd2lem 41396 rnmptssdf 41402 rnmptbdlem 41403 ralrnmpt3 41407 rnmptssbi 41410 fconst7 41415 infleinf2 41564 unb2ltle 41565 uzublem 41580 climinf3 41873 limsupequzlem 41879 limsupre3uzlem 41892 climisp 41903 climrescn 41905 climxrrelem 41906 climxrre 41907 climxlim2lem 42002 meaiuninc3v 42643 |
Copyright terms: Public domain | W3C validator |