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

Theorem mpteq12dva 4529
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:   ,

Proof of Theorem mpteq12dva
StepHypRef Expression
1 mpteq12dv.1 . . 3
21alrimiv 1719 . 2
3 mpteq12dva.2 . . 3
43ralrimiva 2871 . 2
5 mpteq12f 4528 . 2
62, 4, 5syl2anc 661 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  A.wal 1393  =wceq 1395  e.wcel 1818  A.wral 2807  e.cmpt 4510
This theorem is referenced by:  mpteq12dv  4530  reps  12742  repswccat  12757  cidpropd  15105  monpropd  15132  fucpropd  15346  curfpropd  15502  hofpropd  15536  yonffthlem  15551  ofco2  18953  pmatcollpw3fi1lem1  19287  rrxnm  21823  sgnsv  27717  ofcfval  28097  ccatmulgnn0dir  28496  signstf0  28525  cncfiooicc  31697  dvcosax  31723  fourierdlem74  31963  fourierdlem75  31964  fourierdlem93  31982
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-ral 2812  df-opab 4511  df-mpt 4512
  Copyright terms: Public domain W3C validator