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 1502 | . 2 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) |
4 | df-ral 2419 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) | |
5 | 3, 4 | sylibr 133 | 1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1329 Ⅎwnf 1436 ∈ wcel 1480 ∀wral 2414 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1423 ax-gen 1425 ax-4 1487 |
This theorem depends on definitions: df-bi 116 df-nf 1437 df-ral 2419 |
This theorem is referenced by: ralrimiv 2502 reximdai 2528 r19.12 2536 rexlimd 2544 rexlimd2 2545 r19.29af2 2570 r19.37 2581 ralidm 3458 iineq2d 3828 mpteq2da 4012 onintonm 4428 mpteqb 5504 fmptdf 5570 eusvobj2 5753 tfri3 6257 mapxpen 6735 fodjuomnilemdc 7009 fimaxre2 10991 zsupcllemstep 11627 bezoutlemmain 11675 bezoutlemzz 11679 exmidunben 11928 mulcncf 12749 limccnp2lem 12803 |
Copyright terms: Public domain | W3C validator |