![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > rexlimivw | GIF version |
Description: Weaker version of rexlimiv 2588. (Contributed by FL, 19-Sep-2011.) |
Ref | Expression |
---|---|
rexlimivw.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
rexlimivw | ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexlimivw.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | a1i 9 | . 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) |
3 | 2 | rexlimiv 2588 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2148 ∃wrex 2456 |
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 1447 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-4 1510 ax-17 1526 ax-ial 1534 ax-i5r 1535 |
This theorem depends on definitions: df-bi 117 df-nf 1461 df-ral 2460 df-rex 2461 |
This theorem is referenced by: r19.29vva 2622 eliun 3892 reusv3i 4461 elrnmptg 4881 fun11iun 5484 fmpt 5669 fliftfun 5800 elrnmpo 5991 releldm2 6189 tfrlem4 6317 iinerm 6610 elixpsn 6738 isfi 6764 cardcl 7183 cardval3ex 7187 ltbtwnnqq 7417 recexprlemlol 7628 recexprlemupu 7630 suplocsr 7811 restsspw 12704 ssnei 13791 tgcnp 13849 xmetunirn 13998 metss 14134 metrest 14146 |
Copyright terms: Public domain | W3C validator |