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

Theorem cbvmpt 4971
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 2015 . . . 4 𝑤(𝑥𝐴𝑧 = 𝐵)
2 nfv 2015 . . . . 5 𝑥 𝑤𝐴
3 nfs1v 2313 . . . . 5 𝑥[𝑤 / 𝑥]𝑧 = 𝐵
42, 3nfan 2004 . . . 4 𝑥(𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)
5 eleq1w 2888 . . . . 5 (𝑥 = 𝑤 → (𝑥𝐴𝑤𝐴))
6 sbequ12 2288 . . . . 5 (𝑥 = 𝑤 → (𝑧 = 𝐵 ↔ [𝑤 / 𝑥]𝑧 = 𝐵))
75, 6anbi12d 626 . . . 4 (𝑥 = 𝑤 → ((𝑥𝐴𝑧 = 𝐵) ↔ (𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)))
81, 4, 7cbvopab1 4945 . . 3 {⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)} = {⟨𝑤, 𝑧⟩ ∣ (𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)}
9 nfv 2015 . . . . 5 𝑦 𝑤𝐴
10 cbvmpt.1 . . . . . . 7 𝑦𝐵
1110nfeq2 2984 . . . . . 6 𝑦 𝑧 = 𝐵
1211nfsb 2574 . . . . 5 𝑦[𝑤 / 𝑥]𝑧 = 𝐵
139, 12nfan 2004 . . . 4 𝑦(𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)
14 nfv 2015 . . . 4 𝑤(𝑦𝐴𝑧 = 𝐶)
15 eleq1w 2888 . . . . 5 (𝑤 = 𝑦 → (𝑤𝐴𝑦𝐴))
16 sbequ 2506 . . . . . 6 (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝑧 = 𝐵 ↔ [𝑦 / 𝑥]𝑧 = 𝐵))
17 cbvmpt.2 . . . . . . . 8 𝑥𝐶
1817nfeq2 2984 . . . . . . 7 𝑥 𝑧 = 𝐶
19 cbvmpt.3 . . . . . . . 8 (𝑥 = 𝑦𝐵 = 𝐶)
2019eqeq2d 2834 . . . . . . 7 (𝑥 = 𝑦 → (𝑧 = 𝐵𝑧 = 𝐶))
2118, 20sbie 2538 . . . . . 6 ([𝑦 / 𝑥]𝑧 = 𝐵𝑧 = 𝐶)
2216, 21syl6bb 279 . . . . 5 (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝑧 = 𝐵𝑧 = 𝐶))
2315, 22anbi12d 626 . . . 4 (𝑤 = 𝑦 → ((𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵) ↔ (𝑦𝐴𝑧 = 𝐶)))
2413, 14, 23cbvopab1 4945 . . 3 {⟨𝑤, 𝑧⟩ ∣ (𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧 = 𝐶)}
258, 24eqtri 2848 . 2 {⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧 = 𝐶)}
26 df-mpt 4952 . 2 (𝑥𝐴𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)}
27 df-mpt 4952 . 2 (𝑦𝐴𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧 = 𝐶)}
2825, 26, 273eqtr4i 2858 1 (𝑥𝐴𝐵) = (𝑦𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386   = wceq 1658  [wsb 2069  wcel 2166  wnfc 2955  {copab 4934  cmpt 4951
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 2390  ax-ext 2802
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 2811  df-cleq 2817  df-clel 2820  df-nfc 2957  df-rab 3125  df-v 3415  df-dif 3800  df-un 3802  df-in 3804  df-ss 3811  df-nul 4144  df-if 4306  df-sn 4397  df-pr 4399  df-op 4403  df-opab 4935  df-mpt 4952
This theorem is referenced by:  cbvmptv  4972  dffn5f  6498  fvmpts  6531  fvmpt2i  6536  fvmptex  6540  fmptcof  6646  fmptcos  6647  fliftfuns  6818  offval2  7173  ofmpteq  7175  mpt2curryvald  7660  qliftfuns  8098  axcc2  9573  ac6num  9615  seqof2  13152  summolem2a  14822  zsum  14825  fsumcvg2  14834  fsumrlim  14916  cbvprod  15017  prodmolem2a  15036  zprod  15039  fprod  15043  pcmptdvds  15968  prdsdsval2  16496  gsumconstf  18687  gsummpt1n0  18716  gsum2d2  18725  dprd2d2  18796  gsumdixp  18962  psrass1lem  19737  coe1fzgsumdlem  20030  gsumply1eq  20034  evl1gsumdlem  20079  madugsum  20816  cnmpt1t  21838  cnmpt2k  21861  elmptrab  22000  flfcnp2  22180  prdsxmet  22543  fsumcn  23042  ovoliunlem3  23669  ovoliun  23670  ovoliun2  23671  voliun  23719  mbfpos  23816  mbfposb  23818  i1fposd  23872  itg2cnlem1  23926  isibl2  23931  cbvitg  23940  itgss3  23979  itgfsum  23991  itgabs  23999  itgcn  24007  limcmpt  24045  dvmptfsum  24136  lhop2  24176  dvfsumle  24182  dvfsumlem2  24188  itgsubstlem  24209  itgsubst  24210  itgulm2  24561  rlimcnp2  25105  gsummpt2co  30324  esumsnf  30670  mbfposadd  33999  itgabsnc  34021  ftc1cnnclem  34025  ftc2nc  34036  mzpsubst  38154  rabdiophlem2  38209  aomclem8  38473  fsumcnf  39997  disjf1  40176  disjrnmpt2  40182  disjinfi  40187  fmptf  40248  cncfmptss  40613  mulc1cncfg  40615  expcnfg  40617  fprodcn  40626  fnlimabslt  40705  climmptf  40707  liminfvalxr  40809  icccncfext  40894  cncficcgt0  40895  cncfiooicclem1  40900  fprodcncf  40908  dvmptmulf  40946  iblsplitf  40979  stoweidlem21  41031  stirlinglem4  41087  stirlinglem13  41096  stirlinglem15  41098  fourierd  41232  fourierclimd  41233  sge0iunmptlemre  41422  sge0iunmpt  41425  sge0ltfirpmpt2  41433  sge0isummpt2  41439  sge0xaddlem2  41441  sge0xadd  41442  meadjiun  41473  meaiunincf  41490  meaiuninc3  41492  omeiunle  41524  caratheodorylem2  41534  ovncvrrp  41571  vonioo  41689  smflim2  41805  smfsup  41813  smfinf  41817  smflimsup  41827  smfliminf  41830
  Copyright terms: Public domain W3C validator