Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > rexlimivw | GIF version |
Description: Weaker version of rexlimiv 2520. (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 2520 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1465 ∃wrex 2394 |
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 1408 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-4 1472 ax-17 1491 ax-ial 1499 ax-i5r 1500 |
This theorem depends on definitions: df-bi 116 df-nf 1422 df-ral 2398 df-rex 2399 |
This theorem is referenced by: r19.29vva 2554 eliun 3787 reusv3i 4350 elrnmptg 4761 fun11iun 5356 fmpt 5538 fliftfun 5665 elrnmpo 5852 releldm2 6051 tfrlem4 6178 iinerm 6469 elixpsn 6597 isfi 6623 cardcl 7005 cardval3ex 7009 ltbtwnnqq 7191 recexprlemlol 7402 recexprlemupu 7404 suplocsr 7585 restsspw 12057 ssnei 12247 tgcnp 12305 xmetunirn 12454 metss 12590 metrest 12602 |
Copyright terms: Public domain | W3C validator |