![]() |
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 1539 | . 2 ⊢ Ⅎ𝑥𝜓 | |
2 | rexlimiv.1 | . 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) | |
3 | 1, 2 | rexlimi 2600 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2160 ∃wrex 2469 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1458 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-4 1521 ax-17 1537 ax-ial 1545 ax-i5r 1546 |
This theorem depends on definitions: df-bi 117 df-nf 1472 df-ral 2473 df-rex 2474 |
This theorem is referenced by: rexlimiva 2602 rexlimivw 2603 rexlimivv 2613 r19.36av 2641 r19.44av 2649 r19.45av 2650 rexn0 3536 uniss2 3855 elres 4961 ssimaex 5597 mpoexw 6237 tfrlem5 6338 tfrlem8 6342 ecoptocl 6647 mapsn 6715 elixpsn 6760 ixpsnf1o 6761 findcard 6915 findcard2 6916 findcard2s 6917 fiintim 6956 prnmaddl 7518 0re 7986 cnegexlem2 8162 0cnALT 8176 bndndx 9204 uzn0 9572 ublbneg 9642 rexanuz2 11031 opnneiid 14116 2sqlem2 14915 bj-inf2vnlem2 15176 |
Copyright terms: Public domain | W3C validator |