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

Theorem cbvmpt 4493
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 1760 . . . 4  |-  F/ w
( x  e.  A  /\  z  =  B
)
2 nfv 1760 . . . . 5  |-  F/ x  w  e.  A
3 nfs1v 2265 . . . . 5  |-  F/ x [ w  /  x ] z  =  B
42, 3nfan 2010 . . . 4  |-  F/ x
( w  e.  A  /\  [ w  /  x ] z  =  B )
5 eleq1 2516 . . . . 5  |-  ( x  =  w  ->  (
x  e.  A  <->  w  e.  A ) )
6 sbequ12 2082 . . . . 5  |-  ( x  =  w  ->  (
z  =  B  <->  [ w  /  x ] z  =  B ) )
75, 6anbi12d 716 . . . 4  |-  ( x  =  w  ->  (
( x  e.  A  /\  z  =  B
)  <->  ( w  e.  A  /\  [ w  /  x ] z  =  B ) ) )
81, 4, 7cbvopab1 4472 . . 3  |-  { <. x ,  z >.  |  ( x  e.  A  /\  z  =  B ) }  =  { <. w ,  z >.  |  ( w  e.  A  /\  [ w  /  x ]
z  =  B ) }
9 nfv 1760 . . . . 5  |-  F/ y  w  e.  A
10 cbvmpt.1 . . . . . . 7  |-  F/_ y B
1110nfeq2 2606 . . . . . 6  |-  F/ y  z  =  B
1211nfsb 2268 . . . . 5  |-  F/ y [ w  /  x ] z  =  B
139, 12nfan 2010 . . . 4  |-  F/ y ( w  e.  A  /\  [ w  /  x ] z  =  B )
14 nfv 1760 . . . 4  |-  F/ w
( y  e.  A  /\  z  =  C
)
15 eleq1 2516 . . . . 5  |-  ( w  =  y  ->  (
w  e.  A  <->  y  e.  A ) )
16 sbequ 2204 . . . . . 6  |-  ( w  =  y  ->  ( [ w  /  x ] z  =  B  <->  [ y  /  x ] z  =  B ) )
17 cbvmpt.2 . . . . . . . 8  |-  F/_ x C
1817nfeq2 2606 . . . . . . 7  |-  F/ x  z  =  C
19 cbvmpt.3 . . . . . . . 8  |-  ( x  =  y  ->  B  =  C )
2019eqeq2d 2460 . . . . . . 7  |-  ( x  =  y  ->  (
z  =  B  <->  z  =  C ) )
2118, 20sbie 2236 . . . . . 6  |-  ( [ y  /  x ]
z  =  B  <->  z  =  C )
2216, 21syl6bb 265 . . . . 5  |-  ( w  =  y  ->  ( [ w  /  x ] z  =  B  <-> 
z  =  C ) )
2315, 22anbi12d 716 . . . 4  |-  ( w  =  y  ->  (
( w  e.  A  /\  [ w  /  x ] z  =  B )  <->  ( y  e.  A  /\  z  =  C ) ) )
2413, 14, 23cbvopab1 4472 . . 3  |-  { <. w ,  z >.  |  ( w  e.  A  /\  [ w  /  x ]
z  =  B ) }  =  { <. y ,  z >.  |  ( y  e.  A  /\  z  =  C ) }
258, 24eqtri 2472 . 2  |-  { <. x ,  z >.  |  ( x  e.  A  /\  z  =  B ) }  =  { <. y ,  z >.  |  ( y  e.  A  /\  z  =  C ) }
26 df-mpt 4462 . 2  |-  ( x  e.  A  |->  B )  =  { <. x ,  z >.  |  ( x  e.  A  /\  z  =  B ) }
27 df-mpt 4462 . 2  |-  ( y  e.  A  |->  C )  =  { <. y ,  z >.  |  ( y  e.  A  /\  z  =  C ) }
2825, 26, 273eqtr4i 2482 1  |-  ( x  e.  A  |->  B )  =  ( y  e.  A  |->  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    = wceq 1443   [wsb 1796    e. wcel 1886   F/_wnfc 2578   {copab 4459    |-> cmpt 4460
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-rab 2745  df-v 3046  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-sn 3968  df-pr 3970  df-op 3974  df-opab 4461  df-mpt 4462
This theorem is referenced by:  cbvmptv  4494  dffn5f  5918  fvmpts  5949  fvmpt2i  5954  fvmptex  5958  fmptcof  6055  fmptcos  6056  fliftfuns  6205  offval2  6545  ofmpteq  6547  mpt2curryvald  7014  qliftfuns  7447  axcc2  8864  ac6num  8906  seqof2  12268  summolem2a  13774  zsum  13777  fsumcvg2  13786  fsumrlim  13864  cbvprod  13962  prodmolem2a  13981  zprod  13984  fprod  13988  pcmptdvds  14832  prdsdsval2  15375  gsumconstf  17561  gsummpt1n0  17590  gsum2d2  17599  dprd2d2  17670  gsumdixp  17830  psrass1lem  18594  coe1fzgsumdlem  18888  gsumply1eq  18892  evl1gsumdlem  18937  madugsum  19661  cnmpt1t  20673  cnmpt2k  20696  elmptrab  20835  flfcnp2  21015  prdsxmet  21377  fsumcn  21895  ovoliunlem3  22450  ovoliun  22451  ovoliun2  22452  voliun  22500  mbfpos  22600  mbfposb  22602  i1fposd  22658  itg2cnlem1  22712  isibl2  22717  cbvitg  22726  itgss3  22765  itgfsum  22777  itgabs  22785  itgcn  22793  limcmpt  22831  dvmptfsum  22920  lhop2  22960  dvfsumle  22966  dvfsumlem2  22972  itgsubstlem  22993  itgsubst  22994  itgulm2  23357  rlimcnp2  23885  gsummpt2co  28536  esumsnf  28878  mbfposadd  31981  itgabsnc  32004  ftc1cnnclem  32008  ftc2nc  32019  mzpsubst  35584  rabdiophlem2  35639  aomclem8  35913  fsumcnf  37336  disjf1  37451  disjrnmpt2  37457  disjinfi  37462  cncfmptss  37659  mulc1cncfg  37661  expcnfg  37665  icccncfext  37759  cncficcgt0  37760  cncfiooicclem1  37765  fprodcncf  37773  dvmptmulf  37806  iblsplitf  37841  stoweidlem21  37875  stirlinglem4  37933  stirlinglem13  37942  stirlinglem15  37944  fourierd  38080  fourierclimd  38081  sge0iunmptlemre  38251  sge0iunmpt  38254  sge0ltfirpmpt2  38262  sge0isummpt2  38268  sge0xaddlem2  38270  sge0xadd  38271  meadjiun  38298  omeiunle  38332  caratheodorylem2  38342  ovncvrrp  38380
  Copyright terms: Public domain W3C validator