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

Theorem cbvmptf 5156
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 2381. See cbvmptfg 5157 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 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 1906 . . . 4 𝑤(𝑥𝐴𝑧 = 𝐵)
2 cbvmptf.1 . . . . . 6 𝑥𝐴
32nfcri 2968 . . . . 5 𝑥 𝑤𝐴
4 nfs1v 2264 . . . . 5 𝑥[𝑤 / 𝑥]𝑧 = 𝐵
53, 4nfan 1891 . . . 4 𝑥(𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)
6 eleq1w 2892 . . . . 5 (𝑥 = 𝑤 → (𝑥𝐴𝑤𝐴))
7 sbequ12 2243 . . . . 5 (𝑥 = 𝑤 → (𝑧 = 𝐵 ↔ [𝑤 / 𝑥]𝑧 = 𝐵))
86, 7anbi12d 630 . . . 4 (𝑥 = 𝑤 → ((𝑥𝐴𝑧 = 𝐵) ↔ (𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)))
91, 5, 8cbvopab1 5130 . . 3 {⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)} = {⟨𝑤, 𝑧⟩ ∣ (𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)}
10 cbvmptf.2 . . . . . 6 𝑦𝐴
1110nfcri 2968 . . . . 5 𝑦 𝑤𝐴
12 cbvmptf.3 . . . . . . 7 𝑦𝐵
1312nfeq2 2992 . . . . . 6 𝑦 𝑧 = 𝐵
1413nfsbv 2340 . . . . 5 𝑦[𝑤 / 𝑥]𝑧 = 𝐵
1511, 14nfan 1891 . . . 4 𝑦(𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)
16 nfv 1906 . . . 4 𝑤(𝑦𝐴𝑧 = 𝐶)
17 eleq1w 2892 . . . . 5 (𝑤 = 𝑦 → (𝑤𝐴𝑦𝐴))
18 sbequ 2081 . . . . . 6 (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝑧 = 𝐵 ↔ [𝑦 / 𝑥]𝑧 = 𝐵))
19 cbvmptf.4 . . . . . . . 8 𝑥𝐶
2019nfeq2 2992 . . . . . . 7 𝑥 𝑧 = 𝐶
21 cbvmptf.5 . . . . . . . 8 (𝑥 = 𝑦𝐵 = 𝐶)
2221eqeq2d 2829 . . . . . . 7 (𝑥 = 𝑦 → (𝑧 = 𝐵𝑧 = 𝐶))
2320, 22sbiev 2321 . . . . . 6 ([𝑦 / 𝑥]𝑧 = 𝐵𝑧 = 𝐶)
2418, 23syl6bb 288 . . . . 5 (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝑧 = 𝐵𝑧 = 𝐶))
2517, 24anbi12d 630 . . . 4 (𝑤 = 𝑦 → ((𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵) ↔ (𝑦𝐴𝑧 = 𝐶)))
2615, 16, 25cbvopab1 5130 . . 3 {⟨𝑤, 𝑧⟩ ∣ (𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧 = 𝐶)}
279, 26eqtri 2841 . 2 {⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧 = 𝐶)}
28 df-mpt 5138 . 2 (𝑥𝐴𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)}
29 df-mpt 5138 . 2 (𝑦𝐴𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧 = 𝐶)}
3027, 28, 293eqtr4i 2851 1 (𝑥𝐴𝐵) = (𝑦𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1528  [wsb 2060  wcel 2105  wnfc 2958  {copab 5119  cmpt 5137
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-opab 5120  df-mpt 5138
This theorem is referenced by:  cbvmpt  5158  resmptf  5900  fvmpt2f  6762  offval2f  7410  suppss2f  30312  fmptdF  30329  acunirnmpt2f  30334  funcnv4mpt  30342  cbvesum  31200  esumpfinvalf  31234  binomcxplemdvbinom  40562  binomcxplemdvsum  40564  binomcxplemnotnn0  40565  supxrleubrnmptf  41603  fnlimfv  41820  fnlimfvre2  41834  fnlimf  41835  limsupequzmptf  41888  sge0iunmptlemre  42574  smflim  42930  smflim2  42957  smfsup  42965  smfinf  42969  smflimsuplem2  42972  smflimsuplem5  42975  smflimsup  42979  smfliminf  42982
  Copyright terms: Public domain W3C validator