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 1521 | . 2 ⊢ Ⅎ𝑥𝜓 | |
2 | rexlimiv.1 | . 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) | |
3 | 1, 2 | rexlimi 2580 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2141 ∃wrex 2449 |
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 1440 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-4 1503 ax-17 1519 ax-ial 1527 ax-i5r 1528 |
This theorem depends on definitions: df-bi 116 df-nf 1454 df-ral 2453 df-rex 2454 |
This theorem is referenced by: rexlimiva 2582 rexlimivw 2583 rexlimivv 2593 r19.36av 2621 r19.44av 2629 r19.45av 2630 rexn0 3512 uniss2 3825 elres 4925 ssimaex 5555 mpoexw 6190 tfrlem5 6291 tfrlem8 6295 ecoptocl 6598 mapsn 6666 elixpsn 6711 ixpsnf1o 6712 findcard 6864 findcard2 6865 findcard2s 6866 fiintim 6904 prnmaddl 7445 0re 7913 cnegexlem2 8088 0cnALT 8102 bndndx 9127 uzn0 9495 ublbneg 9565 rexanuz2 10948 opnneiid 12923 2sqlem2 13710 bj-inf2vnlem2 13971 |
Copyright terms: Public domain | W3C validator |