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

Theorem mpoeq123dva 7507
Description: An equality deduction for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017.)
Hypotheses
Ref Expression
mpoeq123dv.1 (𝜑𝐴 = 𝐷)
mpoeq123dva.2 ((𝜑𝑥𝐴) → 𝐵 = 𝐸)
mpoeq123dva.3 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → 𝐶 = 𝐹)
Assertion
Ref Expression
mpoeq123dva (𝜑 → (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐷, 𝑦𝐸𝐹))
Distinct variable groups:   𝜑,𝑥   𝜑,𝑦
Allowed substitution hints:   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)   𝐶(𝑥,𝑦)   𝐷(𝑥,𝑦)   𝐸(𝑥,𝑦)   𝐹(𝑥,𝑦)

Proof of Theorem mpoeq123dva
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 mpoeq123dva.3 . . . . . 6 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → 𝐶 = 𝐹)
21eqeq2d 2748 . . . . 5 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → (𝑧 = 𝐶𝑧 = 𝐹))
32pm5.32da 579 . . . 4 (𝜑 → (((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐹)))
4 mpoeq123dva.2 . . . . . . . 8 ((𝜑𝑥𝐴) → 𝐵 = 𝐸)
54eleq2d 2827 . . . . . . 7 ((𝜑𝑥𝐴) → (𝑦𝐵𝑦𝐸))
65pm5.32da 579 . . . . . 6 (𝜑 → ((𝑥𝐴𝑦𝐵) ↔ (𝑥𝐴𝑦𝐸)))
7 mpoeq123dv.1 . . . . . . . 8 (𝜑𝐴 = 𝐷)
87eleq2d 2827 . . . . . . 7 (𝜑 → (𝑥𝐴𝑥𝐷))
98anbi1d 631 . . . . . 6 (𝜑 → ((𝑥𝐴𝑦𝐸) ↔ (𝑥𝐷𝑦𝐸)))
106, 9bitrd 279 . . . . 5 (𝜑 → ((𝑥𝐴𝑦𝐵) ↔ (𝑥𝐷𝑦𝐸)))
1110anbi1d 631 . . . 4 (𝜑 → (((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐹) ↔ ((𝑥𝐷𝑦𝐸) ∧ 𝑧 = 𝐹)))
123, 11bitrd 279 . . 3 (𝜑 → (((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑥𝐷𝑦𝐸) ∧ 𝑧 = 𝐹)))
1312oprabbidv 7499 . 2 (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐷𝑦𝐸) ∧ 𝑧 = 𝐹)})
14 df-mpo 7436 . 2 (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
15 df-mpo 7436 . 2 (𝑥𝐷, 𝑦𝐸𝐹) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐷𝑦𝐸) ∧ 𝑧 = 𝐹)}
1613, 14, 153eqtr4g 2802 1 (𝜑 → (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐷, 𝑦𝐸𝐹))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1540  wcel 2108  {coprab 7432  cmpo 7433
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-oprab 7435  df-mpo 7436
This theorem is referenced by:  mpoeq123dv  7508  natpropd  18024  fucpropd  18025  curfpropd  18278  hofpropd  18312  rngcifuestrc  20639  funcrngcsetc  20640  funcrngcsetcALT  20641  funcringcsetc  20674  rrxdsfi  25445  eengv  28994  elntg  28999  submat1n  33804  rrxtopnfi  46302  eenglngeehlnm  48660
  Copyright terms: Public domain W3C validator