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

Theorem cbvmpt 4943
Description: Rule to change the bound variable in a maps-to function, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. (Contributed by NM, 11-Sep-2011.)
Hypotheses
Ref Expression
cbvmpt.1 𝑦𝐵
cbvmpt.2 𝑥𝐶
cbvmpt.3 (𝑥 = 𝑦𝐵 = 𝐶)
Assertion
Ref Expression
cbvmpt (𝑥𝐴𝐵) = (𝑦𝐴𝐶)
Distinct variable groups:   𝑥,𝐴   𝑦,𝐴
Allowed substitution hints:   𝐵(𝑥,𝑦)   𝐶(𝑥,𝑦)

Proof of Theorem cbvmpt
Dummy variables 𝑧 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfv 2005 . . . 4 𝑤(𝑥𝐴𝑧 = 𝐵)
2 nfv 2005 . . . . 5 𝑥 𝑤𝐴
3 nfs1v 2286 . . . . 5 𝑥[𝑤 / 𝑥]𝑧 = 𝐵
42, 3nfan 1990 . . . 4 𝑥(𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)
5 eleq1w 2868 . . . . 5 (𝑥 = 𝑤 → (𝑥𝐴𝑤𝐴))
6 sbequ12 2279 . . . . 5 (𝑥 = 𝑤 → (𝑧 = 𝐵 ↔ [𝑤 / 𝑥]𝑧 = 𝐵))
75, 6anbi12d 618 . . . 4 (𝑥 = 𝑤 → ((𝑥𝐴𝑧 = 𝐵) ↔ (𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)))
81, 4, 7cbvopab1 4917 . . 3 {⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)} = {⟨𝑤, 𝑧⟩ ∣ (𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)}
9 nfv 2005 . . . . 5 𝑦 𝑤𝐴
10 cbvmpt.1 . . . . . . 7 𝑦𝐵
1110nfeq2 2964 . . . . . 6 𝑦 𝑧 = 𝐵
1211nfsb 2602 . . . . 5 𝑦[𝑤 / 𝑥]𝑧 = 𝐵
139, 12nfan 1990 . . . 4 𝑦(𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)
14 nfv 2005 . . . 4 𝑤(𝑦𝐴𝑧 = 𝐶)
15 eleq1w 2868 . . . . 5 (𝑤 = 𝑦 → (𝑤𝐴𝑦𝐴))
16 sbequ 2535 . . . . . 6 (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝑧 = 𝐵 ↔ [𝑦 / 𝑥]𝑧 = 𝐵))
17 cbvmpt.2 . . . . . . . 8 𝑥𝐶
1817nfeq2 2964 . . . . . . 7 𝑥 𝑧 = 𝐶
19 cbvmpt.3 . . . . . . . 8 (𝑥 = 𝑦𝐵 = 𝐶)
2019eqeq2d 2816 . . . . . . 7 (𝑥 = 𝑦 → (𝑧 = 𝐵𝑧 = 𝐶))
2118, 20sbie 2567 . . . . . 6 ([𝑦 / 𝑥]𝑧 = 𝐵𝑧 = 𝐶)
2216, 21syl6bb 278 . . . . 5 (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝑧 = 𝐵𝑧 = 𝐶))
2315, 22anbi12d 618 . . . 4 (𝑤 = 𝑦 → ((𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵) ↔ (𝑦𝐴𝑧 = 𝐶)))
2413, 14, 23cbvopab1 4917 . . 3 {⟨𝑤, 𝑧⟩ ∣ (𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧 = 𝐶)}
258, 24eqtri 2828 . 2 {⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧 = 𝐶)}
26 df-mpt 4924 . 2 (𝑥𝐴𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)}
27 df-mpt 4924 . 2 (𝑦𝐴𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧 = 𝐶)}
2825, 26, 273eqtr4i 2838 1 (𝑥𝐴𝐵) = (𝑦𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1637  [wsb 2060  wcel 2156  wnfc 2935  {copab 4906  cmpt 4923
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-rab 3105  df-v 3393  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-opab 4907  df-mpt 4924
This theorem is referenced by:  cbvmptv  4944  dffn5f  6473  fvmpts  6506  fvmpt2i  6511  fvmptex  6515  fmptcof  6620  fmptcos  6621  fliftfuns  6788  offval2  7144  ofmpteq  7146  mpt2curryvald  7631  qliftfuns  8069  axcc2  9544  ac6num  9586  seqof2  13082  summolem2a  14669  zsum  14672  fsumcvg2  14681  fsumrlim  14765  cbvprod  14866  prodmolem2a  14885  zprod  14888  fprod  14892  pcmptdvds  15815  prdsdsval2  16349  gsumconstf  18536  gsummpt1n0  18565  gsum2d2  18574  dprd2d2  18645  gsumdixp  18811  psrass1lem  19586  coe1fzgsumdlem  19879  gsumply1eq  19883  evl1gsumdlem  19928  madugsum  20660  cnmpt1t  21682  cnmpt2k  21705  elmptrab  21844  flfcnp2  22024  prdsxmet  22387  fsumcn  22886  ovoliunlem3  23485  ovoliun  23486  ovoliun2  23487  voliun  23535  mbfpos  23632  mbfposb  23634  i1fposd  23688  itg2cnlem1  23742  isibl2  23747  cbvitg  23756  itgss3  23795  itgfsum  23807  itgabs  23815  itgcn  23823  limcmpt  23861  dvmptfsum  23952  lhop2  23992  dvfsumle  23998  dvfsumlem2  24004  itgsubstlem  24025  itgsubst  24026  itgulm2  24377  rlimcnp2  24907  gsummpt2co  30105  esumsnf  30451  mbfposadd  33769  itgabsnc  33791  ftc1cnnclem  33795  ftc2nc  33806  mzpsubst  37813  rabdiophlem2  37868  aomclem8  38132  fsumcnf  39674  disjf1  39858  disjrnmpt2  39864  disjinfi  39869  fmptf  39932  cncfmptss  40299  mulc1cncfg  40301  expcnfg  40303  fprodcn  40312  fnlimabslt  40391  climmptf  40393  liminfvalxr  40495  icccncfext  40580  cncficcgt0  40581  cncfiooicclem1  40586  fprodcncf  40594  dvmptmulf  40632  iblsplitf  40665  stoweidlem21  40717  stirlinglem4  40773  stirlinglem13  40782  stirlinglem15  40784  fourierd  40918  fourierclimd  40919  sge0iunmptlemre  41111  sge0iunmpt  41114  sge0ltfirpmpt2  41122  sge0isummpt2  41128  sge0xaddlem2  41130  sge0xadd  41131  meadjiun  41162  meaiunincf  41179  meaiuninc3  41181  omeiunle  41213  caratheodorylem2  41223  ovncvrrp  41260  vonioo  41378  smflim2  41494  smfsup  41502  smfinf  41506  smflimsup  41516  smfliminf  41519
  Copyright terms: Public domain W3C validator