Theorem cbvmpt2v 6359

Description: Rule to change the bound variable in a maps-to function, using implicit substitution. With a longer proof analogous to cbvmpt 4524, some distinct variable requirements could be eliminated. (Contributed by NM, 11-Jun-2013.)

Hypotheses

Ref	Expression
cbvmpt2v.1	|- ( x = z -> C = E )
cbvmpt2v.2	|- ( y = w -> E = D )

Assertion

Ref	Expression
cbvmpt2v	|- ( x e. A , y e. B |-> C ) = ( z e. A , w e. B |-> D )

Distinct variable groups:   x, w, y, z, A   w, B, x, y, z   w, C, z   x, D, y

Allowed substitution hints:   C( x, y)   D( z, w)   E( x, y, z, w)

Proof of Theorem cbvmpt2v

Step	Hyp	Ref	Expression
1		nfcv 2603	. 2 |- F/_ z C
2		nfcv 2603	. 2 |- F/_ w C
3		nfcv 2603	. 2 |- F/_ x D
4		nfcv 2603	. 2 |- F/_ y D
5		cbvmpt2v.1	. . 3 |- ( x = z -> C = E )
6		cbvmpt2v.2	. . 3 |- ( y = w -> E = D )
7	5, 6	sylan9eq 2502	. 2 |- ( ( x = z /\ y = w ) -> C = D )
8	1, 2, 3, 4, 7	cbvmpt2 6358	1 |- ( x e. A , y e. B |-> C ) = ( z e. A , w e. B |-> D )

Syntax hints:   -> wi 4   = wceq 1381   |-> cmpt2 6280

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4555  ax-nul 4563  ax-pr 4673

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-rab 2800  df-v 3095  df-dif 3462  df-un 3464  df-in 3466  df-ss 3473  df-nul 3769  df-if 3924  df-sn 4012  df-pr 4014  df-op 4018  df-opab 4493  df-oprab 6282  df-mpt2 6283

This theorem is referenced by:  seqomlem0  7113  dffi3  7890  cantnfsuc  8089  cantnfsucOLD  8119  fin23lem33  8725  om2uzrdg  12043  uzrdgsuci  12047  sadcp1  13979  smupp1  14004  imasvscafn  14808  mgmnsgrpex  15920  sgrpnmndex  15921  sylow1  16494  sylow2b  16514  sylow3lem5  16522  sylow3  16524  efgmval  16601  efgtf  16611  frlmphl  18682  pmatcollpw3lem  19154  mp2pm2mplem3  19179  txbas  19938  bcth  21638  opnmbl  21881  mbfimaopn  21933  mbfi1fseq  21998  motplusg  23798  ttgval  24047  numclwwlk5  24981  opsqrlem3  26930  fvproj  27705  dya2iocival  28114  sxbrsigalem5  28129  sxbrsigalem6  28130  eulerpart  28191  sseqp1  28204  cvmliftlem15  28613  cvmlift2  28631  opnmbllem0  30022  mblfinlem1  30023  mblfinlem2  30024  sdc  30209  funcrngcsetc  32542  funcringcsetc  32575  lmod1zr  32824  tendoplcbv  36224  dvhvaddcbv  36539  dvhvscacbv  36548