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

Theorem cbvmptf 5256
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.) (Revised by Thierry Arnoux, 9-Mar-2017.) Add disjoint variable condition to avoid ax-13 2374. See cbvmptfg 5257 for a less restrictive version requiring more axioms. (Revised by GG, 17-Jan-2024.)
Hypotheses
Ref Expression
cbvmptf.1 𝑥𝐴
cbvmptf.2 𝑦𝐴
cbvmptf.3 𝑦𝐵
cbvmptf.4 𝑥𝐶
cbvmptf.5 (𝑥 = 𝑦𝐵 = 𝐶)
Assertion
Ref Expression
cbvmptf (𝑥𝐴𝐵) = (𝑦𝐴𝐶)
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)   𝐶(𝑥,𝑦)

Proof of Theorem cbvmptf
Dummy variables 𝑧 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfv 1911 . . . 4 𝑤(𝑥𝐴𝑧 = 𝐵)
2 cbvmptf.1 . . . . . 6 𝑥𝐴
32nfcri 2894 . . . . 5 𝑥 𝑤𝐴
4 nfs1v 2153 . . . . 5 𝑥[𝑤 / 𝑥]𝑧 = 𝐵
53, 4nfan 1896 . . . 4 𝑥(𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)
6 eleq1w 2821 . . . . 5 (𝑥 = 𝑤 → (𝑥𝐴𝑤𝐴))
7 sbequ12 2248 . . . . 5 (𝑥 = 𝑤 → (𝑧 = 𝐵 ↔ [𝑤 / 𝑥]𝑧 = 𝐵))
86, 7anbi12d 632 . . . 4 (𝑥 = 𝑤 → ((𝑥𝐴𝑧 = 𝐵) ↔ (𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)))
91, 5, 8cbvopab1 5222 . . 3 {⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)} = {⟨𝑤, 𝑧⟩ ∣ (𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)}
10 cbvmptf.2 . . . . . 6 𝑦𝐴
1110nfcri 2894 . . . . 5 𝑦 𝑤𝐴
12 cbvmptf.3 . . . . . . 7 𝑦𝐵
1312nfeq2 2920 . . . . . 6 𝑦 𝑧 = 𝐵
1413nfsbv 2328 . . . . 5 𝑦[𝑤 / 𝑥]𝑧 = 𝐵
1511, 14nfan 1896 . . . 4 𝑦(𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)
16 nfv 1911 . . . 4 𝑤(𝑦𝐴𝑧 = 𝐶)
17 eleq1w 2821 . . . . 5 (𝑤 = 𝑦 → (𝑤𝐴𝑦𝐴))
18 sbequ 2080 . . . . . 6 (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝑧 = 𝐵 ↔ [𝑦 / 𝑥]𝑧 = 𝐵))
19 cbvmptf.4 . . . . . . . 8 𝑥𝐶
2019nfeq2 2920 . . . . . . 7 𝑥 𝑧 = 𝐶
21 cbvmptf.5 . . . . . . . 8 (𝑥 = 𝑦𝐵 = 𝐶)
2221eqeq2d 2745 . . . . . . 7 (𝑥 = 𝑦 → (𝑧 = 𝐵𝑧 = 𝐶))
2320, 22sbiev 2312 . . . . . 6 ([𝑦 / 𝑥]𝑧 = 𝐵𝑧 = 𝐶)
2418, 23bitrdi 287 . . . . 5 (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝑧 = 𝐵𝑧 = 𝐶))
2517, 24anbi12d 632 . . . 4 (𝑤 = 𝑦 → ((𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵) ↔ (𝑦𝐴𝑧 = 𝐶)))
2615, 16, 25cbvopab1 5222 . . 3 {⟨𝑤, 𝑧⟩ ∣ (𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧 = 𝐶)}
279, 26eqtri 2762 . 2 {⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧 = 𝐶)}
28 df-mpt 5231 . 2 (𝑥𝐴𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)}
29 df-mpt 5231 . 2 (𝑦𝐴𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧 = 𝐶)}
3027, 28, 293eqtr4i 2772 1 (𝑥𝐴𝐵) = (𝑦𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1536  [wsb 2061  wcel 2105  wnfc 2887  {copab 5209  cmpt 5230
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-opab 5210  df-mpt 5231
This theorem is referenced by:  cbvmpt  5258  resmptf  6058  fvmpt2f  7016  offval2f  7711  suppss2f  32654  fmptdF  32672  acunirnmpt2f  32677  funcnv4mpt  32685  cbvesum  34022  esumpfinvalf  34056  binomcxplemdvbinom  44348  binomcxplemdvsum  44350  binomcxplemnotnn0  44351  fmptff  45214  supxrleubrnmptf  45400  fnlimfv  45618  fnlimfvre2  45632  fnlimf  45633  limsupequzmptf  45686  sge0iunmptlemre  46370  smflim  46732  smflim2  46761  smfsup  46769  smfinf  46773  smflimsuplem2  46776  smflimsuplem5  46779  smflimsup  46783  smfliminf  46786
  Copyright terms: Public domain W3C validator