![]() |
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 1509 | . 2 ⊢ Ⅎ𝑥𝜓 | |
2 | rexlimiv.1 | . 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) | |
3 | 1, 2 | rexlimi 2545 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1481 ∃wrex 2418 |
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 1424 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-4 1488 ax-17 1507 ax-ial 1515 ax-i5r 1516 |
This theorem depends on definitions: df-bi 116 df-nf 1438 df-ral 2422 df-rex 2423 |
This theorem is referenced by: rexlimiva 2547 rexlimivw 2548 rexlimivv 2558 r19.36av 2585 r19.44av 2593 r19.45av 2594 rexn0 3466 uniss2 3775 elres 4863 ssimaex 5490 tfrlem5 6219 tfrlem8 6223 ecoptocl 6524 mapsn 6592 elixpsn 6637 ixpsnf1o 6638 findcard 6790 findcard2 6791 findcard2s 6792 fiintim 6825 prnmaddl 7322 0re 7790 cnegexlem2 7962 0cnALT 7976 bndndx 9000 uzn0 9365 ublbneg 9432 rexanuz2 10795 opnneiid 12372 bj-inf2vnlem2 13340 |
Copyright terms: Public domain | W3C validator |