![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cbvmpt2v | Structured version Visualization version Unicode version |
Description: Rule to change the bound variable in a maps-to function, using implicit substitution. With a longer proof analogous to cbvmpt 4507, some distinct variable requirements could be eliminated. (Contributed by NM, 11-Jun-2013.) |
Ref | Expression |
---|---|
cbvmpt2v.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
cbvmpt2v.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
cbvmpt2v |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2602 |
. 2
![]() ![]() ![]() ![]() | |
2 | nfcv 2602 |
. 2
![]() ![]() ![]() ![]() | |
3 | nfcv 2602 |
. 2
![]() ![]() ![]() ![]() | |
4 | nfcv 2602 |
. 2
![]() ![]() ![]() ![]() | |
5 | cbvmpt2v.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | cbvmpt2v.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 5, 6 | sylan9eq 2515 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 1, 2, 3, 4, 7 | cbvmpt2 6396 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-9 1906 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 ax-sep 4538 ax-nul 4547 ax-pr 4652 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 993 df-tru 1457 df-ex 1674 df-nf 1678 df-sb 1808 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2591 df-ne 2634 df-rab 2757 df-v 3058 df-dif 3418 df-un 3420 df-in 3422 df-ss 3429 df-nul 3743 df-if 3893 df-sn 3980 df-pr 3982 df-op 3986 df-opab 4475 df-oprab 6318 df-mpt2 6319 |
This theorem is referenced by: seqomlem0 7191 dffi3 7970 cantnfsuc 8200 fin23lem33 8800 om2uzrdg 12201 uzrdgsuci 12205 sadcp1 14477 smupp1 14502 imasvscafn 15491 mgmnsgrpex 16713 sgrpnmndex 16714 sylow1 17303 sylow2b 17323 sylow3lem5 17331 sylow3 17333 efgmval 17410 efgtf 17420 frlmphl 19387 pmatcollpw3lem 19855 mp2pm2mplem3 19880 txbas 20630 bcth 22345 opnmbl 22608 mbfimaopn 22660 mbfi1fseq 22727 motplusg 24635 ttgval 24953 numclwwlk5 25888 opsqrlem3 27843 mdetpmtr12 28699 madjusmdetlem4 28704 fvproj 28707 dya2iocival 29143 sxbrsigalem5 29158 sxbrsigalem6 29159 eulerpart 29263 sseqp1 29276 cvmliftlem15 30069 cvmlift2 30087 opnmbllem0 32020 mblfinlem1 32021 mblfinlem2 32022 sdc 32117 tendoplcbv 34386 dvhvaddcbv 34701 dvhvscacbv 34710 hoidmvle 38459 ovnhoi 38462 hoimbl 38490 funcrngcsetc 40272 funcrngcsetcALT 40273 funcringcsetc 40309 lmod1zr 40558 |
Copyright terms: Public domain | W3C validator |