Theorem mpteq12dv 5187

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   ↦ cmpt 5181

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 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-opab 5163  df-mpt 5182

This theorem is referenced by:  mpteq1  5189  mpteq1i  5191  mpteq12i  5197  ovmpt3rab1  7626  offval  7641  offval3  7936  cantnffval  9584  cnfcomlem  9620  fseqenlem1  9946  dfac12lem1  10066  dfac12r  10069  ackbij2lem2  10161  ackbij2lem3  10162  r1om  10165  ccatfval  14508  swrdval  14579  revval  14695  odzval  16731  vdwpc  16920  restval  17358  prdsval  17387  imasval  17444  qusval  17475  mrcfval  17543  cidfval  17611  monfval  17668  ismon  17669  isepi  17676  idfuval  17812  resfval  17828  resfval2  17829  fucval  17897  homafval  17965  idafval  17993  prfval  18134  prf2fval  18136  curfval  18158  curfpropd  18168  hofval  18187  hof2fval  18190  yonedalem3a  18209  yonedalem4a  18210  yonedalem4c  18212  yonedainv  18216  lubfval  18283  glbfval  18296  ipoval  18465  grpinvfval  18920  grpinvfvalALT  18921  grpinvpropd  18957  mulgnn0gsum  19022  cntzfval  19261  pmtrfval  19391  psgnfval  19441  odfval  19473  odfvalALT  19474  sylow1lem2  19540  sylow1lem4  19542  sylow2blem1  19561  sylow3lem1  19568  sylow3lem2  19569  sylow3lem3  19570  sylow3lem6  19573  pj1fval  19635  vrgpfval  19707  gsum2dlem2  19912  gsum2d2  19915  dprdval  19946  dprd2dlem2  19983  dprd2dlem1  19984  dprd2da  19985  dprd2d2  19987  dpjfval  19998  srgbinom  20178  rgspnval  20557  staffval  20786  lspfval  20936  lsppropd  20982  sraval  21139  isphl  21595  ocvfval  21633  pjfval  21673  uvcfval  21751  aspval  21840  asclfval  21846  ressascl  21864  psrval  21883  psrass1lem  21900  psrmulval  21912  mvrfval  21948  opsrval  22013  mpfrcl  22052  evlsval  22053  selvffval  22088  mhpmulcl  22104  psdffval  22112  coe1mul2  22223  cply1mul  22252  evls1fval  22275  evl1fval  22284  evl1maprhm  22335  mamufval  22348  mvmulfval  22498  marepvfval  22521  submafval  22535  mdetfval  22542  madufval  22593  minmar1fval  22602  mat2pmatfval  22679  cpm2mfval  22705  decpmatmullem  22727  decpmatmulsumfsupp  22729  pm2mpval  22751  pm2mpmhmlem1  22774  pm2mpmhmlem2  22775  chpmatfval  22786  ntrfval  22980  clsfval  22981  neifval  23055  lpfval  23094  ordtval  23145  ordtbas2  23147  ordtcnv  23157  ordtrest  23158  ordtrest2  23160  cnpfval  23190  kqval  23682  fmval  23899  fmf  23901  flffval  23945  fcfval  23989  cnextval  24017  tsmsval2  24086  nmfval  24544  nmpropd  24550  nmpropd2  24551  subgnm  24589  tngnm  24607  nmofval  24670  pi1xfrcnv  25025  iscph  25138  tcphval  25186  limcfval  25841  dvfval  25866  eldv  25867  mdegfval  26035  mdegmullem  26051  mdegpropd  26057  coe1mul3  26072  ig1pval  26149  taylfval  26334  ishlg  28686  mirval  28739  ishpg  28843  lmif  28869  islmib  28871  vtxdgfval  29553  vtxdeqd  29563  grpoinvfval  30609  nmoofval  30849  eigvalfval  31984  indv  32941  ressnm  33056  tocycval  33201  idlsrgval  33595  extvval  33707  extvfval  33708  mplvrpmrhm  33723  issply  33737  minplyval  33882  ordtprsval  34095  ordtprsuni  34096  ordtrestNEW  34098  ofcfval  34275  ofcfval3  34279  omsval  34470  sitgval  34509  issibf  34510  sitgfval  34518  signstfv  34740  cvmliftlem5  35502  cvmliftlem15  35511  mvrsval  35718  mrsubffval  35720  elmrsubrn  35733  msubffval  35736  mvhfval  35746  msrfval  35750  fwddifval  36375  fwddifnval  36376  tailfval  36585  bj-imdirvallem  37429  bj-endval  37564  cureq  37841  lsatset  39360  lkrfval  39457  pmapfval  40126  pclfvalN  40259  polfvalN  40274  watfvalN  40362  ldilfset  40478  ltrnfset  40487  dilfsetN  40522  trnfsetN  40525  trlfset  40530  trlset  40531  tgrpfset  41114  tendofset  41128  erngfset  41169  erngset  41170  erngfset-rN  41177  erngset-rN  41178  dvafset  41374  diaffval  41400  diafval  41401  dvhfset  41450  docaffvalN  41491  docafvalN  41492  djaffvalN  41503  dibffval  41510  dibfval  41511  dicffval  41544  dicfval  41545  dihffval  41600  dochffval  41719  dochfval  41720  djhffval  41766  lcdfval  41958  mapdffval  41996  mapdfval  41997  hvmapffval  42128  hvmapfval  42129  hdmap1ffval  42165  hdmap1fval  42166  hdmapffval  42196  hdmapfval  42197  hgmapffval  42255  hgmapfval  42256  hlhilset  42304  prjcrvfval  42983  hbtlem1  43474  hbtlem7  43476  cytpval  43553  rfovd  44351  fsovd  44358  fsovcnvlem  44363  dssmapfvd  44367  ntrneibex  44423  mnringvald  44563  ovnval  46893  hspmbllem2  46979  smflimsuplem1  47172  smflimsuplem3  47174  smflimsuplem7  47178  smflimsup  47180  ply1mulgsumlem3  48742  ply1mulgsumlem4  48743  ply1mulgsum  48744  lincval  48763  iinfprg  49412  fucofvalg  49671  precofval3  49724  prcofvalg  49729  lmdfval  50002  cmdfval  50003