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

Theorem cbvmpov 7488
Description: Rule to change the bound variable in a maps-to function, using implicit substitution. With a longer proof analogous to cbvmpt 5252, 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 2902 . 2 𝑧𝐶
2 nfcv 2902 . 2 𝑤𝐶
3 nfcv 2902 . 2 𝑥𝐷
4 nfcv 2902 . 2 𝑦𝐷
5 cbvmpov.1 . . 3 (𝑥 = 𝑧𝐶 = 𝐸)
6 cbvmpov.2 . . 3 (𝑦 = 𝑤𝐸 = 𝐷)
75, 6sylan9eq 2791 . 2 ((𝑥 = 𝑧𝑦 = 𝑤) → 𝐶 = 𝐷)
81, 2, 3, 4, 7cbvmpo 7487 1 (𝑥𝐴, 𝑦𝐵𝐶) = (𝑧𝐴, 𝑤𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  cmpo 7395
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5292  ax-nul 5299  ax-pr 5420
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-rab 3432  df-v 3475  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4523  df-sn 4623  df-pr 4625  df-op 4629  df-opab 5204  df-oprab 7397  df-mpo 7398
This theorem is referenced by:  fvproj  8102  seqomlem0  8431  dffi3  9408  cantnfsuc  9647  fin23lem33  10322  om2uzrdg  13903  uzrdgsuci  13907  sadcp1  16378  smupp1  16403  imasvscafn  17465  mgmnsgrpex  18787  sgrpnmndex  18788  sylow1  19435  sylow2b  19455  sylow3lem5  19463  sylow3  19465  efgmval  19544  efgtf  19554  frlmphl  21269  pmatcollpw3lem  22214  mp2pm2mplem3  22239  txbas  23000  bcth  24775  opnmbl  25048  mbfimaopn  25102  mbfi1fseq  25168  motplusg  27658  ttgval  27991  ttgvalOLD  27992  opsqrlem3  31258  fedgmul  32554  mdetpmtr12  32636  madjusmdetlem4  32641  dya2iocival  33103  sxbrsigalem5  33118  sxbrsigalem6  33119  eulerpart  33212  sseqp1  33225  cvmliftlem15  34120  cvmlift2  34138  opnmbllem0  36328  mblfinlem1  36329  mblfinlem2  36330  sdc  36417  tendoplcbv  39451  dvhvaddcbv  39765  dvhvscacbv  39774  fsovcnvlem  42535  ntrneibex  42595  ioorrnopn  44794  hoidmvle  45089  ovnhoi  45092  hoimbl  45120  smflimlem6  45265  funcrngcsetc  46544  funcrngcsetcALT  46545  funcringcsetc  46581  lmod1zr  46822  functhinclem4  47312
  Copyright terms: Public domain W3C validator