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

Theorem cbvmpt 4747
 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 1842 . . . 4 𝑤(𝑥𝐴𝑧 = 𝐵)
2 nfv 1842 . . . . 5 𝑥 𝑤𝐴
3 nfs1v 2436 . . . . 5 𝑥[𝑤 / 𝑥]𝑧 = 𝐵
42, 3nfan 1827 . . . 4 𝑥(𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)
5 eleq1 2688 . . . . 5 (𝑥 = 𝑤 → (𝑥𝐴𝑤𝐴))
6 sbequ12 2110 . . . . 5 (𝑥 = 𝑤 → (𝑧 = 𝐵 ↔ [𝑤 / 𝑥]𝑧 = 𝐵))
75, 6anbi12d 747 . . . 4 (𝑥 = 𝑤 → ((𝑥𝐴𝑧 = 𝐵) ↔ (𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)))
81, 4, 7cbvopab1 4721 . . 3 {⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)} = {⟨𝑤, 𝑧⟩ ∣ (𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)}
9 nfv 1842 . . . . 5 𝑦 𝑤𝐴
10 cbvmpt.1 . . . . . . 7 𝑦𝐵
1110nfeq2 2779 . . . . . 6 𝑦 𝑧 = 𝐵
1211nfsb 2439 . . . . 5 𝑦[𝑤 / 𝑥]𝑧 = 𝐵
139, 12nfan 1827 . . . 4 𝑦(𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)
14 nfv 1842 . . . 4 𝑤(𝑦𝐴𝑧 = 𝐶)
15 eleq1 2688 . . . . 5 (𝑤 = 𝑦 → (𝑤𝐴𝑦𝐴))
16 sbequ 2375 . . . . . 6 (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝑧 = 𝐵 ↔ [𝑦 / 𝑥]𝑧 = 𝐵))
17 cbvmpt.2 . . . . . . . 8 𝑥𝐶
1817nfeq2 2779 . . . . . . 7 𝑥 𝑧 = 𝐶
19 cbvmpt.3 . . . . . . . 8 (𝑥 = 𝑦𝐵 = 𝐶)
2019eqeq2d 2631 . . . . . . 7 (𝑥 = 𝑦 → (𝑧 = 𝐵𝑧 = 𝐶))
2118, 20sbie 2407 . . . . . 6 ([𝑦 / 𝑥]𝑧 = 𝐵𝑧 = 𝐶)
2216, 21syl6bb 276 . . . . 5 (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝑧 = 𝐵𝑧 = 𝐶))
2315, 22anbi12d 747 . . . 4 (𝑤 = 𝑦 → ((𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵) ↔ (𝑦𝐴𝑧 = 𝐶)))
2413, 14, 23cbvopab1 4721 . . 3 {⟨𝑤, 𝑧⟩ ∣ (𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧 = 𝐶)}
258, 24eqtri 2643 . 2 {⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧 = 𝐶)}
26 df-mpt 4728 . 2 (𝑥𝐴𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)}
27 df-mpt 4728 . 2 (𝑦𝐴𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧 = 𝐶)}
2825, 26, 273eqtr4i 2653 1 (𝑥𝐴𝐵) = (𝑦𝐴𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384   = wceq 1482  [wsb 1879   ∈ wcel 1989  Ⅎwnfc 2750  {copab 4710   ↦ cmpt 4727 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-rab 2920  df-v 3200  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-nul 3914  df-if 4085  df-sn 4176  df-pr 4178  df-op 4182  df-opab 4711  df-mpt 4728 This theorem is referenced by:  cbvmptv  4748  dffn5f  6250  fvmpts  6283  fvmpt2i  6288  fvmptex  6292  fmptcof  6395  fmptcos  6396  fliftfuns  6561  offval2  6911  ofmpteq  6913  mpt2curryvald  7393  qliftfuns  7831  axcc2  9256  ac6num  9298  seqof2  12854  summolem2a  14440  zsum  14443  fsumcvg2  14452  fsumrlim  14537  cbvprod  14639  prodmolem2a  14658  zprod  14661  fprod  14665  pcmptdvds  15592  prdsdsval2  16138  gsumconstf  18329  gsummpt1n0  18358  gsum2d2  18367  dprd2d2  18437  gsumdixp  18603  psrass1lem  19371  coe1fzgsumdlem  19665  gsumply1eq  19669  evl1gsumdlem  19714  madugsum  20443  cnmpt1t  21462  cnmpt2k  21485  elmptrab  21624  flfcnp2  21805  prdsxmet  22168  fsumcn  22667  ovoliunlem3  23266  ovoliun  23267  ovoliun2  23268  voliun  23316  mbfpos  23412  mbfposb  23414  i1fposd  23468  itg2cnlem1  23522  isibl2  23527  cbvitg  23536  itgss3  23575  itgfsum  23587  itgabs  23595  itgcn  23603  limcmpt  23641  dvmptfsum  23732  lhop2  23772  dvfsumle  23778  dvfsumlem2  23784  itgsubstlem  23805  itgsubst  23806  itgulm2  24157  rlimcnp2  24687  gsummpt2co  29765  esumsnf  30111  mbfposadd  33437  itgabsnc  33459  ftc1cnnclem  33463  ftc2nc  33474  mzpsubst  37137  rabdiophlem2  37192  aomclem8  37457  fsumcnf  39006  disjf1  39191  disjrnmpt2  39197  disjinfi  39202  fmptf  39270  cncfmptss  39625  mulc1cncfg  39627  expcnfg  39629  fprodcn  39638  fnlimabslt  39717  climmptf  39719  liminfvalxr  39815  icccncfext  39869  cncficcgt0  39870  cncfiooicclem1  39875  fprodcncf  39883  dvmptmulf  39921  iblsplitf  39955  stoweidlem21  40007  stirlinglem4  40063  stirlinglem13  40072  stirlinglem15  40074  fourierd  40208  fourierclimd  40209  sge0iunmptlemre  40401  sge0iunmpt  40404  sge0ltfirpmpt2  40412  sge0isummpt2  40418  sge0xaddlem2  40420  sge0xadd  40421  meadjiun  40452  omeiunle  40500  caratheodorylem2  40510  ovncvrrp  40547  vonioo  40665  smflim2  40781  smfsup  40789  smfinf  40793  smflimsup  40803  smfliminf  40806
 Copyright terms: Public domain W3C validator