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

Theorem mpteq12dva 5008
Description: An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017.)
Hypotheses
Ref Expression
mpteq12dv.1 (𝜑𝐴 = 𝐶)
mpteq12dva.2 ((𝜑𝑥𝐴) → 𝐵 = 𝐷)
Assertion
Ref Expression
mpteq12dva (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐶𝐷))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑥)   𝐷(𝑥)

Proof of Theorem mpteq12dva
StepHypRef Expression
1 mpteq12dv.1 . . 3 (𝜑𝐴 = 𝐶)
21alrimiv 1887 . 2 (𝜑 → ∀𝑥 𝐴 = 𝐶)
3 mpteq12dva.2 . . 3 ((𝜑𝑥𝐴) → 𝐵 = 𝐷)
43ralrimiva 3127 . 2 (𝜑 → ∀𝑥𝐴 𝐵 = 𝐷)
5 mpteq12f 5007 . 2 ((∀𝑥 𝐴 = 𝐶 ∧ ∀𝑥𝐴 𝐵 = 𝐷) → (𝑥𝐴𝐵) = (𝑥𝐶𝐷))
62, 4, 5syl2anc 576 1 (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐶𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 387  wal 1506   = wceq 1508  wcel 2051  wral 3083  cmpt 5005
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-12 2107  ax-ext 2745
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2754  df-cleq 2766  df-clel 2841  df-ral 3088  df-opab 4989  df-mpt 5006
This theorem is referenced by:  mpteq12dv  5009  pfxmpt  13859  reps  13988  repswccat  14004  cidpropd  16851  monpropd  16878  fucpropd  17118  curfpropd  17354  hofpropd  17388  yonffthlem  17403  ofco2  20780  pmatcollpw3fi1lem1  21114  rrxnm  23713  ushgredgedg  26730  ushgredgedgloop  26732  cshw1s2  30394  cycpm2tr  30481  sgnsv  30501  extdg1id  30715  ofcfval  31034  ccatmulgnn0dir  31491  signstf0  31517  curunc  34348  cncfiooicc  41637  dvcosax  41671  fourierdlem74  41926  fourierdlem75  41927  fourierdlem93  41945  smfsupxr  42551  smflimsuplem8  42562
  Copyright terms: Public domain W3C validator