Theorem cbvmpt2v 6397

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.)

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 2602	. 2 |- F/_ z C
2		nfcv 2602	. 2 |- F/_ w C
3		nfcv 2602	. 2 |- F/_ x D
4		nfcv 2602	. 2 |- F/_ y D
5		cbvmpt2v.1	. . 3 |- ( x = z -> C = E )
6		cbvmpt2v.2	. . 3 |- ( y = w -> E = D )
7	5, 6	sylan9eq 2515	. 2 |- ( ( x = z /\ y = w ) -> C = D )
8	1, 2, 3, 4, 7	cbvmpt2 6396	1 |- ( x e. A , y e. B |-> C ) = ( z e. A , w e. B |-> D )

Syntax hints:   -> wi 4   = wceq 1454   |-> cmpt2 6316

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