Theorem mpteq12dv 5194

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 2142, ax-12 2178. (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 5193	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   ↦ cmpt 5188

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-opab 5170  df-mpt 5189

This theorem is referenced by:  mpteq1  5196  mpteq1i  5198  mpteq12i  5204  ovmpt3rab1  7647  offval  7662  offval3  7961  cantnffval  9616  cnfcomlem  9652  fseqenlem1  9977  dfac12lem1  10097  dfac12r  10100  ackbij2lem2  10192  ackbij2lem3  10193  r1om  10196  ccatfval  14538  swrdval  14608  revval  14725  odzval  16762  vdwpc  16951  restval  17389  prdsval  17418  imasval  17474  qusval  17505  mrcfval  17569  cidfval  17637  monfval  17694  ismon  17695  isepi  17702  idfuval  17838  resfval  17854  resfval2  17855  fucval  17923  homafval  17991  idafval  18019  prfval  18160  prf2fval  18162  curfval  18184  curfpropd  18194  hofval  18213  hof2fval  18216  yonedalem3a  18235  yonedalem4a  18236  yonedalem4c  18238  yonedainv  18242  lubfval  18309  glbfval  18322  ipoval  18489  grpinvfval  18910  grpinvfvalALT  18911  grpinvpropd  18947  mulgnn0gsum  19012  cntzfval  19252  pmtrfval  19380  psgnfval  19430  odfval  19462  odfvalALT  19463  sylow1lem2  19529  sylow1lem4  19531  sylow2blem1  19550  sylow3lem1  19557  sylow3lem2  19558  sylow3lem3  19559  sylow3lem6  19562  pj1fval  19624  vrgpfval  19696  gsum2dlem2  19901  gsum2d2  19904  dprdval  19935  dprd2dlem2  19972  dprd2dlem1  19973  dprd2da  19974  dprd2d2  19976  dpjfval  19987  srgbinom  20140  rgspnval  20521  staffval  20750  lspfval  20879  lsppropd  20925  sraval  21082  isphl  21537  ocvfval  21575  pjfval  21615  uvcfval  21693  aspval  21782  asclfval  21788  ressascl  21805  psrval  21824  psrass1lem  21841  psrmulval  21853  mvrfval  21890  opsrval  21953  mpfrcl  21992  evlsval  21993  selvffval  22020  mhpmulcl  22036  psdffval  22044  coe1mul2  22155  cply1mul  22183  evls1fval  22206  evl1fval  22215  evl1maprhm  22266  mamufval  22279  mvmulfval  22429  marepvfval  22452  submafval  22466  mdetfval  22473  madufval  22524  minmar1fval  22533  mat2pmatfval  22610  cpm2mfval  22636  decpmatmullem  22658  decpmatmulsumfsupp  22660  pm2mpval  22682  pm2mpmhmlem1  22705  pm2mpmhmlem2  22706  chpmatfval  22717  ntrfval  22911  clsfval  22912  neifval  22986  lpfval  23025  ordtval  23076  ordtbas2  23078  ordtcnv  23088  ordtrest  23089  ordtrest2  23091  cnpfval  23121  kqval  23613  fmval  23830  fmf  23832  flffval  23876  fcfval  23920  cnextval  23948  tsmsval2  24017  nmfval  24476  nmpropd  24482  nmpropd2  24483  subgnm  24521  tngnm  24539  nmofval  24602  pi1xfrcnv  24957  iscph  25070  tcphval  25118  limcfval  25773  dvfval  25798  eldv  25799  mdegfval  25967  mdegmullem  25983  mdegpropd  25989  coe1mul3  26004  ig1pval  26081  taylfval  26266  ishlg  28529  mirval  28582  ishpg  28686  lmif  28712  islmib  28714  vtxdgfval  29395  vtxdeqd  29405  grpoinvfval  30451  nmoofval  30691  eigvalfval  31826  indv  32775  ressnm  32886  tocycval  33065  idlsrgval  33474  minplyval  33695  ordtprsval  33908  ordtprsuni  33909  ordtrestNEW  33911  ofcfval  34088  ofcfval3  34092  omsval  34284  sitgval  34323  issibf  34324  sitgfval  34332  signstfv  34554  cvmliftlem5  35276  cvmliftlem15  35285  mvrsval  35492  mrsubffval  35494  elmrsubrn  35507  msubffval  35510  mvhfval  35520  msrfval  35524  fwddifval  36150  fwddifnval  36151  tailfval  36360  bj-imdirvallem  37168  bj-endval  37303  cureq  37590  lsatset  38983  lkrfval  39080  pmapfval  39750  pclfvalN  39883  polfvalN  39898  watfvalN  39986  ldilfset  40102  ltrnfset  40111  dilfsetN  40146  trnfsetN  40149  trlfset  40154  trlset  40155  tgrpfset  40738  tendofset  40752  erngfset  40793  erngset  40794  erngfset-rN  40801  erngset-rN  40802  dvafset  40998  diaffval  41024  diafval  41025  dvhfset  41074  docaffvalN  41115  docafvalN  41116  djaffvalN  41127  dibffval  41134  dibfval  41135  dicffval  41168  dicfval  41169  dihffval  41224  dochffval  41343  dochfval  41344  djhffval  41390  lcdfval  41582  mapdffval  41620  mapdfval  41621  hvmapffval  41752  hvmapfval  41753  hdmap1ffval  41789  hdmap1fval  41790  hdmapffval  41820  hdmapfval  41821  hgmapffval  41879  hgmapfval  41880  hlhilset  41928  prjcrvfval  42619  hbtlem1  43112  hbtlem7  43114  cytpval  43191  rfovd  43990  fsovd  43997  fsovcnvlem  44002  dssmapfvd  44006  ntrneibex  44062  mnringvald  44202  ovnval  46539  hspmbllem2  46625  smflimsuplem1  46818  smflimsuplem3  46820  smflimsuplem7  46824  smflimsup  46826  ply1mulgsumlem3  48377  ply1mulgsumlem4  48378  ply1mulgsum  48379  lincval  48398  iinfprg  49048  fucofvalg  49307  precofval3  49360  prcofvalg  49365  lmdfval  49638  cmdfval  49639