Theorem mpteq12dv 5207

Description: An equality inference for the maps-to notation. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 16-Dec-2013.) Remove dependency on ax-10 2141, ax-12 2177. (Revised by SN and GG, 1-Dec-2023.)

Hypotheses

Ref	Expression
mpteq12dv.1	⊢ (𝜑 → 𝐴 = 𝐶)
mpteq12dv.2	⊢ (𝜑 → 𝐵 = 𝐷)

Assertion

Ref	Expression
mpteq12dv	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑥)   𝐷(𝑥)

Proof of Theorem mpteq12dv

Step	Hyp	Ref	Expression
1		mpteq12dv.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
2		mpteq12dv.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐷)
3	2	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷)
4	1, 3	mpteq12dva 5206	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108   ↦ cmpt 5201

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-opab 5182  df-mpt 5202

This theorem is referenced by:  mpteq1  5209  mpteq1i  5211  mpteq12i  5218  ovmpt3rab1  7663  offval  7678  offval3  7979  cantnffval  9675  cnfcomlem  9711  fseqenlem1  10036  dfac12lem1  10156  dfac12r  10159  ackbij2lem2  10251  ackbij2lem3  10252  r1om  10255  ccatfval  14589  swrdval  14659  revval  14776  odzval  16809  vdwpc  16998  restval  17438  prdsval  17467  imasval  17523  qusval  17554  mrcfval  17618  cidfval  17686  monfval  17743  ismon  17744  isepi  17751  idfuval  17887  resfval  17903  resfval2  17904  fucval  17972  homafval  18040  idafval  18068  prfval  18209  prf2fval  18211  curfval  18233  curfpropd  18243  hofval  18262  hof2fval  18265  yonedalem3a  18284  yonedalem4a  18285  yonedalem4c  18287  yonedainv  18291  lubfval  18358  glbfval  18371  ipoval  18538  grpinvfval  18959  grpinvfvalALT  18960  grpinvpropd  18996  mulgnn0gsum  19061  cntzfval  19301  pmtrfval  19429  psgnfval  19479  odfval  19511  odfvalALT  19512  sylow1lem2  19578  sylow1lem4  19580  sylow2blem1  19599  sylow3lem1  19606  sylow3lem2  19607  sylow3lem3  19608  sylow3lem6  19611  pj1fval  19673  vrgpfval  19745  gsum2dlem2  19950  gsum2d2  19953  dprdval  19984  dprd2dlem2  20021  dprd2dlem1  20022  dprd2da  20023  dprd2d2  20025  dpjfval  20036  srgbinom  20189  rgspnval  20570  staffval  20799  lspfval  20928  lsppropd  20974  sraval  21131  isphl  21586  ocvfval  21624  pjfval  21664  uvcfval  21742  aspval  21831  asclfval  21837  ressascl  21854  psrval  21873  psrass1lem  21890  psrmulval  21902  mvrfval  21939  opsrval  22002  mpfrcl  22041  evlsval  22042  selvffval  22069  mhpmulcl  22085  psdffval  22093  coe1mul2  22204  cply1mul  22232  evls1fval  22255  evl1fval  22264  evl1maprhm  22315  mamufval  22328  mvmulfval  22478  marepvfval  22501  submafval  22515  mdetfval  22522  madufval  22573  minmar1fval  22582  mat2pmatfval  22659  cpm2mfval  22685  decpmatmullem  22707  decpmatmulsumfsupp  22709  pm2mpval  22731  pm2mpmhmlem1  22754  pm2mpmhmlem2  22755  chpmatfval  22766  ntrfval  22960  clsfval  22961  neifval  23035  lpfval  23074  ordtval  23125  ordtbas2  23127  ordtcnv  23137  ordtrest  23138  ordtrest2  23140  cnpfval  23170  kqval  23662  fmval  23879  fmf  23881  flffval  23925  fcfval  23969  cnextval  23997  tsmsval2  24066  nmfval  24525  nmpropd  24531  nmpropd2  24532  subgnm  24570  tngnm  24588  nmofval  24651  pi1xfrcnv  25006  iscph  25120  tcphval  25168  limcfval  25823  dvfval  25848  eldv  25849  mdegfval  26017  mdegmullem  26033  mdegpropd  26039  coe1mul3  26054  ig1pval  26131  taylfval  26316  ishlg  28527  mirval  28580  ishpg  28684  lmif  28710  islmib  28712  vtxdgfval  29393  vtxdeqd  29403  grpoinvfval  30449  nmoofval  30689  eigvalfval  31824  indv  32775  ressnm  32886  tocycval  33065  idlsrgval  33464  minplyval  33685  ordtprsval  33895  ordtprsuni  33896  ordtrestNEW  33898  ofcfval  34075  ofcfval3  34079  omsval  34271  sitgval  34310  issibf  34311  sitgfval  34319  signstfv  34541  cvmliftlem5  35257  cvmliftlem15  35266  mvrsval  35473  mrsubffval  35475  elmrsubrn  35488  msubffval  35491  mvhfval  35501  msrfval  35505  fwddifval  36126  fwddifnval  36127  tailfval  36336  bj-imdirvallem  37144  bj-endval  37279  cureq  37566  lsatset  38954  lkrfval  39051  pmapfval  39721  pclfvalN  39854  polfvalN  39869  watfvalN  39957  ldilfset  40073  ltrnfset  40082  dilfsetN  40117  trnfsetN  40120  trlfset  40125  trlset  40126  tgrpfset  40709  tendofset  40723  erngfset  40764  erngset  40765  erngfset-rN  40772  erngset-rN  40773  dvafset  40969  diaffval  40995  diafval  40996  dvhfset  41045  docaffvalN  41086  docafvalN  41087  djaffvalN  41098  dibffval  41105  dibfval  41106  dicffval  41139  dicfval  41140  dihffval  41195  dochffval  41314  dochfval  41315  djhffval  41361  lcdfval  41553  mapdffval  41591  mapdfval  41592  hvmapffval  41723  hvmapfval  41724  hdmap1ffval  41760  hdmap1fval  41761  hdmapffval  41791  hdmapfval  41792  hgmapffval  41850  hgmapfval  41851  hlhilset  41899  prjcrvfval  42601  hbtlem1  43094  hbtlem7  43096  cytpval  43173  rfovd  43972  fsovd  43979  fsovcnvlem  43984  dssmapfvd  43988  ntrneibex  44044  mnringvald  44185  ovnval  46518  hspmbllem2  46604  smflimsuplem1  46797  smflimsuplem3  46799  smflimsuplem7  46803  smflimsup  46805  ply1mulgsumlem3  48312  ply1mulgsumlem4  48313  ply1mulgsum  48314  lincval  48333  iinfprg  48974  fucofvalg  49177  precofval3  49230  prcofvalg  49235  lmdfval  49471  cmdfval  49472