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 4749, 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 2764 | . 2 | |
2 | nfcv 2764 | . 2 | |
3 | nfcv 2764 | . 2 | |
4 | nfcv 2764 | . 2 | |
5 | cbvmpt2v.1 | . . 3 | |
6 | cbvmpt2v.2 | . . 3 | |
7 | 5, 6 | sylan9eq 2676 | . 2 |
8 | 1, 2, 3, 4, 7 | cbvmpt2 6734 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wceq 1483 cmpt2 6652 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pr 4906 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-rab 2921 df-v 3202 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-opab 4713 df-oprab 6654 df-mpt2 6655 |
This theorem is referenced by: seqomlem0 7544 dffi3 8337 cantnfsuc 8567 fin23lem33 9167 om2uzrdg 12755 uzrdgsuci 12759 sadcp1 15177 smupp1 15202 imasvscafn 16197 mgmnsgrpex 17418 sgrpnmndex 17419 sylow1 18018 sylow2b 18038 sylow3lem5 18046 sylow3 18048 efgmval 18125 efgtf 18135 frlmphl 20120 pmatcollpw3lem 20588 mp2pm2mplem3 20613 txbas 21370 bcth 23126 opnmbl 23370 mbfimaopn 23423 mbfi1fseq 23488 motplusg 25437 ttgval 25755 opsqrlem3 29001 mdetpmtr12 29891 madjusmdetlem4 29896 fvproj 29899 dya2iocival 30335 sxbrsigalem5 30350 sxbrsigalem6 30351 eulerpart 30444 sseqp1 30457 cvmliftlem15 31280 cvmlift2 31298 opnmbllem0 33445 mblfinlem1 33446 mblfinlem2 33447 sdc 33540 tendoplcbv 36063 dvhvaddcbv 36378 dvhvscacbv 36387 fsovcnvlem 38307 ntrneibex 38371 ioorrnopn 40525 hoidmvle 40814 ovnhoi 40817 hoimbl 40845 smflimlem6 40984 funcrngcsetc 41998 funcrngcsetcALT 41999 funcringcsetc 42035 lmod1zr 42282 |
Copyright terms: Public domain | W3C validator |