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

Theorem mpoeq123dva 7425
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 2823 . . . . . . 7 ((𝜑𝑥𝐴) → (𝑦𝐵𝑦𝐸))
65pm5.32da 579 . . . . . 6 (𝜑 → ((𝑥𝐴𝑦𝐵) ↔ (𝑥𝐴𝑦𝐸)))
7 mpoeq123dv.1 . . . . . . . 8 (𝜑𝐴 = 𝐷)
87eleq2d 2823 . . . . . . 7 (𝜑 → (𝑥𝐴𝑥𝐷))
98anbi1d 630 . . . . . 6 (𝜑 → ((𝑥𝐴𝑦𝐸) ↔ (𝑥𝐷𝑦𝐸)))
106, 9bitrd 278 . . . . 5 (𝜑 → ((𝑥𝐴𝑦𝐵) ↔ (𝑥𝐷𝑦𝐸)))
1110anbi1d 630 . . . 4 (𝜑 → (((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐹) ↔ ((𝑥𝐷𝑦𝐸) ∧ 𝑧 = 𝐹)))
123, 11bitrd 278 . . 3 (𝜑 → (((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑥𝐷𝑦𝐸) ∧ 𝑧 = 𝐹)))
1312oprabbidv 7417 . 2 (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐷𝑦𝐸) ∧ 𝑧 = 𝐹)})
14 df-mpo 7356 . 2 (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
15 df-mpo 7356 . 2 (𝑥𝐷, 𝑦𝐸𝐹) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐷𝑦𝐸) ∧ 𝑧 = 𝐹)}
1613, 14, 153eqtr4g 2802 1 (𝜑 → (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐷, 𝑦𝐸𝐹))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1541  wcel 2106  {coprab 7352  cmpo 7353
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-oprab 7355  df-mpo 7356
This theorem is referenced by:  mpoeq123dv  7426  natpropd  17825  fucpropd  17826  curfpropd  18082  hofpropd  18116  rrxdsfi  24727  istrkgl  27229  eengv  27757  elntg  27762  submat1n  32198  rrxtopnfi  44429  rngcifuestrc  46196  funcrngcsetc  46197  funcrngcsetcALT  46198  funcringcsetc  46234  eenglngeehlnm  46726
  Copyright terms: Public domain W3C validator