![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > cbvmptv | Unicode version |
Description: Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by Mario Carneiro, 19-Feb-2013.) |
Ref | Expression |
---|---|
cbvmptv.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
cbvmptv |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2319 |
. 2
![]() ![]() ![]() ![]() | |
2 | nfcv 2319 |
. 2
![]() ![]() ![]() ![]() | |
3 | cbvmptv.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | cbvmpt 4098 |
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 106 ax-ia2 107 ax-ia3 108 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-3an 980 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-v 2739 df-un 3133 df-sn 3598 df-pr 3599 df-op 3601 df-opab 4065 df-mpt 4066 |
This theorem is referenced by: fnmptfvd 5620 frecsuc 6407 xpmapen 6849 omp1eom 7093 fodjuomni 7146 fodjumkv 7157 nninfwlporlemd 7169 nninfwlpor 7171 nninfwlpoim 7175 caucvgsrlembnd 7799 negiso 8911 infrenegsupex 9593 frec2uzsucd 10400 frecuzrdgdom 10417 frecuzrdgfun 10419 frecuzrdgsuct 10423 0tonninf 10438 1tonninf 10439 seq3f1oleml 10502 seq3f1o 10503 hashfz1 10762 xrnegiso 11269 infxrnegsupex 11270 climcvg1n 11357 summodc 11390 zsumdc 11391 fsum3 11394 fsumadd 11413 prodmodc 11585 zproddc 11586 fprodseq 11590 phimullem 12224 eulerthlemh 12230 eulerthlemth 12231 ennnfonelemnn0 12422 ennnfonelemr 12423 ctinfom 12428 grplactcnv 12971 cdivcncfap 14057 expcncf 14062 2sqlem1 14431 bj-charfunbi 14533 subctctexmid 14720 nninfsellemqall 14734 nninfomni 14738 nninffeq 14739 exmidsbthrlem 14740 exmidsbthr 14741 isomninn 14749 iswomninn 14768 ismkvnn 14771 |
Copyright terms: Public domain | W3C validator |