![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > rexlimiv | GIF version |
Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.) |
Ref | Expression |
---|---|
rexlimiv.1 | ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) |
Ref | Expression |
---|---|
rexlimiv | ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1462 | . 2 ⊢ Ⅎ𝑥𝜓 | |
2 | rexlimiv.1 | . 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) | |
3 | 1, 2 | rexlimi 2476 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1434 ∃wrex 2354 |
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 1377 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-4 1441 ax-17 1460 ax-ial 1468 ax-i5r 1469 |
This theorem depends on definitions: df-bi 115 df-nf 1391 df-ral 2358 df-rex 2359 |
This theorem is referenced by: rexlimiva 2478 rexlimivw 2479 rexlimivv 2488 r19.36av 2511 r19.44av 2519 r19.45av 2520 rexn0 3361 uniss2 3658 elres 4705 ssimaex 5310 tfrlem5 6011 tfrlem8 6015 ecoptocl 6309 mapsn 6377 findcard 6534 findcard2 6535 findcard2s 6536 prnmaddl 6952 0re 7391 cnegexlem2 7561 0cnALT 7575 bndndx 8564 uzn0 8929 ublbneg 8993 rexanuz2 10251 bj-inf2vnlem2 11209 |
Copyright terms: Public domain | W3C validator |