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

Theorem cbvmptf 4676
 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 1830 . . . 4 𝑤(𝑥𝐴𝑧 = 𝐵)
2 cbvmptf.1 . . . . . 6 𝑥𝐴
32nfcri 2745 . . . . 5 𝑥 𝑤𝐴
4 nfs1v 2425 . . . . 5 𝑥[𝑤 / 𝑥]𝑧 = 𝐵
53, 4nfan 1816 . . . 4 𝑥(𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)
6 eleq1 2676 . . . . 5 (𝑥 = 𝑤 → (𝑥𝐴𝑤𝐴))
7 sbequ12 2097 . . . . 5 (𝑥 = 𝑤 → (𝑧 = 𝐵 ↔ [𝑤 / 𝑥]𝑧 = 𝐵))
86, 7anbi12d 743 . . . 4 (𝑥 = 𝑤 → ((𝑥𝐴𝑧 = 𝐵) ↔ (𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)))
91, 5, 8cbvopab1 4655 . . 3 {⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)} = {⟨𝑤, 𝑧⟩ ∣ (𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)}
10 cbvmptf.2 . . . . . 6 𝑦𝐴
1110nfcri 2745 . . . . 5 𝑦 𝑤𝐴
12 cbvmptf.3 . . . . . . 7 𝑦𝐵
1312nfeq2 2766 . . . . . 6 𝑦 𝑧 = 𝐵
1413nfsb 2428 . . . . 5 𝑦[𝑤 / 𝑥]𝑧 = 𝐵
1511, 14nfan 1816 . . . 4 𝑦(𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)
16 nfv 1830 . . . 4 𝑤(𝑦𝐴𝑧 = 𝐶)
17 eleq1 2676 . . . . 5 (𝑤 = 𝑦 → (𝑤𝐴𝑦𝐴))
18 cbvmptf.4 . . . . . . 7 𝑥𝐶
1918nfeq2 2766 . . . . . 6 𝑥 𝑧 = 𝐶
20 cbvmptf.5 . . . . . . 7 (𝑥 = 𝑦𝐵 = 𝐶)
2120eqeq2d 2620 . . . . . 6 (𝑥 = 𝑦 → (𝑧 = 𝐵𝑧 = 𝐶))
2219, 21sbhypf 3226 . . . . 5 (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝑧 = 𝐵𝑧 = 𝐶))
2317, 22anbi12d 743 . . . 4 (𝑤 = 𝑦 → ((𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵) ↔ (𝑦𝐴𝑧 = 𝐶)))
2415, 16, 23cbvopab1 4655 . . 3 {⟨𝑤, 𝑧⟩ ∣ (𝑤𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧 = 𝐶)}
259, 24eqtri 2632 . 2 {⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧 = 𝐶)}
26 df-mpt 4645 . 2 (𝑥𝐴𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)}
27 df-mpt 4645 . 2 (𝑦𝐴𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧 = 𝐶)}
2825, 26, 273eqtr4i 2642 1 (𝑥𝐴𝐵) = (𝑦𝐴𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475  [wsb 1867   ∈ wcel 1977  Ⅎwnfc 2738  {copab 4642   ↦ cmpt 4643 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-opab 4644  df-mpt 4645 This theorem is referenced by:  fvmpt2f  6192  offval2f  6807  suppss2f  28819  fmptdF  28836  resmptf  28838  acunirnmpt2f  28843  funcnv4mpt  28853  cbvesum  29431  esumpfinvalf  29465  binomcxplemdvbinom  37574  binomcxplemdvsum  37576  binomcxplemnotnn0  37577  fnlimfv  38730  fnlimfvre2  38744  fnlimf  38745  sge0iunmptlemre  39308  smflim  39663
 Copyright terms: Public domain W3C validator