Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cbvmpov Structured version   Visualization version   GIF version

Theorem cbvmpov 7229
 Description: Rule to change the bound variable in a maps-to function, using implicit substitution. With a longer proof analogous to cbvmpt 5132, some distinct variable requirements could be eliminated. (Contributed by NM, 11-Jun-2013.)
Hypotheses
Ref Expression
cbvmpov.1 (𝑥 = 𝑧𝐶 = 𝐸)
cbvmpov.2 (𝑦 = 𝑤𝐸 = 𝐷)
Assertion
Ref Expression
cbvmpov (𝑥𝐴, 𝑦𝐵𝐶) = (𝑧𝐴, 𝑤𝐵𝐷)
Distinct variable groups:   𝑥,𝑤,𝑦,𝑧,𝐴   𝑤,𝐵,𝑥,𝑦,𝑧   𝑤,𝐶,𝑧   𝑥,𝐷,𝑦
Allowed substitution hints:   𝐶(𝑥,𝑦)   𝐷(𝑧,𝑤)   𝐸(𝑥,𝑦,𝑧,𝑤)

Proof of Theorem cbvmpov
StepHypRef Expression
1 nfcv 2955 . 2 𝑧𝐶
2 nfcv 2955 . 2 𝑤𝐶
3 nfcv 2955 . 2 𝑥𝐷
4 nfcv 2955 . 2 𝑦𝐷
5 cbvmpov.1 . . 3 (𝑥 = 𝑧𝐶 = 𝐸)
6 cbvmpov.2 . . 3 (𝑦 = 𝑤𝐸 = 𝐷)
75, 6sylan9eq 2853 . 2 ((𝑥 = 𝑧𝑦 = 𝑤) → 𝐶 = 𝐷)
81, 2, 3, 4, 7cbvmpo 7228 1 (𝑥𝐴, 𝑦𝐵𝐶) = (𝑧𝐴, 𝑤𝐵𝐷)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1538   ∈ cmpo 7138 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5168  ax-nul 5175  ax-pr 5296 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-v 3443  df-dif 3884  df-un 3886  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-opab 5094  df-oprab 7140  df-mpo 7141 This theorem is referenced by:  fvproj  7814  seqomlem0  8071  dffi3  8882  cantnfsuc  9120  fin23lem33  9759  om2uzrdg  13322  uzrdgsuci  13326  sadcp1  15797  smupp1  15822  imasvscafn  16805  mgmnsgrpex  18091  sgrpnmndex  18092  sylow1  18724  sylow2b  18744  sylow3lem5  18752  sylow3  18754  efgmval  18834  efgtf  18844  frlmphl  20475  pmatcollpw3lem  21398  mp2pm2mplem3  21423  txbas  22182  bcth  23943  opnmbl  24216  mbfimaopn  24270  mbfi1fseq  24335  motplusg  26346  ttgval  26679  opsqrlem3  29935  fedgmul  31130  mdetpmtr12  31193  madjusmdetlem4  31198  dya2iocival  31656  sxbrsigalem5  31671  sxbrsigalem6  31672  eulerpart  31765  sseqp1  31778  cvmliftlem15  32673  cvmlift2  32691  opnmbllem0  35112  mblfinlem1  35113  mblfinlem2  35114  sdc  35201  tendoplcbv  38090  dvhvaddcbv  38404  dvhvscacbv  38413  fsovcnvlem  40757  ntrneibex  40819  ioorrnopn  42990  hoidmvle  43282  ovnhoi  43285  hoimbl  43313  smflimlem6  43452  funcrngcsetc  44665  funcrngcsetcALT  44666  funcringcsetc  44702  lmod1zr  44943
 Copyright terms: Public domain W3C validator