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 4537, 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 2629	. 2 |- F/_ z C
2		nfcv 2629	. 2 |- F/_ w C
3		nfcv 2629	. 2 |- F/_ x D
4		nfcv 2629	. 2 |- F/_ y D
5		cbvmpt2v.1	. . 3 |- ( x = z -> C = E )
6		cbvmpt2v.2	. . 3 |- ( y = w -> E = D )
7	5, 6	sylan9eq 2528	. 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 1379   |-> cmpt2 6284

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-opab 4506  df-oprab 6286  df-mpt2 6287

This theorem is referenced by:  seqomlem0  7111  dffi3  7887  cantnfsuc  8085  cantnfsucOLD  8115  fin23lem33  8721  om2uzrdg  12031  uzrdgsuci  12035  sadcp1  13960  smupp1  13985  imasvscafn  14788  sylow1  16419  sylow2b  16439  sylow3lem5  16447  sylow3  16449  efgmval  16526  efgtf  16536  frlmphl  18579  pmatcollpw3lem  19051  mp2pm2mplem3  19076  txbas  19803  bcth  21503  opnmbl  21746  mbfimaopn  21798  mbfi1fseq  21863  motplusg  23657  ttgval  23854  numclwwlk5  24789  opsqrlem3  26737  fvproj  27498  dya2iocival  27884  sxbrsigalem5  27899  sxbrsigalem6  27900  eulerpart  27961  sseqp1  27974  cvmliftlem15  28383  cvmlift2  28401  opnmbllem0  29627  mblfinlem1  29628  mblfinlem2  29629  sdc  29840  lmod1zr  32175  tendoplcbv  35571  dvhvaddcbv  35886  dvhvscacbv  35895