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

Theorem mpteq12dv 5124
Description: An equality inference for the maps-to notation. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 16-Dec-2013.) Drop ax-10 2146 while shortening its proof. (Revised by Steven Nguyen and Gino Giotto, 1-Dec-2023.)
Hypotheses
Ref Expression
mpteq12dv.1 (𝜑𝐴 = 𝐶)
mpteq12dv.2 (𝜑𝐵 = 𝐷)
Assertion
Ref Expression
mpteq12dv (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐶𝐷))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑥)   𝐷(𝑥)

Proof of Theorem mpteq12dv
StepHypRef Expression
1 nfv 1916 . 2 𝑥𝜑
2 mpteq12dv.1 . 2 (𝜑𝐴 = 𝐶)
3 mpteq12dv.2 . 2 (𝜑𝐵 = 𝐷)
41, 2, 3mpteq12df 5121 1 (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐶𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  cmpt 5119
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-12 2178  ax-ext 2793
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2800  df-cleq 2814  df-clel 2892  df-opab 5102  df-mpt 5120
This theorem is referenced by:  mpteq12i  5132  ovmpt3rab1  7378  offval  7391  offval3  7658  cantnffval  9102  cnfcomlem  9138  fseqenlem1  9427  dfac12lem1  9546  dfac12r  9549  ackbij2lem2  9639  ackbij2lem3  9640  r1om  9643  ccatfval  13904  swrdval  13984  revval  14101  odzval  16105  vdwpc  16293  restval  16678  prdsval  16706  imasval  16762  qusval  16793  mrcfval  16857  cidfval  16925  monfval  16980  ismon  16981  isepi  16988  idfuval  17124  resfval  17140  resfval2  17141  fucval  17206  homafval  17267  idafval  17295  prfval  17427  prf2fval  17429  curfval  17451  curfpropd  17461  hofval  17480  hof2fval  17483  yonedalem3a  17502  yonedalem4a  17503  yonedalem4c  17505  yonedainv  17509  lubfval  17566  glbfval  17579  ipoval  17742  grpinvfval  18120  grpinvfvalALT  18121  grpinvpropd  18152  mulgnn0gsum  18212  cntzfval  18428  pmtrfval  18556  psgnfval  18606  odfval  18638  odfvalALT  18639  sylow1lem2  18702  sylow1lem4  18704  sylow2blem1  18723  sylow3lem1  18730  sylow3lem2  18731  sylow3lem3  18732  sylow3lem6  18735  pj1fval  18798  vrgpfval  18870  gsum2dlem2  19069  gsum2d2  19072  dprdval  19103  dprd2dlem2  19140  dprd2dlem1  19141  dprd2da  19142  dprd2d2  19144  dpjfval  19155  srgbinom  19273  staffval  19593  lspfval  19720  lsppropd  19765  sraval  19923  aspval  20077  asclfval  20083  ressascl  20100  psrval  20117  psrass1lem  20132  psrmulval  20141  mvrfval  20175  opsrval  20230  mpfrcl  20273  evlsval  20274  selvffval  20304  coe1mul2  20412  cply1mul  20437  evls1fval  20457  evl1fval  20466  isphl  20747  ocvfval  20785  pjfval  20825  uvcfval  20903  mamufval  20971  mvmulfval  21126  marepvfval  21149  submafval  21163  mdetfval  21170  madufval  21221  minmar1fval  21230  mat2pmatfval  21306  cpm2mfval  21332  decpmatmullem  21354  decpmatmulsumfsupp  21356  pm2mpval  21378  pm2mpmhmlem1  21401  pm2mpmhmlem2  21402  chpmatfval  21413  ntrfval  21607  clsfval  21608  neifval  21682  lpfval  21721  ordtval  21772  ordtbas2  21774  ordtcnv  21784  ordtrest  21785  ordtrest2  21787  cnpfval  21817  kqval  22309  fmval  22526  fmf  22528  flffval  22572  fcfval  22616  cnextval  22644  tsmsval2  22713  nmfval  23173  nmpropd  23178  nmpropd2  23179  subgnm  23217  tngnm  23235  nmofval  23298  pi1xfrcnv  23640  iscph  23753  tcphval  23800  limcfval  24453  dvfval  24478  eldv  24479  mdegfval  24641  mdegmullem  24657  mdegpropd  24663  coe1mul3  24678  ig1pval  24751  taylfval  24932  ishlg  26374  mirval  26427  ishpg  26531  lmif  26557  islmib  26559  vtxdgfval  27235  vtxdeqd  27245  grpoinvfval  28283  nmoofval  28523  eigvalfval  29658  ressnm  30624  tocycval  30757  ordtprsval  31168  ordtprsuni  31169  ordtrestNEW  31171  indv  31278  ofcfval  31364  ofcfval3  31368  omsval  31558  sitgval  31597  issibf  31598  sitgfval  31606  signstfv  31840  cvmliftlem5  32543  cvmliftlem15  32552  mvrsval  32759  mrsubffval  32761  elmrsubrn  32774  msubffval  32777  mvhfval  32787  msrfval  32791  fwddifval  33630  fwddifnval  33631  tailfval  33727  bj-imdirval  34488  bj-endval  34612  cureq  34911  lsatset  36164  lkrfval  36261  pmapfval  36930  pclfvalN  37063  polfvalN  37078  watfvalN  37166  ldilfset  37282  ltrnfset  37291  dilfsetN  37326  trnfsetN  37329  trlfset  37334  trlset  37335  tgrpfset  37918  tendofset  37932  erngfset  37973  erngset  37974  erngfset-rN  37981  erngset-rN  37982  dvafset  38178  diaffval  38204  diafval  38205  dvhfset  38254  docaffvalN  38295  docafvalN  38296  djaffvalN  38307  dibffval  38314  dibfval  38315  dicffval  38348  dicfval  38349  dihffval  38404  dochffval  38523  dochfval  38524  djhffval  38570  lcdfval  38762  mapdffval  38800  mapdfval  38801  hvmapffval  38932  hvmapfval  38933  hdmap1ffval  38969  hdmap1fval  38970  hdmapffval  39000  hdmapfval  39001  hgmapffval  39059  hgmapfval  39060  hlhilset  39108  hbtlem1  39862  hbtlem7  39864  rgspnval  39907  cytpval  39948  rfovd  40482  fsovd  40489  fsovcnvlem  40494  dssmapfvd  40498  ntrneibex  40558  mnringvald  40704  ovnval  42971  hspmbllem2  43057  smflimsuplem1  43242  smflimsuplem3  43244  smflimsuplem7  43248  smflimsup  43250  ply1mulgsumlem3  44587  ply1mulgsumlem4  44588  ply1mulgsum  44589  lincval  44609
  Copyright terms: Public domain W3C validator