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

Theorem cbvmpt 4110
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 1605 . . . 4  |-  F/ w
( x  e.  A  /\  z  =  B
)
2 nfv 1605 . . . . 5  |-  F/ x  w  e.  A
3 nfs1v 2045 . . . . 5  |-  F/ x [ w  /  x ] z  =  B
42, 3nfan 1771 . . . 4  |-  F/ x
( w  e.  A  /\  [ w  /  x ] z  =  B )
5 eleq1 2343 . . . . 5  |-  ( x  =  w  ->  (
x  e.  A  <->  w  e.  A ) )
6 sbequ12 1860 . . . . 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 4089 . . 3  |-  { <. x ,  z >.  |  ( x  e.  A  /\  z  =  B ) }  =  { <. w ,  z >.  |  ( w  e.  A  /\  [ w  /  x ]
z  =  B ) }
9 nfv 1605 . . . . 5  |-  F/ y  w  e.  A
10 cbvmpt.1 . . . . . . 7  |-  F/_ y B
1110nfeq2 2430 . . . . . 6  |-  F/ y  z  =  B
1211nfsb 2048 . . . . 5  |-  F/ y [ w  /  x ] z  =  B
139, 12nfan 1771 . . . 4  |-  F/ y ( w  e.  A  /\  [ w  /  x ] z  =  B )
14 nfv 1605 . . . 4  |-  F/ w
( y  e.  A  /\  z  =  C
)
15 eleq1 2343 . . . . 5  |-  ( w  =  y  ->  (
w  e.  A  <->  y  e.  A ) )
16 sbequ 2000 . . . . . 6  |-  ( w  =  y  ->  ( [ w  /  x ] z  =  B  <->  [ y  /  x ] z  =  B ) )
17 cbvmpt.2 . . . . . . . 8  |-  F/_ x C
1817nfeq2 2430 . . . . . . 7  |-  F/ x  z  =  C
19 cbvmpt.3 . . . . . . . 8  |-  ( x  =  y  ->  B  =  C )
2019eqeq2d 2294 . . . . . . 7  |-  ( x  =  y  ->  (
z  =  B  <->  z  =  C ) )
2118, 20sbie 1978 . . . . . 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 4089 . . 3  |-  { <. w ,  z >.  |  ( w  e.  A  /\  [ w  /  x ]
z  =  B ) }  =  { <. y ,  z >.  |  ( y  e.  A  /\  z  =  C ) }
258, 24eqtri 2303 . 2  |-  { <. x ,  z >.  |  ( x  e.  A  /\  z  =  B ) }  =  { <. y ,  z >.  |  ( y  e.  A  /\  z  =  C ) }
26 df-mpt 4079 . 2  |-  ( x  e.  A  |->  B )  =  { <. x ,  z >.  |  ( x  e.  A  /\  z  =  B ) }
27 df-mpt 4079 . 2  |-  ( y  e.  A  |->  C )  =  { <. y ,  z >.  |  ( y  e.  A  /\  z  =  C ) }
2825, 26, 273eqtr4i 2313 1  |-  ( x  e.  A  |->  B )  =  ( y  e.  A  |->  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1623   [wsb 1629    e. wcel 1684   F/_wnfc 2406   {copab 4076    e. cmpt 4077
This theorem is referenced by:  cbvmptv  4111  dffn5f  5577  fvmpts  5603  fvmpt2i  5607  fvmptex  5610  fmptcof  5692  fmptcos  5693  fliftfuns  5813  offval2  6095  qliftfuns  6745  axcc2  8063  ac6num  8106  cbvsum  12168  summolem2a  12188  zsum  12191  fsum  12193  fsumcvg2  12200  fsumrlim  12269  pcmptdvds  12942  prdsdsval2  13383  gsum2d2  15225  dprd2d2  15279  gsumdixp  15392  psrass1lem  16123  cnmpt1t  17359  cnmpt2k  17382  elmptrab  17522  flfcnp2  17702  prdsxmet  17933  fsumcn  18374  ovoliunlem3  18863  ovoliun  18864  ovoliun2  18865  voliun  18911  mbfpos  19006  mbfposb  19008  i1fposd  19062  itg2cnlem1  19116  isibl2  19121  cbvitg  19130  itgss3  19169  itgfsum  19181  itgabs  19189  itgcn  19197  limcmpt  19233  dvmptfsum  19322  lhop2  19362  dvfsumle  19368  dvfsumlem2  19374  itgsubstlem  19395  itgsubst  19396  itgulm2  19785  rlimcnp2  20261  ballotlemi  23059  ballotlemsval  23067  ballotlemsv  23068  ballotlemrval  23076  ballotlemrinv  23092  xrge0mulc1cn  23323  xrge0tmdALT  23327  xrge0tmd  23328  gsumconstf  23381  esumcvg  23454  dya2iocrrnval  23582  cbvprodi  25312  ofmpteq  26797  mzpsubst  26826  rabdiophlem2  26883  aomclem8  27159  fsumcnf  27692  fmuldfeqlem1  27712  cncfmptss  27717  mulc1cncfg  27721  expcnfg  27726  itgsin0pilem1  27744  stoweidlem21  27770  stirlinglem2  27824  stirlinglem3  27825  stirlinglem4  27826  stirlinglem8  27830  stirlinglem13  27835  stirlinglem15  27837
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-opab 4078  df-mpt 4079
  Copyright terms: Public domain W3C validator