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

Theorem cbvmpt 4668
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 1829 . . . 4 𝑤(𝑥𝐴𝑧 = 𝐵)
2 nfv 1829 . . . . 5 𝑥 𝑤𝐴
3 nfs1v 2421 . . . . 5 𝑥[𝑤 / 𝑥]𝑧 = 𝐵
42, 3nfan 1815 . . . 4 𝑥(𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)
5 eleq1 2672 . . . . 5 (𝑥 = 𝑤 → (𝑥𝐴𝑤𝐴))
6 sbequ12 2095 . . . . 5 (𝑥 = 𝑤 → (𝑧 = 𝐵 ↔ [𝑤 / 𝑥]𝑧 = 𝐵))
75, 6anbi12d 742 . . . 4 (𝑥 = 𝑤 → ((𝑥𝐴𝑧 = 𝐵) ↔ (𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)))
81, 4, 7cbvopab1 4646 . . 3 {⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)} = {⟨𝑤, 𝑧⟩ ∣ (𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)}
9 nfv 1829 . . . . 5 𝑦 𝑤𝐴
10 cbvmpt.1 . . . . . . 7 𝑦𝐵
1110nfeq2 2762 . . . . . 6 𝑦 𝑧 = 𝐵
1211nfsb 2424 . . . . 5 𝑦[𝑤 / 𝑥]𝑧 = 𝐵
139, 12nfan 1815 . . . 4 𝑦(𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)
14 nfv 1829 . . . 4 𝑤(𝑦𝐴𝑧 = 𝐶)
15 eleq1 2672 . . . . 5 (𝑤 = 𝑦 → (𝑤𝐴𝑦𝐴))
16 sbequ 2360 . . . . . 6 (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝑧 = 𝐵 ↔ [𝑦 / 𝑥]𝑧 = 𝐵))
17 cbvmpt.2 . . . . . . . 8 𝑥𝐶
1817nfeq2 2762 . . . . . . 7 𝑥 𝑧 = 𝐶
19 cbvmpt.3 . . . . . . . 8 (𝑥 = 𝑦𝐵 = 𝐶)
2019eqeq2d 2616 . . . . . . 7 (𝑥 = 𝑦 → (𝑧 = 𝐵𝑧 = 𝐶))
2118, 20sbie 2392 . . . . . 6 ([𝑦 / 𝑥]𝑧 = 𝐵𝑧 = 𝐶)
2216, 21syl6bb 274 . . . . 5 (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝑧 = 𝐵𝑧 = 𝐶))
2315, 22anbi12d 742 . . . 4 (𝑤 = 𝑦 → ((𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵) ↔ (𝑦𝐴𝑧 = 𝐶)))
2413, 14, 23cbvopab1 4646 . . 3 {⟨𝑤, 𝑧⟩ ∣ (𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧 = 𝐶)}
258, 24eqtri 2628 . 2 {⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧 = 𝐶)}
26 df-mpt 4636 . 2 (𝑥𝐴𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)}
27 df-mpt 4636 . 2 (𝑦𝐴𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧 = 𝐶)}
2825, 26, 273eqtr4i 2638 1 (𝑥𝐴𝐵) = (𝑦𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474  [wsb 1866  wcel 1976  wnfc 2734  {copab 4633  cmpt 4634
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-rab 2901  df-v 3171  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-nul 3871  df-if 4033  df-sn 4122  df-pr 4124  df-op 4128  df-opab 4635  df-mpt 4636
This theorem is referenced by:  cbvmptv  4669  dffn5f  6144  fvmpts  6176  fvmpt2i  6181  fvmptex  6185  fmptcof  6286  fmptcos  6287  fliftfuns  6439  offval2  6786  ofmpteq  6788  mpt2curryvald  7257  qliftfuns  7695  axcc2  9116  ac6num  9158  seqof2  12673  summolem2a  14236  zsum  14239  fsumcvg2  14248  fsumrlim  14327  cbvprod  14427  prodmolem2a  14446  zprod  14449  fprod  14453  pcmptdvds  15379  prdsdsval2  15910  gsumconstf  18101  gsummpt1n0  18130  gsum2d2  18139  dprd2d2  18209  gsumdixp  18375  psrass1lem  19141  coe1fzgsumdlem  19435  gsumply1eq  19439  evl1gsumdlem  19484  madugsum  20207  cnmpt1t  21217  cnmpt2k  21240  elmptrab  21379  flfcnp2  21560  prdsxmet  21922  fsumcn  22409  ovoliunlem3  22993  ovoliun  22994  ovoliun2  22995  voliun  23043  mbfpos  23138  mbfposb  23140  i1fposd  23194  itg2cnlem1  23248  isibl2  23253  cbvitg  23262  itgss3  23301  itgfsum  23313  itgabs  23321  itgcn  23329  limcmpt  23367  dvmptfsum  23456  lhop2  23496  dvfsumle  23502  dvfsumlem2  23508  itgsubstlem  23529  itgsubst  23530  itgulm2  23881  rlimcnp2  24407  gsummpt2co  28914  esumsnf  29256  mbfposadd  32427  itgabsnc  32449  ftc1cnnclem  32453  ftc2nc  32464  mzpsubst  36129  rabdiophlem2  36184  aomclem8  36449  fsumcnf  38003  disjf1  38164  disjrnmpt2  38170  disjinfi  38175  cncfmptss  38455  mulc1cncfg  38457  expcnfg  38459  fprodcn  38468  fnlimabslt  38547  icccncfext  38574  cncficcgt0  38575  cncfiooicclem1  38580  fprodcncf  38588  dvmptmulf  38628  iblsplitf  38663  stoweidlem21  38715  stirlinglem4  38771  stirlinglem13  38780  stirlinglem15  38782  fourierd  38916  fourierclimd  38917  sge0iunmptlemre  39109  sge0iunmpt  39112  sge0ltfirpmpt2  39120  sge0isummpt2  39126  sge0xaddlem2  39128  sge0xadd  39129  meadjiun  39160  omeiunle  39208  caratheodorylem2  39218  ovncvrrp  39255  vonioo  39374
  Copyright terms: Public domain W3C validator