Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ralrimi | GIF version |
Description: Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 10-Oct-1999.) |
Ref | Expression |
---|---|
ralrimi.1 | ⊢ Ⅎ𝑥𝜑 |
ralrimi.2 | ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓)) |
Ref | Expression |
---|---|
ralrimi | ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralrimi.1 | . . 3 ⊢ Ⅎ𝑥𝜑 | |
2 | ralrimi.2 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓)) | |
3 | 1, 2 | alrimi 1455 | . 2 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) |
4 | df-ral 2353 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) | |
5 | 3, 4 | sylibr 132 | 1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1282 Ⅎwnf 1389 ∈ wcel 1433 ∀wral 2348 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1376 ax-gen 1378 ax-4 1440 |
This theorem depends on definitions: df-bi 115 df-nf 1390 df-ral 2353 |
This theorem is referenced by: ralrimiv 2433 reximdai 2459 r19.12 2466 rexlimd 2474 rexlimd2 2475 r19.29af2 2496 r19.37 2506 ralidm 3341 iineq2d 3698 mpteq2da 3867 onintonm 4261 mpteqb 5282 eusvobj2 5518 tfri3 5976 fimaxre2 10109 zsupcllemstep 10341 bezoutlemmain 10387 bezoutlemzz 10391 |
Copyright terms: Public domain | W3C validator |