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

Theorem mpoeq123dva 7482
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 2743 . . . . 5 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → (𝑧 = 𝐶𝑧 = 𝐹))
32pm5.32da 579 . . . 4 (𝜑 → (((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐹)))
4 mpoeq123dva.2 . . . . . . . 8 ((𝜑𝑥𝐴) → 𝐵 = 𝐸)
54eleq2d 2819 . . . . . . 7 ((𝜑𝑥𝐴) → (𝑦𝐵𝑦𝐸))
65pm5.32da 579 . . . . . 6 (𝜑 → ((𝑥𝐴𝑦𝐵) ↔ (𝑥𝐴𝑦𝐸)))
7 mpoeq123dv.1 . . . . . . . 8 (𝜑𝐴 = 𝐷)
87eleq2d 2819 . . . . . . 7 (𝜑 → (𝑥𝐴𝑥𝐷))
98anbi1d 630 . . . . . 6 (𝜑 → ((𝑥𝐴𝑦𝐸) ↔ (𝑥𝐷𝑦𝐸)))
106, 9bitrd 278 . . . . 5 (𝜑 → ((𝑥𝐴𝑦𝐵) ↔ (𝑥𝐷𝑦𝐸)))
1110anbi1d 630 . . . 4 (𝜑 → (((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐹) ↔ ((𝑥𝐷𝑦𝐸) ∧ 𝑧 = 𝐹)))
123, 11bitrd 278 . . 3 (𝜑 → (((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑥𝐷𝑦𝐸) ∧ 𝑧 = 𝐹)))
1312oprabbidv 7474 . 2 (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐷𝑦𝐸) ∧ 𝑧 = 𝐹)})
14 df-mpo 7413 . 2 (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
15 df-mpo 7413 . 2 (𝑥𝐷, 𝑦𝐸𝐹) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐷𝑦𝐸) ∧ 𝑧 = 𝐹)}
1613, 14, 153eqtr4g 2797 1 (𝜑 → (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐷, 𝑦𝐸𝐹))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1541  wcel 2106  {coprab 7409  cmpo 7410
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 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-oprab 7412  df-mpo 7413
This theorem is referenced by:  mpoeq123dv  7483  natpropd  17928  fucpropd  17929  curfpropd  18185  hofpropd  18219  rrxdsfi  24927  eengv  28234  elntg  28239  submat1n  32780  rrxtopnfi  44993  rngcifuestrc  46885  funcrngcsetc  46886  funcrngcsetcALT  46887  funcringcsetc  46923  eenglngeehlnm  47415
  Copyright terms: Public domain W3C validator