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

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

Proof of Theorem mpt2eq123dva
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 mpt2eq123dva.3 . . . . . 6 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → 𝐶 = 𝐹)
21eqeq2d 2788 . . . . 5 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → (𝑧 = 𝐶𝑧 = 𝐹))
32pm5.32da 574 . . . 4 (𝜑 → (((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐹)))
4 mpt2eq123dva.2 . . . . . . . 8 ((𝜑𝑥𝐴) → 𝐵 = 𝐸)
54eleq2d 2845 . . . . . . 7 ((𝜑𝑥𝐴) → (𝑦𝐵𝑦𝐸))
65pm5.32da 574 . . . . . 6 (𝜑 → ((𝑥𝐴𝑦𝐵) ↔ (𝑥𝐴𝑦𝐸)))
7 mpt2eq123dv.1 . . . . . . . 8 (𝜑𝐴 = 𝐷)
87eleq2d 2845 . . . . . . 7 (𝜑 → (𝑥𝐴𝑥𝐷))
98anbi1d 623 . . . . . 6 (𝜑 → ((𝑥𝐴𝑦𝐸) ↔ (𝑥𝐷𝑦𝐸)))
106, 9bitrd 271 . . . . 5 (𝜑 → ((𝑥𝐴𝑦𝐵) ↔ (𝑥𝐷𝑦𝐸)))
1110anbi1d 623 . . . 4 (𝜑 → (((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐹) ↔ ((𝑥𝐷𝑦𝐸) ∧ 𝑧 = 𝐹)))
123, 11bitrd 271 . . 3 (𝜑 → (((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑥𝐷𝑦𝐸) ∧ 𝑧 = 𝐹)))
1312oprabbidv 6988 . 2 (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐷𝑦𝐸) ∧ 𝑧 = 𝐹)})
14 df-mpt2 6929 . 2 (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
15 df-mpt2 6929 . 2 (𝑥𝐷, 𝑦𝐸𝐹) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐷𝑦𝐸) ∧ 𝑧 = 𝐹)}
1613, 14, 153eqtr4g 2839 1 (𝜑 → (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐷, 𝑦𝐸𝐹))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 386   = wceq 1601   ∈ wcel 2107  {coprab 6925   ↦ cmpt2 6926 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-12 2163  ax-ext 2754 This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-oprab 6928  df-mpt2 6929 This theorem is referenced by:  mpt2eq123dv  6996  natpropd  17032  fucpropd  17033  curfpropd  17270  hofpropd  17304  rrxdsfi  23628  istrkgl  25826  eengv  26345  elntg  26350  submat1n  30477  rrxtopnfi  41445  rngcifuestrc  43026  funcrngcsetc  43027  funcrngcsetcALT  43028  funcringcsetc  43064  eenglngeehlnm  43489
 Copyright terms: Public domain W3C validator