| 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 412 | . 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓)) |
| 4 | 1, 3 | ralrimi 3257 | 1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 Ⅎwnf 1783 ∈ wcel 2108 ∀wral 3061 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-12 2177 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-nf 1784 df-ral 3062 |
| This theorem is referenced by: fompt 7138 ss2iundf 43672 ismnushort 44320 modelaxreplem3 44997 ssrabdf 45120 iunssdf 45161 rnmptssd 45201 dmmptdff 45228 axccd 45234 dmmptdf2 45238 mpteq12daOLD 45249 rnmptbd2lem 45255 rnmptssdf 45261 rnmptbdlem 45262 ralrnmpt3 45266 rnmptssbi 45267 fconst7 45271 fmptdff 45278 rnmptssdff 45282 infleinf2 45425 unb2ltle 45426 uzublem 45441 cvgcaule 45502 climinf3 45731 limsupequzlem 45737 limsupre3uzlem 45750 climisp 45761 climrescn 45763 climxrrelem 45764 climxrre 45765 climxlim2lem 45860 dvnprodlem1 45961 saliunclf 46337 meaiuninc3v 46499 fsupdm 46857 finfdm 46861 |
| Copyright terms: Public domain | W3C validator |