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

Theorem cbvmptf 4781
 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 1883 . . . 4 𝑤(𝑥𝐴𝑧 = 𝐵)
2 cbvmptf.1 . . . . . 6 𝑥𝐴
32nfcri 2787 . . . . 5 𝑥 𝑤𝐴
4 nfs1v 2465 . . . . 5 𝑥[𝑤 / 𝑥]𝑧 = 𝐵
53, 4nfan 1868 . . . 4 𝑥(𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)
6 eleq1 2718 . . . . 5 (𝑥 = 𝑤 → (𝑥𝐴𝑤𝐴))
7 sbequ12 2149 . . . . 5 (𝑥 = 𝑤 → (𝑧 = 𝐵 ↔ [𝑤 / 𝑥]𝑧 = 𝐵))
86, 7anbi12d 747 . . . 4 (𝑥 = 𝑤 → ((𝑥𝐴𝑧 = 𝐵) ↔ (𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)))
91, 5, 8cbvopab1 4756 . . 3 {⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)} = {⟨𝑤, 𝑧⟩ ∣ (𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)}
10 cbvmptf.2 . . . . . 6 𝑦𝐴
1110nfcri 2787 . . . . 5 𝑦 𝑤𝐴
12 cbvmptf.3 . . . . . . 7 𝑦𝐵
1312nfeq2 2809 . . . . . 6 𝑦 𝑧 = 𝐵
1413nfsb 2468 . . . . 5 𝑦[𝑤 / 𝑥]𝑧 = 𝐵
1511, 14nfan 1868 . . . 4 𝑦(𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)
16 nfv 1883 . . . 4 𝑤(𝑦𝐴𝑧 = 𝐶)
17 eleq1 2718 . . . . 5 (𝑤 = 𝑦 → (𝑤𝐴𝑦𝐴))
18 cbvmptf.4 . . . . . . 7 𝑥𝐶
1918nfeq2 2809 . . . . . 6 𝑥 𝑧 = 𝐶
20 cbvmptf.5 . . . . . . 7 (𝑥 = 𝑦𝐵 = 𝐶)
2120eqeq2d 2661 . . . . . 6 (𝑥 = 𝑦 → (𝑧 = 𝐵𝑧 = 𝐶))
2219, 21sbhypf 3284 . . . . 5 (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝑧 = 𝐵𝑧 = 𝐶))
2317, 22anbi12d 747 . . . 4 (𝑤 = 𝑦 → ((𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵) ↔ (𝑦𝐴𝑧 = 𝐶)))
2415, 16, 23cbvopab1 4756 . . 3 {⟨𝑤, 𝑧⟩ ∣ (𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧 = 𝐶)}
259, 24eqtri 2673 . 2 {⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧 = 𝐶)}
26 df-mpt 4763 . 2 (𝑥𝐴𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)}
27 df-mpt 4763 . 2 (𝑦𝐴𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧 = 𝐶)}
2825, 26, 273eqtr4i 2683 1 (𝑥𝐴𝐵) = (𝑦𝐴𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   = wceq 1523  [wsb 1937   ∈ wcel 2030  Ⅎwnfc 2780  {copab 4745   ↦ cmpt 4762 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-opab 4746  df-mpt 4763 This theorem is referenced by:  resmptf  5486  fvmpt2f  6322  offval2f  6951  numclwlk1lem2  27350  suppss2f  29567  fmptdF  29584  acunirnmpt2f  29589  funcnv4mpt  29598  cbvesum  30232  esumpfinvalf  30266  binomcxplemdvbinom  38869  binomcxplemdvsum  38871  binomcxplemnotnn0  38872  supxrleubrnmptf  39993  fnlimfv  40213  fnlimfvre2  40227  fnlimf  40228  limsupequzmptf  40281  sge0iunmptlemre  40950  smflim  41306  smflim2  41333  smfsup  41341  smfinf  41345  smflimsuplem2  41348  smflimsuplem5  41351  smflimsup  41355  smfliminf  41358
 Copyright terms: Public domain W3C validator