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

Theorem cbvmptf 4883
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 Thierry Arnoux, 9-Mar-2017.)
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 1995 . . . 4 𝑤(𝑥𝐴𝑧 = 𝐵)
2 cbvmptf.1 . . . . . 6 𝑥𝐴
32nfcri 2907 . . . . 5 𝑥 𝑤𝐴
4 nfs1v 2274 . . . . 5 𝑥[𝑤 / 𝑥]𝑧 = 𝐵
53, 4nfan 1980 . . . 4 𝑥(𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)
6 eleq1w 2833 . . . . 5 (𝑥 = 𝑤 → (𝑥𝐴𝑤𝐴))
7 sbequ12 2267 . . . . 5 (𝑥 = 𝑤 → (𝑧 = 𝐵 ↔ [𝑤 / 𝑥]𝑧 = 𝐵))
86, 7anbi12d 616 . . . 4 (𝑥 = 𝑤 → ((𝑥𝐴𝑧 = 𝐵) ↔ (𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)))
91, 5, 8cbvopab1 4858 . . 3 {⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)} = {⟨𝑤, 𝑧⟩ ∣ (𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)}
10 cbvmptf.2 . . . . . 6 𝑦𝐴
1110nfcri 2907 . . . . 5 𝑦 𝑤𝐴
12 cbvmptf.3 . . . . . . 7 𝑦𝐵
1312nfeq2 2929 . . . . . 6 𝑦 𝑧 = 𝐵
1413nfsb 2590 . . . . 5 𝑦[𝑤 / 𝑥]𝑧 = 𝐵
1511, 14nfan 1980 . . . 4 𝑦(𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)
16 nfv 1995 . . . 4 𝑤(𝑦𝐴𝑧 = 𝐶)
17 eleq1w 2833 . . . . 5 (𝑤 = 𝑦 → (𝑤𝐴𝑦𝐴))
18 cbvmptf.4 . . . . . . 7 𝑥𝐶
1918nfeq2 2929 . . . . . 6 𝑥 𝑧 = 𝐶
20 cbvmptf.5 . . . . . . 7 (𝑥 = 𝑦𝐵 = 𝐶)
2120eqeq2d 2781 . . . . . 6 (𝑥 = 𝑦 → (𝑧 = 𝐵𝑧 = 𝐶))
2219, 21sbhypf 3405 . . . . 5 (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝑧 = 𝐵𝑧 = 𝐶))
2317, 22anbi12d 616 . . . 4 (𝑤 = 𝑦 → ((𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵) ↔ (𝑦𝐴𝑧 = 𝐶)))
2415, 16, 23cbvopab1 4858 . . 3 {⟨𝑤, 𝑧⟩ ∣ (𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧 = 𝐶)}
259, 24eqtri 2793 . 2 {⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧 = 𝐶)}
26 df-mpt 4865 . 2 (𝑥𝐴𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)}
27 df-mpt 4865 . 2 (𝑦𝐴𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧 = 𝐶)}
2825, 26, 273eqtr4i 2803 1 (𝑥𝐴𝐵) = (𝑦𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1631  [wsb 2049  wcel 2145  wnfc 2900  {copab 4847  cmpt 4864
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-opab 4848  df-mpt 4865
This theorem is referenced by:  resmptf  5591  fvmpt2f  6427  offval2f  7059  numclwwlk1lem2  27545  numclwwlk1lem2OLD  27546  suppss2f  29778  fmptdF  29795  acunirnmpt2f  29800  funcnv4mpt  29809  cbvesum  30443  esumpfinvalf  30477  binomcxplemdvbinom  39078  binomcxplemdvsum  39080  binomcxplemnotnn0  39081  supxrleubrnmptf  40193  fnlimfv  40410  fnlimfvre2  40424  fnlimf  40425  limsupequzmptf  40478  sge0iunmptlemre  41146  smflim  41502  smflim2  41529  smfsup  41537  smfinf  41541  smflimsuplem2  41544  smflimsuplem5  41547  smflimsup  41551  smfliminf  41554
  Copyright terms: Public domain W3C validator