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

Theorem cbvmpt 4126
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 1609 . . . 4  |-  F/ w
( x  e.  A  /\  z  =  B
)
2 nfv 1609 . . . . 5  |-  F/ x  w  e.  A
3 nfs1v 2058 . . . . 5  |-  F/ x [ w  /  x ] z  =  B
42, 3nfan 1783 . . . 4  |-  F/ x
( w  e.  A  /\  [ w  /  x ] z  =  B )
5 eleq1 2356 . . . . 5  |-  ( x  =  w  ->  (
x  e.  A  <->  w  e.  A ) )
6 sbequ12 1872 . . . . 5  |-  ( x  =  w  ->  (
z  =  B  <->  [ w  /  x ] z  =  B ) )
75, 6anbi12d 691 . . . 4  |-  ( x  =  w  ->  (
( x  e.  A  /\  z  =  B
)  <->  ( w  e.  A  /\  [ w  /  x ] z  =  B ) ) )
81, 4, 7cbvopab1 4105 . . 3  |-  { <. x ,  z >.  |  ( x  e.  A  /\  z  =  B ) }  =  { <. w ,  z >.  |  ( w  e.  A  /\  [ w  /  x ]
z  =  B ) }
9 nfv 1609 . . . . 5  |-  F/ y  w  e.  A
10 cbvmpt.1 . . . . . . 7  |-  F/_ y B
1110nfeq2 2443 . . . . . 6  |-  F/ y  z  =  B
1211nfsb 2061 . . . . 5  |-  F/ y [ w  /  x ] z  =  B
139, 12nfan 1783 . . . 4  |-  F/ y ( w  e.  A  /\  [ w  /  x ] z  =  B )
14 nfv 1609 . . . 4  |-  F/ w
( y  e.  A  /\  z  =  C
)
15 eleq1 2356 . . . . 5  |-  ( w  =  y  ->  (
w  e.  A  <->  y  e.  A ) )
16 sbequ 2013 . . . . . 6  |-  ( w  =  y  ->  ( [ w  /  x ] z  =  B  <->  [ y  /  x ] z  =  B ) )
17 cbvmpt.2 . . . . . . . 8  |-  F/_ x C
1817nfeq2 2443 . . . . . . 7  |-  F/ x  z  =  C
19 cbvmpt.3 . . . . . . . 8  |-  ( x  =  y  ->  B  =  C )
2019eqeq2d 2307 . . . . . . 7  |-  ( x  =  y  ->  (
z  =  B  <->  z  =  C ) )
2118, 20sbie 1991 . . . . . 6  |-  ( [ y  /  x ]
z  =  B  <->  z  =  C )
2216, 21syl6bb 252 . . . . 5  |-  ( w  =  y  ->  ( [ w  /  x ] z  =  B  <-> 
z  =  C ) )
2315, 22anbi12d 691 . . . 4  |-  ( w  =  y  ->  (
( w  e.  A  /\  [ w  /  x ] z  =  B )  <->  ( y  e.  A  /\  z  =  C ) ) )
2413, 14, 23cbvopab1 4105 . . 3  |-  { <. w ,  z >.  |  ( w  e.  A  /\  [ w  /  x ]
z  =  B ) }  =  { <. y ,  z >.  |  ( y  e.  A  /\  z  =  C ) }
258, 24eqtri 2316 . 2  |-  { <. x ,  z >.  |  ( x  e.  A  /\  z  =  B ) }  =  { <. y ,  z >.  |  ( y  e.  A  /\  z  =  C ) }
26 df-mpt 4095 . 2  |-  ( x  e.  A  |->  B )  =  { <. x ,  z >.  |  ( x  e.  A  /\  z  =  B ) }
27 df-mpt 4095 . 2  |-  ( y  e.  A  |->  C )  =  { <. y ,  z >.  |  ( y  e.  A  /\  z  =  C ) }
2825, 26, 273eqtr4i 2326 1  |-  ( x  e.  A  |->  B )  =  ( y  e.  A  |->  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1632   [wsb 1638    e. wcel 1696   F/_wnfc 2419   {copab 4092    e. cmpt 4093
This theorem is referenced by:  cbvmptv  4127  dffn5f  5593  fvmpts  5619  fvmpt2i  5623  fvmptex  5626  fmptcof  5708  fmptcos  5709  fliftfuns  5829  offval2  6111  qliftfuns  6761  axcc2  8079  ac6num  8122  cbvsum  12184  summolem2a  12204  zsum  12207  fsum  12209  fsumcvg2  12216  fsumrlim  12285  pcmptdvds  12958  prdsdsval2  13399  gsum2d2  15241  dprd2d2  15295  gsumdixp  15408  psrass1lem  16139  cnmpt1t  17375  cnmpt2k  17398  elmptrab  17538  flfcnp2  17718  prdsxmet  17949  fsumcn  18390  ovoliunlem3  18879  ovoliun  18880  ovoliun2  18881  voliun  18927  mbfpos  19022  mbfposb  19024  i1fposd  19078  itg2cnlem1  19132  isibl2  19137  cbvitg  19146  itgss3  19185  itgfsum  19197  itgabs  19205  itgcn  19213  limcmpt  19249  dvmptfsum  19338  lhop2  19378  dvfsumle  19384  dvfsumlem2  19390  itgsubstlem  19411  itgsubst  19412  itgulm2  19801  rlimcnp2  20277  ballotlemi  23075  ballotlemsval  23083  ballotlemsv  23084  ballotlemrval  23092  ballotlemrinv  23108  xrge0mulc1cn  23338  xrge0tmdALT  23342  xrge0tmd  23343  gsumconstf  23396  esumcvg  23469  dya2iocrrnval  23597  cbvcprod  24137  prodmolem2a  24157  zprod  24160  fprod  24164  itgabsnc  25020  ftc1cnnclem  25024  cbvprodi  25415  ofmpteq  26900  mzpsubst  26929  rabdiophlem2  26986  aomclem8  27262  fsumcnf  27795  fmuldfeqlem1  27815  cncfmptss  27820  mulc1cncfg  27824  expcnfg  27829  itgsin0pilem1  27847  stoweidlem21  27873  stirlinglem2  27927  stirlinglem3  27928  stirlinglem4  27929  stirlinglem8  27933  stirlinglem13  27938  stirlinglem15  27940
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-opab 4094  df-mpt 4095
  Copyright terms: Public domain W3C validator