![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > rexlimivw | GIF version |
Description: Weaker version of rexlimiv 2502. (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 2502 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1448 ∃wrex 2376 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1391 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-4 1455 ax-17 1474 ax-ial 1482 ax-i5r 1483 |
This theorem depends on definitions: df-bi 116 df-nf 1405 df-ral 2380 df-rex 2381 |
This theorem is referenced by: r19.29vva 2535 eliun 3764 reusv3i 4318 elrnmptg 4729 fun11iun 5322 fmpt 5502 fliftfun 5629 elrnmpo 5816 releldm2 6013 tfrlem4 6140 iinerm 6431 elixpsn 6559 isfi 6585 cardcl 6948 cardval3ex 6952 ltbtwnnqq 7124 recexprlemlol 7335 recexprlemupu 7337 restsspw 11912 ssnei 12102 tgcnp 12159 xmetunirn 12286 metss 12422 metrest 12434 |
Copyright terms: Public domain | W3C validator |