Theorem cbvmpt2v 6171

Description: Rule to change the bound variable in a maps-to function, using implicit substitution. With a longer proof analogous to cbvmpt 4387, 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 2584	. 2 |- F/_ z C
2		nfcv 2584	. 2 |- F/_ w C
3		nfcv 2584	. 2 |- F/_ x D
4		nfcv 2584	. 2 |- F/_ y D
5		cbvmpt2v.1	. . 3 |- ( x = z -> C = E )
6		cbvmpt2v.2	. . 3 |- ( y = w -> E = D )
7	5, 6	sylan9eq 2495	. 2 |- ( ( x = z /\ y = w ) -> C = D )
8	1, 2, 3, 4, 7	cbvmpt2 6170	1 |- ( x e. A , y e. B |-> C ) = ( z e. A , w e. B |-> D )

Syntax hints:   -> wi 4   = wceq 1369   e. cmpt2 6098

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4418  ax-nul 4426  ax-pr 4536

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ne 2613  df-rab 2729  df-v 2979  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347  df-nul 3643  df-if 3797  df-sn 3883  df-pr 3885  df-op 3889  df-opab 4356  df-oprab 6100  df-mpt2 6101

This theorem is referenced by:  seqomlem0  6909  dffi3  7686  cantnfsuc  7883  cantnfsucOLD  7913  fin23lem33  8519  om2uzrdg  11784  uzrdgsuci  11788  sadcp1  13656  smupp1  13681  imasvscafn  14480  sylow1  16107  sylow2b  16127  sylow3lem5  16135  sylow3  16137  efgmval  16214  efgtf  16224  frlmphl  18211  txbas  19145  bcth  20845  opnmbl  21087  mbfimaopn  21139  mbfi1fseq  21204  ttgval  23126  opsqrlem3  25551  dya2iocival  26693  sxbrsigalem5  26708  sxbrsigalem6  26709  eulerpart  26770  sseqp1  26783  cvmliftlem15  27192  cvmlift2  27210  opnmbllem0  28432  mblfinlem1  28433  mblfinlem2  28434  sdc  28645  numclwwlk5  30710  pmatcollpw1dst  30906  pmatcollpw1  30909  pmatcollpw2lem  30910  pmattomply1lem  30913  pmattomply1ghmlem2  30914  pmattomply1f1lem  30915  pmattomply1rn  30917  pmattomply1coe1  30919  idpmattoidmply1  30920  mp2pm2mplem3  30923  mp2pm2mplem5  30925  mp2pm2mp  30926  pmattomply1fo  30928  pmattomply1ghm  30930  pmattomply1mhmlem2  30934  lmod1zr  31040  tendoplcbv  34424  dvhvaddcbv  34739  dvhvscacbv  34748