![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > rexlimivw | Unicode version |
Description: Weaker version of rexlimiv 2546. (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 2546 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
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 1424 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-4 1488 ax-17 1507 ax-ial 1515 ax-i5r 1516 |
This theorem depends on definitions: df-bi 116 df-nf 1438 df-ral 2422 df-rex 2423 |
This theorem is referenced by: r19.29vva 2580 eliun 3825 reusv3i 4388 elrnmptg 4799 fun11iun 5396 fmpt 5578 fliftfun 5705 elrnmpo 5892 releldm2 6091 tfrlem4 6218 iinerm 6509 elixpsn 6637 isfi 6663 cardcl 7054 cardval3ex 7058 ltbtwnnqq 7247 recexprlemlol 7458 recexprlemupu 7460 suplocsr 7641 restsspw 12169 ssnei 12359 tgcnp 12417 xmetunirn 12566 metss 12702 metrest 12714 |
Copyright terms: Public domain | W3C validator |