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

Theorem cbvmpt 4372
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 1674 . . . 4  |-  F/ w
( x  e.  A  /\  z  =  B
)
2 nfv 1674 . . . . 5  |-  F/ x  w  e.  A
3 nfs1v 2146 . . . . 5  |-  F/ x [ w  /  x ] z  =  B
42, 3nfan 1861 . . . 4  |-  F/ x
( w  e.  A  /\  [ w  /  x ] z  =  B )
5 eleq1 2495 . . . . 5  |-  ( x  =  w  ->  (
x  e.  A  <->  w  e.  A ) )
6 sbequ12 1937 . . . . 5  |-  ( x  =  w  ->  (
z  =  B  <->  [ w  /  x ] z  =  B ) )
75, 6anbi12d 705 . . . 4  |-  ( x  =  w  ->  (
( x  e.  A  /\  z  =  B
)  <->  ( w  e.  A  /\  [ w  /  x ] z  =  B ) ) )
81, 4, 7cbvopab1 4352 . . 3  |-  { <. x ,  z >.  |  ( x  e.  A  /\  z  =  B ) }  =  { <. w ,  z >.  |  ( w  e.  A  /\  [ w  /  x ]
z  =  B ) }
9 nfv 1674 . . . . 5  |-  F/ y  w  e.  A
10 cbvmpt.1 . . . . . . 7  |-  F/_ y B
1110nfeq2 2582 . . . . . 6  |-  F/ y  z  =  B
1211nfsb 2150 . . . . 5  |-  F/ y [ w  /  x ] z  =  B
139, 12nfan 1861 . . . 4  |-  F/ y ( w  e.  A  /\  [ w  /  x ] z  =  B )
14 nfv 1674 . . . 4  |-  F/ w
( y  e.  A  /\  z  =  C
)
15 eleq1 2495 . . . . 5  |-  ( w  =  y  ->  (
w  e.  A  <->  y  e.  A ) )
16 sbequ 2066 . . . . . 6  |-  ( w  =  y  ->  ( [ w  /  x ] z  =  B  <->  [ y  /  x ] z  =  B ) )
17 cbvmpt.2 . . . . . . . 8  |-  F/_ x C
1817nfeq2 2582 . . . . . . 7  |-  F/ x  z  =  C
19 cbvmpt.3 . . . . . . . 8  |-  ( x  =  y  ->  B  =  C )
2019eqeq2d 2446 . . . . . . 7  |-  ( x  =  y  ->  (
z  =  B  <->  z  =  C ) )
2118, 20sbie 2100 . . . . . 6  |-  ( [ y  /  x ]
z  =  B  <->  z  =  C )
2216, 21syl6bb 261 . . . . 5  |-  ( w  =  y  ->  ( [ w  /  x ] z  =  B  <-> 
z  =  C ) )
2315, 22anbi12d 705 . . . 4  |-  ( w  =  y  ->  (
( w  e.  A  /\  [ w  /  x ] z  =  B )  <->  ( y  e.  A  /\  z  =  C ) ) )
2413, 14, 23cbvopab1 4352 . . 3  |-  { <. w ,  z >.  |  ( w  e.  A  /\  [ w  /  x ]
z  =  B ) }  =  { <. y ,  z >.  |  ( y  e.  A  /\  z  =  C ) }
258, 24eqtri 2455 . 2  |-  { <. x ,  z >.  |  ( x  e.  A  /\  z  =  B ) }  =  { <. y ,  z >.  |  ( y  e.  A  /\  z  =  C ) }
26 df-mpt 4342 . 2  |-  ( x  e.  A  |->  B )  =  { <. x ,  z >.  |  ( x  e.  A  /\  z  =  B ) }
27 df-mpt 4342 . 2  |-  ( y  e.  A  |->  C )  =  { <. y ,  z >.  |  ( y  e.  A  /\  z  =  C ) }
2825, 26, 273eqtr4i 2465 1  |-  ( x  e.  A  |->  B )  =  ( y  e.  A  |->  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1364   [wsb 1701    e. wcel 1757   F/_wnfc 2558   {copab 4339    e. cmpt 4340
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2416
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1702  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rab 2716  df-v 2966  df-dif 3321  df-un 3323  df-in 3325  df-ss 3332  df-nul 3628  df-if 3782  df-sn 3868  df-pr 3870  df-op 3874  df-opab 4341  df-mpt 4342
This theorem is referenced by:  cbvmptv  4373  dffn5f  5736  fvmpts  5766  fvmpt2i  5770  fvmptex  5774  fmptcof  5866  fmptcos  5867  fliftfuns  5996  offval2  6327  ofmpteq  6329  qliftfuns  7177  axcc2  8596  ac6num  8638  seqof2  11850  summolem2a  13178  zsum  13181  fsumcvg2  13190  fsumrlim  13259  pcmptdvds  13941  prdsdsval2  14407  gsum2d2  16442  dprd2d2  16519  gsumdixpOLD  16637  gsumdixp  16638  psrass1lem  17383  madugsum  18293  cnmpt1t  19082  cnmpt2k  19105  elmptrab  19244  flfcnp2  19424  prdsxmet  19788  fsumcn  20290  ovoliunlem3  20831  ovoliun  20832  ovoliun2  20833  voliun  20879  mbfpos  20973  mbfposb  20975  i1fposd  21029  itg2cnlem1  21083  isibl2  21088  cbvitg  21097  itgss3  21136  itgfsum  21148  itgabs  21156  itgcn  21164  limcmpt  21202  dvmptfsum  21291  lhop2  21331  dvfsumle  21337  dvfsumlem2  21343  itgsubstlem  21364  itgsubst  21365  itgulm2  21761  rlimcnp2  22247  gsumconstf  26097  xrge0tmd  26232  cbvprod  27277  prodmolem2a  27296  zprod  27299  fprod  27303  mbfposadd  28285  itgabsnc  28307  ftc1cnnclem  28311  ftc2nc  28322  mzpsubst  28932  rabdiophlem2  28987  aomclem8  29261  fsumcnf  29590  cncfmptss  29615  mulc1cncfg  29618  expcnfg  29621  stoweidlem21  29664  stirlinglem4  29720  stirlinglem13  29729  stirlinglem15  29731
  Copyright terms: Public domain W3C validator