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

Theorem cbvmpt2v 6119
Description: Rule to change the bound variable in a maps-to function, using implicit substitution. With a longer proof analogous to cbvmpt 4267, some distinct variable requirements could be eliminated. (Contributed by NM, 11-Jun-2013.)
Hypotheses
Ref Expression
cbvmpt2v.1  |-  ( x  =  z  ->  C  =  E )
cbvmpt2v.2  |-  ( y  =  w  ->  E  =  D )
Assertion
Ref Expression
cbvmpt2v  |-  ( x  e.  A ,  y  e.  B  |->  C )  =  ( z  e.  A ,  w  e.  B  |->  D )
Distinct variable groups:    x, w, y, z, A    w, B, x, y, z    w, C, z    x, D, y
Allowed substitution hints:    C( x, y)    D( z, w)    E( x, y, z, w)

Proof of Theorem cbvmpt2v
StepHypRef Expression
1 nfcv 2548 . 2  |-  F/_ z C
2 nfcv 2548 . 2  |-  F/_ w C
3 nfcv 2548 . 2  |-  F/_ x D
4 nfcv 2548 . 2  |-  F/_ y D
5 cbvmpt2v.1 . . 3  |-  ( x  =  z  ->  C  =  E )
6 cbvmpt2v.2 . . 3  |-  ( y  =  w  ->  E  =  D )
75, 6sylan9eq 2464 . 2  |-  ( ( x  =  z  /\  y  =  w )  ->  C  =  D )
81, 2, 3, 4, 7cbvmpt2 6118 1  |-  ( x  e.  A ,  y  e.  B  |->  C )  =  ( z  e.  A ,  w  e.  B  |->  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. cmpt2 6050
This theorem is referenced by:  seqomlem0  6673  dffi3  7402  cantnfsuc  7589  fin23lem33  8189  om2uzrdg  11259  uzrdgsuci  11263  sadcp1  12930  smupp1  12955  imasvscafn  13725  sylow1  15200  sylow2b  15220  sylow3lem5  15228  sylow3  15230  efgmval  15307  efgtf  15317  txbas  17560  bcth  19243  opnmbl  19455  mbfimaopn  19509  mbfi1fseq  19574  opsqrlem3  23606  dya2iocival  24584  sxbrsigalem5  24599  sxbrsigalem6  24600  cvmliftlem15  24946  cvmlift2  24964  mblfinlem  26151  sdc  26346  tendoplcbv  31269  dvhvaddcbv  31584  dvhvscacbv  31593
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-sep 4298  ax-nul 4306  ax-pr 4371
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-rab 2683  df-v 2926  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-nul 3597  df-if 3708  df-sn 3788  df-pr 3789  df-op 3791  df-opab 4235  df-oprab 6052  df-mpt2 6053
  Copyright terms: Public domain W3C validator