Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > rexlimivw | GIF version |
Description: Weaker version of rexlimiv 2471. (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 2471 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1433 ∃wrex 2349 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1376 ax-gen 1378 ax-ie1 1422 ax-ie2 1423 ax-4 1440 ax-17 1459 ax-ial 1467 ax-i5r 1468 |
This theorem depends on definitions: df-bi 115 df-nf 1390 df-ral 2353 df-rex 2354 |
This theorem is referenced by: r19.29vva 2500 eliun 3682 reusv3i 4209 elrnmptg 4604 fun11iun 5167 fmpt 5340 fliftfun 5456 elrnmpt2 5634 releldm2 5831 tfrlem4 5952 iinerm 6201 isfi 6264 cardcl 6450 cardval3ex 6454 ltbtwnnqq 6605 recexprlemlol 6816 recexprlemupu 6818 |
Copyright terms: Public domain | W3C validator |