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

Theorem cbvmpt 4547
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 1708 . . . 4  |-  F/ w
( x  e.  A  /\  z  =  B
)
2 nfv 1708 . . . . 5  |-  F/ x  w  e.  A
3 nfs1v 2182 . . . . 5  |-  F/ x [ w  /  x ] z  =  B
42, 3nfan 1929 . . . 4  |-  F/ x
( w  e.  A  /\  [ w  /  x ] z  =  B )
5 eleq1 2529 . . . . 5  |-  ( x  =  w  ->  (
x  e.  A  <->  w  e.  A ) )
6 sbequ12 1993 . . . . 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 4527 . . 3  |-  { <. x ,  z >.  |  ( x  e.  A  /\  z  =  B ) }  =  { <. w ,  z >.  |  ( w  e.  A  /\  [ w  /  x ]
z  =  B ) }
9 nfv 1708 . . . . 5  |-  F/ y  w  e.  A
10 cbvmpt.1 . . . . . . 7  |-  F/_ y B
1110nfeq2 2636 . . . . . 6  |-  F/ y  z  =  B
1211nfsb 2185 . . . . 5  |-  F/ y [ w  /  x ] z  =  B
139, 12nfan 1929 . . . 4  |-  F/ y ( w  e.  A  /\  [ w  /  x ] z  =  B )
14 nfv 1708 . . . 4  |-  F/ w
( y  e.  A  /\  z  =  C
)
15 eleq1 2529 . . . . 5  |-  ( w  =  y  ->  (
w  e.  A  <->  y  e.  A ) )
16 sbequ 2118 . . . . . 6  |-  ( w  =  y  ->  ( [ w  /  x ] z  =  B  <->  [ y  /  x ] z  =  B ) )
17 cbvmpt.2 . . . . . . . 8  |-  F/_ x C
1817nfeq2 2636 . . . . . . 7  |-  F/ x  z  =  C
19 cbvmpt.3 . . . . . . . 8  |-  ( x  =  y  ->  B  =  C )
2019eqeq2d 2471 . . . . . . 7  |-  ( x  =  y  ->  (
z  =  B  <->  z  =  C ) )
2118, 20sbie 2150 . . . . . 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 4527 . . 3  |-  { <. w ,  z >.  |  ( w  e.  A  /\  [ w  /  x ]
z  =  B ) }  =  { <. y ,  z >.  |  ( y  e.  A  /\  z  =  C ) }
258, 24eqtri 2486 . 2  |-  { <. x ,  z >.  |  ( x  e.  A  /\  z  =  B ) }  =  { <. y ,  z >.  |  ( y  e.  A  /\  z  =  C ) }
26 df-mpt 4517 . 2  |-  ( x  e.  A  |->  B )  =  { <. x ,  z >.  |  ( x  e.  A  /\  z  =  B ) }
27 df-mpt 4517 . 2  |-  ( y  e.  A  |->  C )  =  { <. y ,  z >.  |  ( y  e.  A  /\  z  =  C ) }
2825, 26, 273eqtr4i 2496 1  |-  ( x  e.  A  |->  B )  =  ( y  e.  A  |->  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1395   [wsb 1740    e. wcel 1819   F/_wnfc 2605   {copab 4514    |-> cmpt 4515
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-opab 4516  df-mpt 4517
This theorem is referenced by:  cbvmptv  4548  dffn5f  5928  fvmpts  5958  fvmpt2i  5963  fvmptex  5967  fmptcof  6066  fmptcos  6067  fliftfuns  6213  offval2  6555  ofmpteq  6557  mpt2curryvald  7017  qliftfuns  7416  axcc2  8834  ac6num  8876  seqof2  12167  summolem2a  13548  zsum  13551  fsumcvg2  13560  fsumrlim  13636  cbvprod  13733  prodmolem2a  13752  zprod  13755  fprod  13759  pcmptdvds  14424  prdsdsval2  14900  gsumconstf  17081  gsummpt1n0  17118  gsum2d2  17128  dprd2d2  17219  gsumdixpOLD  17383  gsumdixp  17384  psrass1lem  18155  coe1fzgsumdlem  18469  gsumply1eq  18473  evl1gsumdlem  18518  madugsum  19271  cnmpt1t  20291  cnmpt2k  20314  elmptrab  20453  flfcnp2  20633  prdsxmet  20997  fsumcn  21499  ovoliunlem3  22040  ovoliun  22041  ovoliun2  22042  voliun  22089  mbfpos  22183  mbfposb  22185  i1fposd  22239  itg2cnlem1  22293  isibl2  22298  cbvitg  22307  itgss3  22346  itgfsum  22358  itgabs  22366  itgcn  22374  limcmpt  22412  dvmptfsum  22501  lhop2  22541  dvfsumle  22547  dvfsumlem2  22553  itgsubstlem  22574  itgsubst  22575  itgulm2  22929  rlimcnp2  23421  gsummpt2co  27923  esumsnf  28227  mbfposadd  30224  itgabsnc  30246  ftc1cnnclem  30250  ftc2nc  30261  mzpsubst  30843  rabdiophlem2  30897  aomclem8  31169  fsumcnf  31557  cncfmptss  31742  mulc1cncfg  31744  expcnfg  31747  icccncfext  31851  cncficcgt0  31852  cncfiooicclem1  31857  fprodcncf  31865  dvmptmulf  31895  iblsplitf  31930  stoweidlem21  31964  stirlinglem4  32020  stirlinglem13  32029  stirlinglem15  32031  fourierd  32166  fourierclimd  32167
  Copyright terms: Public domain W3C validator