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

Theorem cbvmpt 4782
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 1883 . . . 4 𝑤(𝑥𝐴𝑧 = 𝐵)
2 nfv 1883 . . . . 5 𝑥 𝑤𝐴
3 nfs1v 2465 . . . . 5 𝑥[𝑤 / 𝑥]𝑧 = 𝐵
42, 3nfan 1868 . . . 4 𝑥(𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)
5 eleq1 2718 . . . . 5 (𝑥 = 𝑤 → (𝑥𝐴𝑤𝐴))
6 sbequ12 2149 . . . . 5 (𝑥 = 𝑤 → (𝑧 = 𝐵 ↔ [𝑤 / 𝑥]𝑧 = 𝐵))
75, 6anbi12d 747 . . . 4 (𝑥 = 𝑤 → ((𝑥𝐴𝑧 = 𝐵) ↔ (𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)))
81, 4, 7cbvopab1 4756 . . 3 {⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)} = {⟨𝑤, 𝑧⟩ ∣ (𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)}
9 nfv 1883 . . . . 5 𝑦 𝑤𝐴
10 cbvmpt.1 . . . . . . 7 𝑦𝐵
1110nfeq2 2809 . . . . . 6 𝑦 𝑧 = 𝐵
1211nfsb 2468 . . . . 5 𝑦[𝑤 / 𝑥]𝑧 = 𝐵
139, 12nfan 1868 . . . 4 𝑦(𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)
14 nfv 1883 . . . 4 𝑤(𝑦𝐴𝑧 = 𝐶)
15 eleq1 2718 . . . . 5 (𝑤 = 𝑦 → (𝑤𝐴𝑦𝐴))
16 sbequ 2404 . . . . . 6 (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝑧 = 𝐵 ↔ [𝑦 / 𝑥]𝑧 = 𝐵))
17 cbvmpt.2 . . . . . . . 8 𝑥𝐶
1817nfeq2 2809 . . . . . . 7 𝑥 𝑧 = 𝐶
19 cbvmpt.3 . . . . . . . 8 (𝑥 = 𝑦𝐵 = 𝐶)
2019eqeq2d 2661 . . . . . . 7 (𝑥 = 𝑦 → (𝑧 = 𝐵𝑧 = 𝐶))
2118, 20sbie 2436 . . . . . 6 ([𝑦 / 𝑥]𝑧 = 𝐵𝑧 = 𝐶)
2216, 21syl6bb 276 . . . . 5 (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝑧 = 𝐵𝑧 = 𝐶))
2315, 22anbi12d 747 . . . 4 (𝑤 = 𝑦 → ((𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵) ↔ (𝑦𝐴𝑧 = 𝐶)))
2413, 14, 23cbvopab1 4756 . . 3 {⟨𝑤, 𝑧⟩ ∣ (𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧 = 𝐶)}
258, 24eqtri 2673 . 2 {⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧 = 𝐶)}
26 df-mpt 4763 . 2 (𝑥𝐴𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)}
27 df-mpt 4763 . 2 (𝑦𝐴𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧 = 𝐶)}
2825, 26, 273eqtr4i 2683 1 (𝑥𝐴𝐵) = (𝑦𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1523  [wsb 1937  wcel 2030  wnfc 2780  {copab 4745  cmpt 4762
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-opab 4746  df-mpt 4763
This theorem is referenced by:  cbvmptv  4783  dffn5f  6291  fvmpts  6324  fvmpt2i  6329  fvmptex  6333  fmptcof  6437  fmptcos  6438  fliftfuns  6604  offval2  6956  ofmpteq  6958  mpt2curryvald  7441  qliftfuns  7877  axcc2  9297  ac6num  9339  seqof2  12899  summolem2a  14490  zsum  14493  fsumcvg2  14502  fsumrlim  14587  cbvprod  14689  prodmolem2a  14708  zprod  14711  fprod  14715  pcmptdvds  15645  prdsdsval2  16191  gsumconstf  18381  gsummpt1n0  18410  gsum2d2  18419  dprd2d2  18489  gsumdixp  18655  psrass1lem  19425  coe1fzgsumdlem  19719  gsumply1eq  19723  evl1gsumdlem  19768  madugsum  20497  cnmpt1t  21516  cnmpt2k  21539  elmptrab  21678  flfcnp2  21858  prdsxmet  22221  fsumcn  22720  ovoliunlem3  23318  ovoliun  23319  ovoliun2  23320  voliun  23368  mbfpos  23463  mbfposb  23465  i1fposd  23519  itg2cnlem1  23573  isibl2  23578  cbvitg  23587  itgss3  23626  itgfsum  23638  itgabs  23646  itgcn  23654  limcmpt  23692  dvmptfsum  23783  lhop2  23823  dvfsumle  23829  dvfsumlem2  23835  itgsubstlem  23856  itgsubst  23857  itgulm2  24208  rlimcnp2  24738  gsummpt2co  29908  esumsnf  30254  mbfposadd  33587  itgabsnc  33609  ftc1cnnclem  33613  ftc2nc  33624  mzpsubst  37628  rabdiophlem2  37683  aomclem8  37948  fsumcnf  39494  disjf1  39683  disjrnmpt2  39689  disjinfi  39694  fmptf  39762  cncfmptss  40137  mulc1cncfg  40139  expcnfg  40141  fprodcn  40150  fnlimabslt  40229  climmptf  40231  liminfvalxr  40333  icccncfext  40418  cncficcgt0  40419  cncfiooicclem1  40424  fprodcncf  40432  dvmptmulf  40470  iblsplitf  40504  stoweidlem21  40556  stirlinglem4  40612  stirlinglem13  40621  stirlinglem15  40623  fourierd  40757  fourierclimd  40758  sge0iunmptlemre  40950  sge0iunmpt  40953  sge0ltfirpmpt2  40961  sge0isummpt2  40967  sge0xaddlem2  40969  sge0xadd  40970  meadjiun  41001  meaiunincf  41018  meaiuninc3  41020  omeiunle  41052  caratheodorylem2  41062  ovncvrrp  41099  vonioo  41217  smflim2  41333  smfsup  41341  smfinf  41345  smflimsup  41355  smfliminf  41358
  Copyright terms: Public domain W3C validator