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

Theorem cbvmpt 4487
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 1769 . . . 4  |-  F/ w
( x  e.  A  /\  z  =  B
)
2 nfv 1769 . . . . 5  |-  F/ x  w  e.  A
3 nfs1v 2286 . . . . 5  |-  F/ x [ w  /  x ] z  =  B
42, 3nfan 2031 . . . 4  |-  F/ x
( w  e.  A  /\  [ w  /  x ] z  =  B )
5 eleq1 2537 . . . . 5  |-  ( x  =  w  ->  (
x  e.  A  <->  w  e.  A ) )
6 sbequ12 2098 . . . . 5  |-  ( x  =  w  ->  (
z  =  B  <->  [ w  /  x ] z  =  B ) )
75, 6anbi12d 725 . . . 4  |-  ( x  =  w  ->  (
( x  e.  A  /\  z  =  B
)  <->  ( w  e.  A  /\  [ w  /  x ] z  =  B ) ) )
81, 4, 7cbvopab1 4466 . . 3  |-  { <. x ,  z >.  |  ( x  e.  A  /\  z  =  B ) }  =  { <. w ,  z >.  |  ( w  e.  A  /\  [ w  /  x ]
z  =  B ) }
9 nfv 1769 . . . . 5  |-  F/ y  w  e.  A
10 cbvmpt.1 . . . . . . 7  |-  F/_ y B
1110nfeq2 2627 . . . . . 6  |-  F/ y  z  =  B
1211nfsb 2289 . . . . 5  |-  F/ y [ w  /  x ] z  =  B
139, 12nfan 2031 . . . 4  |-  F/ y ( w  e.  A  /\  [ w  /  x ] z  =  B )
14 nfv 1769 . . . 4  |-  F/ w
( y  e.  A  /\  z  =  C
)
15 eleq1 2537 . . . . 5  |-  ( w  =  y  ->  (
w  e.  A  <->  y  e.  A ) )
16 sbequ 2225 . . . . . 6  |-  ( w  =  y  ->  ( [ w  /  x ] z  =  B  <->  [ y  /  x ] z  =  B ) )
17 cbvmpt.2 . . . . . . . 8  |-  F/_ x C
1817nfeq2 2627 . . . . . . 7  |-  F/ x  z  =  C
19 cbvmpt.3 . . . . . . . 8  |-  ( x  =  y  ->  B  =  C )
2019eqeq2d 2481 . . . . . . 7  |-  ( x  =  y  ->  (
z  =  B  <->  z  =  C ) )
2118, 20sbie 2257 . . . . . 6  |-  ( [ y  /  x ]
z  =  B  <->  z  =  C )
2216, 21syl6bb 269 . . . . 5  |-  ( w  =  y  ->  ( [ w  /  x ] z  =  B  <-> 
z  =  C ) )
2315, 22anbi12d 725 . . . 4  |-  ( w  =  y  ->  (
( w  e.  A  /\  [ w  /  x ] z  =  B )  <->  ( y  e.  A  /\  z  =  C ) ) )
2413, 14, 23cbvopab1 4466 . . 3  |-  { <. w ,  z >.  |  ( w  e.  A  /\  [ w  /  x ]
z  =  B ) }  =  { <. y ,  z >.  |  ( y  e.  A  /\  z  =  C ) }
258, 24eqtri 2493 . 2  |-  { <. x ,  z >.  |  ( x  e.  A  /\  z  =  B ) }  =  { <. y ,  z >.  |  ( y  e.  A  /\  z  =  C ) }
26 df-mpt 4456 . 2  |-  ( x  e.  A  |->  B )  =  { <. x ,  z >.  |  ( x  e.  A  /\  z  =  B ) }
27 df-mpt 4456 . 2  |-  ( y  e.  A  |->  C )  =  { <. y ,  z >.  |  ( y  e.  A  /\  z  =  C ) }
2825, 26, 273eqtr4i 2503 1  |-  ( x  e.  A  |->  B )  =  ( y  e.  A  |->  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376    = wceq 1452   [wsb 1805    e. wcel 1904   F/_wnfc 2599   {copab 4453    |-> cmpt 4454
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-rab 2765  df-v 3033  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-opab 4455  df-mpt 4456
This theorem is referenced by:  cbvmptv  4488  dffn5f  5935  fvmpts  5966  fvmpt2i  5971  fvmptex  5975  fmptcof  6073  fmptcos  6074  fliftfuns  6225  offval2  6567  ofmpteq  6569  mpt2curryvald  7035  qliftfuns  7468  axcc2  8885  ac6num  8927  seqof2  12309  summolem2a  13858  zsum  13861  fsumcvg2  13870  fsumrlim  13948  cbvprod  14046  prodmolem2a  14065  zprod  14068  fprod  14072  pcmptdvds  14918  prdsdsval2  15460  gsumconstf  17646  gsummpt1n0  17675  gsum2d2  17684  dprd2d2  17755  gsumdixp  17915  psrass1lem  18678  coe1fzgsumdlem  18972  gsumply1eq  18976  evl1gsumdlem  19021  madugsum  19745  cnmpt1t  20757  cnmpt2k  20780  elmptrab  20919  flfcnp2  21100  prdsxmet  21462  fsumcn  21980  ovoliunlem3  22535  ovoliun  22536  ovoliun2  22537  voliun  22586  mbfpos  22686  mbfposb  22688  i1fposd  22744  itg2cnlem1  22798  isibl2  22803  cbvitg  22812  itgss3  22851  itgfsum  22863  itgabs  22871  itgcn  22879  limcmpt  22917  dvmptfsum  23006  lhop2  23046  dvfsumle  23052  dvfsumlem2  23058  itgsubstlem  23079  itgsubst  23080  itgulm2  23443  rlimcnp2  23971  gsummpt2co  28617  esumsnf  28959  mbfposadd  32052  itgabsnc  32075  ftc1cnnclem  32079  ftc2nc  32090  mzpsubst  35661  rabdiophlem2  35716  aomclem8  35990  fsumcnf  37405  disjf1  37528  disjrnmpt2  37534  disjinfi  37539  cncfmptss  37762  mulc1cncfg  37764  expcnfg  37768  icccncfext  37862  cncficcgt0  37863  cncfiooicclem1  37868  fprodcncf  37876  dvmptmulf  37909  iblsplitf  37944  stoweidlem21  37993  stirlinglem4  38051  stirlinglem13  38060  stirlinglem15  38062  fourierd  38198  fourierclimd  38199  sge0iunmptlemre  38371  sge0iunmpt  38374  sge0ltfirpmpt2  38382  sge0isummpt2  38388  sge0xaddlem2  38390  sge0xadd  38391  meadjiun  38420  omeiunle  38457  caratheodorylem2  38467  ovncvrrp  38504
  Copyright terms: Public domain W3C validator