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

Theorem cbvmpt 4508
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 1751 . . . 4  |-  F/ w
( x  e.  A  /\  z  =  B
)
2 nfv 1751 . . . . 5  |-  F/ x  w  e.  A
3 nfs1v 2230 . . . . 5  |-  F/ x [ w  /  x ] z  =  B
42, 3nfan 1983 . . . 4  |-  F/ x
( w  e.  A  /\  [ w  /  x ] z  =  B )
5 eleq1 2492 . . . . 5  |-  ( x  =  w  ->  (
x  e.  A  <->  w  e.  A ) )
6 sbequ12 2046 . . . . 5  |-  ( x  =  w  ->  (
z  =  B  <->  [ w  /  x ] z  =  B ) )
75, 6anbi12d 715 . . . 4  |-  ( x  =  w  ->  (
( x  e.  A  /\  z  =  B
)  <->  ( w  e.  A  /\  [ w  /  x ] z  =  B ) ) )
81, 4, 7cbvopab1 4487 . . 3  |-  { <. x ,  z >.  |  ( x  e.  A  /\  z  =  B ) }  =  { <. w ,  z >.  |  ( w  e.  A  /\  [ w  /  x ]
z  =  B ) }
9 nfv 1751 . . . . 5  |-  F/ y  w  e.  A
10 cbvmpt.1 . . . . . . 7  |-  F/_ y B
1110nfeq2 2599 . . . . . 6  |-  F/ y  z  =  B
1211nfsb 2233 . . . . 5  |-  F/ y [ w  /  x ] z  =  B
139, 12nfan 1983 . . . 4  |-  F/ y ( w  e.  A  /\  [ w  /  x ] z  =  B )
14 nfv 1751 . . . 4  |-  F/ w
( y  e.  A  /\  z  =  C
)
15 eleq1 2492 . . . . 5  |-  ( w  =  y  ->  (
w  e.  A  <->  y  e.  A ) )
16 sbequ 2168 . . . . . 6  |-  ( w  =  y  ->  ( [ w  /  x ] z  =  B  <->  [ y  /  x ] z  =  B ) )
17 cbvmpt.2 . . . . . . . 8  |-  F/_ x C
1817nfeq2 2599 . . . . . . 7  |-  F/ x  z  =  C
19 cbvmpt.3 . . . . . . . 8  |-  ( x  =  y  ->  B  =  C )
2019eqeq2d 2434 . . . . . . 7  |-  ( x  =  y  ->  (
z  =  B  <->  z  =  C ) )
2118, 20sbie 2200 . . . . . 6  |-  ( [ y  /  x ]
z  =  B  <->  z  =  C )
2216, 21syl6bb 264 . . . . 5  |-  ( w  =  y  ->  ( [ w  /  x ] z  =  B  <-> 
z  =  C ) )
2315, 22anbi12d 715 . . . 4  |-  ( w  =  y  ->  (
( w  e.  A  /\  [ w  /  x ] z  =  B )  <->  ( y  e.  A  /\  z  =  C ) ) )
2413, 14, 23cbvopab1 4487 . . 3  |-  { <. w ,  z >.  |  ( w  e.  A  /\  [ w  /  x ]
z  =  B ) }  =  { <. y ,  z >.  |  ( y  e.  A  /\  z  =  C ) }
258, 24eqtri 2449 . 2  |-  { <. x ,  z >.  |  ( x  e.  A  /\  z  =  B ) }  =  { <. y ,  z >.  |  ( y  e.  A  /\  z  =  C ) }
26 df-mpt 4477 . 2  |-  ( x  e.  A  |->  B )  =  { <. x ,  z >.  |  ( x  e.  A  /\  z  =  B ) }
27 df-mpt 4477 . 2  |-  ( y  e.  A  |->  C )  =  { <. y ,  z >.  |  ( y  e.  A  /\  z  =  C ) }
2825, 26, 273eqtr4i 2459 1  |-  ( x  e.  A  |->  B )  =  ( y  e.  A  |->  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    = wceq 1437   [wsb 1786    e. wcel 1867   F/_wnfc 2568   {copab 4474    |-> cmpt 4475
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-rab 2782  df-v 3080  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-sn 3994  df-pr 3996  df-op 4000  df-opab 4476  df-mpt 4477
This theorem is referenced by:  cbvmptv  4509  dffn5f  5927  fvmpts  5958  fvmpt2i  5963  fvmptex  5967  fmptcof  6063  fmptcos  6064  fliftfuns  6213  offval2  6553  ofmpteq  6555  mpt2curryvald  7016  qliftfuns  7449  axcc2  8856  ac6num  8898  seqof2  12257  summolem2a  13748  zsum  13751  fsumcvg2  13760  fsumrlim  13838  cbvprod  13936  prodmolem2a  13955  zprod  13958  fprod  13962  pcmptdvds  14791  prdsdsval2  15334  gsumconstf  17496  gsummpt1n0  17525  gsum2d2  17534  dprd2d2  17605  gsumdixp  17765  psrass1lem  18529  coe1fzgsumdlem  18823  gsumply1eq  18827  evl1gsumdlem  18872  madugsum  19592  cnmpt1t  20604  cnmpt2k  20627  elmptrab  20766  flfcnp2  20946  prdsxmet  21308  fsumcn  21791  ovoliunlem3  22331  ovoliun  22332  ovoliun2  22333  voliun  22381  mbfpos  22481  mbfposb  22483  i1fposd  22539  itg2cnlem1  22593  isibl2  22598  cbvitg  22607  itgss3  22646  itgfsum  22658  itgabs  22666  itgcn  22674  limcmpt  22712  dvmptfsum  22801  lhop2  22841  dvfsumle  22847  dvfsumlem2  22853  itgsubstlem  22874  itgsubst  22875  itgulm2  23226  rlimcnp2  23754  gsummpt2co  28378  esumsnf  28721  mbfposadd  31692  itgabsnc  31715  ftc1cnnclem  31719  ftc2nc  31730  mzpsubst  35299  rabdiophlem2  35354  aomclem8  35629  fsumcnf  36986  disjf1  37084  disjrnmpt2  37090  disjinfi  37095  cncfmptss  37241  mulc1cncfg  37243  expcnfg  37247  icccncfext  37341  cncficcgt0  37342  cncfiooicclem1  37347  fprodcncf  37355  dvmptmulf  37385  iblsplitf  37420  stoweidlem21  37454  stirlinglem4  37512  stirlinglem13  37521  stirlinglem15  37523  fourierd  37658  fourierclimd  37659  sge0iunmptlemre  37795  sge0iunmpt  37798  meadjiun  37817  omeiunle  37851  caratheodorylem2  37861
  Copyright terms: Public domain W3C validator