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 450 | . 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓)) |
4 | 1, 3 | ralrimi 2957 | 1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 Ⅎwnf 1708 ∈ wcel 1990 ∀wral 2912 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-12 2047 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 df-nf 1710 df-ral 2917 |
This theorem is referenced by: ralimda 39326 funimaeq 39461 ralrnmpt3 39474 rnmptssbi 39477 fconst7 39484 infleinf2 39641 unb2ltle 39642 uzublem 39657 climinf3 39948 limsupequzlem 39954 limsupre3uzlem 39967 climisp 39978 climrescn 39980 climxrrelem 39981 climxrre 39982 climxlim2lem 40071 |
Copyright terms: Public domain | W3C validator |