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

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

Proof of Theorem cbvmpt2v
StepHypRef Expression
1 nfcv 2969 . 2 𝑧𝐶
2 nfcv 2969 . 2 𝑤𝐶
3 nfcv 2969 . 2 𝑥𝐷
4 nfcv 2969 . 2 𝑦𝐷
5 cbvmpt2v.1 . . 3 (𝑥 = 𝑧𝐶 = 𝐸)
6 cbvmpt2v.2 . . 3 (𝑦 = 𝑤𝐸 = 𝐷)
75, 6sylan9eq 2881 . 2 ((𝑥 = 𝑧𝑦 = 𝑤) → 𝐶 = 𝐷)
81, 2, 3, 4, 7cbvmpt2 6994 1 (𝑥𝐴, 𝑦𝐵𝐶) = (𝑧𝐴, 𝑤𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1658  cmpt2 6907
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-sep 5005  ax-nul 5013  ax-pr 5127
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-rab 3126  df-v 3416  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-opab 4936  df-oprab 6909  df-mpt2 6910
This theorem is referenced by:  seqomlem0  7810  dffi3  8606  cantnfsuc  8844  fin23lem33  9482  om2uzrdg  13050  uzrdgsuci  13054  sadcp1  15550  smupp1  15575  imasvscafn  16550  mgmnsgrpex  17772  sgrpnmndex  17773  sylow1  18369  sylow2b  18389  sylow3lem5  18397  sylow3  18399  efgmval  18476  efgtf  18486  frlmphl  20487  pmatcollpw3lem  20958  mp2pm2mplem3  20983  txbas  21741  bcth  23497  opnmbl  23768  mbfimaopn  23822  mbfi1fseq  23887  motplusg  25854  ttgval  26174  opsqrlem3  29556  mdetpmtr12  30436  madjusmdetlem4  30441  fvproj  30444  dya2iocival  30880  sxbrsigalem5  30895  sxbrsigalem6  30896  eulerpart  30989  sseqp1  31003  cvmliftlem15  31826  cvmlift2  31844  opnmbllem0  33989  mblfinlem1  33990  mblfinlem2  33991  sdc  34082  tendoplcbv  36850  dvhvaddcbv  37164  dvhvscacbv  37173  fsovcnvlem  39147  ntrneibex  39211  ioorrnopn  41316  hoidmvle  41608  ovnhoi  41611  hoimbl  41639  smflimlem6  41778  funcrngcsetc  42845  funcrngcsetcALT  42846  funcringcsetc  42882  lmod1zr  43129
  Copyright terms: Public domain W3C validator