Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ralrimiv | GIF version |
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Nov-1994.) |
Ref | Expression |
---|---|
ralrimiv.1 | ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓)) |
Ref | Expression |
---|---|
ralrimiv | ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1421 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | ralrimiv.1 | . 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓)) | |
3 | 1, 2 | ralrimi 2390 | 1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1393 ∀wral 2306 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-gen 1338 ax-4 1400 ax-17 1419 |
This theorem depends on definitions: df-bi 110 df-nf 1350 df-ral 2311 |
This theorem is referenced by: ralrimiva 2392 ralrimivw 2393 ralrimivv 2400 r19.27av 2448 rr19.3v 2682 rabssdv 3020 rzal 3318 trin 3864 class2seteq 3916 ralxfrALT 4199 ssorduni 4213 ordsucim 4226 onintonm 4243 issref 4707 funimaexglem 4982 poxp 5853 rdgss 5970 dom2lem 6252 ordiso2 6357 uzind 8349 zindd 8356 lbzbi 8551 icoshftf1o 8859 bj-nntrans2 10077 bj-inf2vnlem1 10095 |
Copyright terms: Public domain | W3C validator |