MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cbvmpt Structured version   Unicode version

Theorem cbvmpt 4382
Description: Rule to change the bound variable in a maps-to function, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. (Contributed by NM, 11-Sep-2011.)
Hypotheses
Ref Expression
cbvmpt.1  |-  F/_ y B
cbvmpt.2  |-  F/_ x C
cbvmpt.3  |-  ( x  =  y  ->  B  =  C )
Assertion
Ref Expression
cbvmpt  |-  ( x  e.  A  |->  B )  =  ( y  e.  A  |->  C )
Distinct variable groups:    x, A    y, A
Allowed substitution hints:    B( x, y)    C( x, y)

Proof of Theorem cbvmpt
Dummy variables  z  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfv 1673 . . . 4  |-  F/ w
( x  e.  A  /\  z  =  B
)
2 nfv 1673 . . . . 5  |-  F/ x  w  e.  A
3 nfs1v 2142 . . . . 5  |-  F/ x [ w  /  x ] z  =  B
42, 3nfan 1861 . . . 4  |-  F/ x
( w  e.  A  /\  [ w  /  x ] z  =  B )
5 eleq1 2503 . . . . 5  |-  ( x  =  w  ->  (
x  e.  A  <->  w  e.  A ) )
6 sbequ12 1936 . . . . 5  |-  ( x  =  w  ->  (
z  =  B  <->  [ w  /  x ] z  =  B ) )
75, 6anbi12d 710 . . . 4  |-  ( x  =  w  ->  (
( x  e.  A  /\  z  =  B
)  <->  ( w  e.  A  /\  [ w  /  x ] z  =  B ) ) )
81, 4, 7cbvopab1 4362 . . 3  |-  { <. x ,  z >.  |  ( x  e.  A  /\  z  =  B ) }  =  { <. w ,  z >.  |  ( w  e.  A  /\  [ w  /  x ]
z  =  B ) }
9 nfv 1673 . . . . 5  |-  F/ y  w  e.  A
10 cbvmpt.1 . . . . . . 7  |-  F/_ y B
1110nfeq2 2590 . . . . . 6  |-  F/ y  z  =  B
1211nfsb 2146 . . . . 5  |-  F/ y [ w  /  x ] z  =  B
139, 12nfan 1861 . . . 4  |-  F/ y ( w  e.  A  /\  [ w  /  x ] z  =  B )
14 nfv 1673 . . . 4  |-  F/ w
( y  e.  A  /\  z  =  C
)
15 eleq1 2503 . . . . 5  |-  ( w  =  y  ->  (
w  e.  A  <->  y  e.  A ) )
16 sbequ 2067 . . . . . 6  |-  ( w  =  y  ->  ( [ w  /  x ] z  =  B  <->  [ y  /  x ] z  =  B ) )
17 cbvmpt.2 . . . . . . . 8  |-  F/_ x C
1817nfeq2 2590 . . . . . . 7  |-  F/ x  z  =  C
19 cbvmpt.3 . . . . . . . 8  |-  ( x  =  y  ->  B  =  C )
2019eqeq2d 2454 . . . . . . 7  |-  ( x  =  y  ->  (
z  =  B  <->  z  =  C ) )
2118, 20sbie 2100 . . . . . 6  |-  ( [ y  /  x ]
z  =  B  <->  z  =  C )
2216, 21syl6bb 261 . . . . 5  |-  ( w  =  y  ->  ( [ w  /  x ] z  =  B  <-> 
z  =  C ) )
2315, 22anbi12d 710 . . . 4  |-  ( w  =  y  ->  (
( w  e.  A  /\  [ w  /  x ] z  =  B )  <->  ( y  e.  A  /\  z  =  C ) ) )
2413, 14, 23cbvopab1 4362 . . 3  |-  { <. w ,  z >.  |  ( w  e.  A  /\  [ w  /  x ]
z  =  B ) }  =  { <. y ,  z >.  |  ( y  e.  A  /\  z  =  C ) }
258, 24eqtri 2463 . 2  |-  { <. x ,  z >.  |  ( x  e.  A  /\  z  =  B ) }  =  { <. y ,  z >.  |  ( y  e.  A  /\  z  =  C ) }
26 df-mpt 4352 . 2  |-  ( x  e.  A  |->  B )  =  { <. x ,  z >.  |  ( x  e.  A  /\  z  =  B ) }
27 df-mpt 4352 . 2  |-  ( y  e.  A  |->  C )  =  { <. y ,  z >.  |  ( y  e.  A  /\  z  =  C ) }
2825, 26, 273eqtr4i 2473 1  |-  ( x  e.  A  |->  B )  =  ( y  e.  A  |->  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1369   [wsb 1700    e. wcel 1756   F/_wnfc 2566   {copab 4349    e. cmpt 4350
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-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
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 2568  df-rab 2724  df-v 2974  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-sn 3878  df-pr 3880  df-op 3884  df-opab 4351  df-mpt 4352
This theorem is referenced by:  cbvmptv  4383  dffn5f  5746  fvmpts  5776  fvmpt2i  5780  fvmptex  5784  fmptcof  5877  fmptcos  5878  fliftfuns  6007  offval2  6336  ofmpteq  6338  mpt2curryvald  6789  qliftfuns  7187  axcc2  8606  ac6num  8648  seqof2  11864  summolem2a  13192  zsum  13195  fsumcvg2  13204  fsumrlim  13274  pcmptdvds  13956  prdsdsval2  14422  gsumconstf  16428  gsummpt1n0  16456  gsum2d2  16466  dprd2d2  16543  gsumdixpOLD  16700  gsumdixp  16701  psrass1lem  17447  evl1gsumdlem  17790  madugsum  18449  cnmpt1t  19238  cnmpt2k  19261  elmptrab  19400  flfcnp2  19580  prdsxmet  19944  fsumcn  20446  ovoliunlem3  20987  ovoliun  20988  ovoliun2  20989  voliun  21035  mbfpos  21129  mbfposb  21131  i1fposd  21185  itg2cnlem1  21239  isibl2  21244  cbvitg  21253  itgss3  21292  itgfsum  21304  itgabs  21312  itgcn  21320  limcmpt  21358  dvmptfsum  21447  lhop2  21487  dvfsumle  21493  dvfsumlem2  21499  itgsubstlem  21520  itgsubst  21521  itgulm2  21874  rlimcnp2  22360  xrge0tmd  26376  cbvprod  27428  prodmolem2a  27447  zprod  27450  fprod  27454  mbfposadd  28439  itgabsnc  28461  ftc1cnnclem  28465  ftc2nc  28476  mzpsubst  29085  rabdiophlem2  29140  aomclem8  29414  fsumcnf  29743  cncfmptss  29768  mulc1cncfg  29770  expcnfg  29773  stoweidlem21  29816  stirlinglem4  29872  stirlinglem13  29881  stirlinglem15  29883  coe1fzgsumdlem  30837
  Copyright terms: Public domain W3C validator