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

Theorem cbvmpt 4299
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 1629 . . . 4  |-  F/ w
( x  e.  A  /\  z  =  B
)
2 nfv 1629 . . . . 5  |-  F/ x  w  e.  A
3 nfs1v 2182 . . . . 5  |-  F/ x [ w  /  x ] z  =  B
42, 3nfan 1846 . . . 4  |-  F/ x
( w  e.  A  /\  [ w  /  x ] z  =  B )
5 eleq1 2496 . . . . 5  |-  ( x  =  w  ->  (
x  e.  A  <->  w  e.  A ) )
6 sbequ12 1944 . . . . 5  |-  ( x  =  w  ->  (
z  =  B  <->  [ w  /  x ] z  =  B ) )
75, 6anbi12d 692 . . . 4  |-  ( x  =  w  ->  (
( x  e.  A  /\  z  =  B
)  <->  ( w  e.  A  /\  [ w  /  x ] z  =  B ) ) )
81, 4, 7cbvopab1 4278 . . 3  |-  { <. x ,  z >.  |  ( x  e.  A  /\  z  =  B ) }  =  { <. w ,  z >.  |  ( w  e.  A  /\  [ w  /  x ]
z  =  B ) }
9 nfv 1629 . . . . 5  |-  F/ y  w  e.  A
10 cbvmpt.1 . . . . . . 7  |-  F/_ y B
1110nfeq2 2583 . . . . . 6  |-  F/ y  z  =  B
1211nfsb 2185 . . . . 5  |-  F/ y [ w  /  x ] z  =  B
139, 12nfan 1846 . . . 4  |-  F/ y ( w  e.  A  /\  [ w  /  x ] z  =  B )
14 nfv 1629 . . . 4  |-  F/ w
( y  e.  A  /\  z  =  C
)
15 eleq1 2496 . . . . 5  |-  ( w  =  y  ->  (
w  e.  A  <->  y  e.  A ) )
16 sbequ 2111 . . . . . 6  |-  ( w  =  y  ->  ( [ w  /  x ] z  =  B  <->  [ y  /  x ] z  =  B ) )
17 cbvmpt.2 . . . . . . . 8  |-  F/_ x C
1817nfeq2 2583 . . . . . . 7  |-  F/ x  z  =  C
19 cbvmpt.3 . . . . . . . 8  |-  ( x  =  y  ->  B  =  C )
2019eqeq2d 2447 . . . . . . 7  |-  ( x  =  y  ->  (
z  =  B  <->  z  =  C ) )
2118, 20sbie 2149 . . . . . 6  |-  ( [ y  /  x ]
z  =  B  <->  z  =  C )
2216, 21syl6bb 253 . . . . 5  |-  ( w  =  y  ->  ( [ w  /  x ] z  =  B  <-> 
z  =  C ) )
2315, 22anbi12d 692 . . . 4  |-  ( w  =  y  ->  (
( w  e.  A  /\  [ w  /  x ] z  =  B )  <->  ( y  e.  A  /\  z  =  C ) ) )
2413, 14, 23cbvopab1 4278 . . 3  |-  { <. w ,  z >.  |  ( w  e.  A  /\  [ w  /  x ]
z  =  B ) }  =  { <. y ,  z >.  |  ( y  e.  A  /\  z  =  C ) }
258, 24eqtri 2456 . 2  |-  { <. x ,  z >.  |  ( x  e.  A  /\  z  =  B ) }  =  { <. y ,  z >.  |  ( y  e.  A  /\  z  =  C ) }
26 df-mpt 4268 . 2  |-  ( x  e.  A  |->  B )  =  { <. x ,  z >.  |  ( x  e.  A  /\  z  =  B ) }
27 df-mpt 4268 . 2  |-  ( y  e.  A  |->  C )  =  { <. y ,  z >.  |  ( y  e.  A  /\  z  =  C ) }
2825, 26, 273eqtr4i 2466 1  |-  ( x  e.  A  |->  B )  =  ( y  e.  A  |->  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1652   [wsb 1658    e. wcel 1725   F/_wnfc 2559   {copab 4265    e. cmpt 4266
This theorem is referenced by:  cbvmptv  4300  dffn5f  5781  fvmpts  5807  fvmpt2i  5811  fvmptex  5815  fmptcof  5902  fmptcos  5903  fliftfuns  6036  offval2  6322  qliftfuns  6991  axcc2  8317  ac6num  8359  seqof2  11381  cbvsum  12489  summolem2a  12509  zsum  12512  fsum  12514  fsumcvg2  12521  fsumrlim  12590  pcmptdvds  13263  prdsdsval2  13706  gsum2d2  15548  dprd2d2  15602  gsumdixp  15715  psrass1lem  16442  cnmpt1t  17697  cnmpt2k  17720  elmptrab  17859  flfcnp2  18039  prdsxmet  18399  fsumcn  18900  ovoliunlem3  19400  ovoliun  19401  ovoliun2  19402  voliun  19448  mbfpos  19543  mbfposb  19545  i1fposd  19599  itg2cnlem1  19653  isibl2  19658  cbvitg  19667  itgss3  19706  itgfsum  19718  itgabs  19726  itgcn  19734  limcmpt  19770  dvmptfsum  19859  lhop2  19899  dvfsumle  19905  dvfsumlem2  19911  itgsubstlem  19932  itgsubst  19933  itgulm2  20325  rlimcnp2  20805  gsumconstf  24222  xrge0tmd  24332  cbvprod  25241  prodmolem2a  25260  zprod  25263  fprod  25267  itgabsnc  26274  ftc1cnnclem  26278  ftc2nc  26289  ofmpteq  26776  mzpsubst  26805  rabdiophlem2  26862  aomclem8  27136  fsumcnf  27668  cncfmptss  27693  mulc1cncfg  27697  expcnfg  27702  stoweidlem21  27746  stirlinglem4  27802  stirlinglem13  27811  stirlinglem15  27813
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rab 2714  df-v 2958  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-opab 4267  df-mpt 4268
  Copyright terms: Public domain W3C validator