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

Theorem cbvmpt2v 6165
Description: Rule to change the bound variable in a maps-to function, using implicit substitution. With a longer proof analogous to cbvmpt 4379, 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 2577 . 2  |-  F/_ z C
2 nfcv 2577 . 2  |-  F/_ w C
3 nfcv 2577 . 2  |-  F/_ x D
4 nfcv 2577 . 2  |-  F/_ y D
5 cbvmpt2v.1 . . 3  |-  ( x  =  z  ->  C  =  E )
6 cbvmpt2v.2 . . 3  |-  ( y  =  w  ->  E  =  D )
75, 6sylan9eq 2493 . 2  |-  ( ( x  =  z  /\  y  =  w )  ->  C  =  D )
81, 2, 3, 4, 7cbvmpt2 6164 1  |-  ( x  e.  A ,  y  e.  B  |->  C )  =  ( z  e.  A ,  w  e.  B  |->  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1364    e. cmpt2 6092
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 1675  ax-6 1713  ax-7 1733  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410  ax-nul 4418  ax-pr 4528
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 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-rab 2722  df-v 2972  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881  df-opab 4348  df-oprab 6094  df-mpt2 6095
This theorem is referenced by:  seqomlem0  6900  dffi3  7677  cantnfsuc  7874  cantnfsucOLD  7904  fin23lem33  8510  om2uzrdg  11775  uzrdgsuci  11779  sadcp1  13647  smupp1  13672  imasvscafn  14471  sylow1  16095  sylow2b  16115  sylow3lem5  16123  sylow3  16125  efgmval  16202  efgtf  16212  frlmphl  18165  txbas  19099  bcth  20799  opnmbl  21041  mbfimaopn  21093  mbfi1fseq  21158  ttgval  23056  opsqrlem3  25481  dya2iocival  26624  sxbrsigalem5  26639  sxbrsigalem6  26640  eulerpart  26695  sseqp1  26708  cvmliftlem15  27117  cvmlift2  27135  opnmbllem0  28352  mblfinlem1  28353  mblfinlem2  28354  sdc  28565  numclwwlk5  30630  lmod1zr  30876  tendoplcbv  34141  dvhvaddcbv  34456  dvhvscacbv  34465
  Copyright terms: Public domain W3C validator