Theorem mpteq12dv 5173

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 5172	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))

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

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 5149  df-mpt 5168

This theorem is referenced by:  mpteq1  5175  mpteq1i  5177  mpteq12i  5183  ovmpt3rab1  7618  offval  7633  offval3  7928  cantnffval  9575  cnfcomlem  9611  fseqenlem1  9937  dfac12lem1  10057  dfac12r  10060  ackbij2lem2  10152  ackbij2lem3  10153  r1om  10156  indv  12152  ccatfval  14526  swrdval  14597  revval  14713  odzval  16753  vdwpc  16942  restval  17380  prdsval  17409  imasval  17466  qusval  17497  mrcfval  17565  cidfval  17633  monfval  17690  ismon  17691  isepi  17698  idfuval  17834  resfval  17850  resfval2  17851  fucval  17919  homafval  17987  idafval  18015  prfval  18156  prf2fval  18158  curfval  18180  curfpropd  18190  hofval  18209  hof2fval  18212  yonedalem3a  18231  yonedalem4a  18232  yonedalem4c  18234  yonedainv  18238  lubfval  18305  glbfval  18318  ipoval  18487  grpinvfval  18945  grpinvfvalALT  18946  grpinvpropd  18982  mulgnn0gsum  19047  cntzfval  19286  pmtrfval  19416  psgnfval  19466  odfval  19498  odfvalALT  19499  sylow1lem2  19565  sylow1lem4  19567  sylow2blem1  19586  sylow3lem1  19593  sylow3lem2  19594  sylow3lem3  19595  sylow3lem6  19598  pj1fval  19660  vrgpfval  19732  gsum2dlem2  19937  gsum2d2  19940  dprdval  19971  dprd2dlem2  20008  dprd2dlem1  20009  dprd2da  20010  dprd2d2  20012  dpjfval  20023  srgbinom  20203  rgspnval  20580  staffval  20809  lspfval  20959  lsppropd  21005  sraval  21162  isphl  21618  ocvfval  21656  pjfval  21696  uvcfval  21774  aspval  21862  asclfval  21868  ressascl  21886  psrval  21905  psrass1lem  21922  psrmulval  21933  mvrfval  21969  opsrval  22034  mpfrcl  22073  evlsval  22074  selvffval  22109  mhpmulcl  22125  psdffval  22133  coe1mul2  22244  cply1mul  22271  evls1fval  22294  evl1fval  22303  evl1maprhm  22354  mamufval  22367  mvmulfval  22517  marepvfval  22540  submafval  22554  mdetfval  22561  madufval  22612  minmar1fval  22621  mat2pmatfval  22698  cpm2mfval  22724  decpmatmullem  22746  decpmatmulsumfsupp  22748  pm2mpval  22770  pm2mpmhmlem1  22793  pm2mpmhmlem2  22794  chpmatfval  22805  ntrfval  22999  clsfval  23000  neifval  23074  lpfval  23113  ordtval  23164  ordtbas2  23166  ordtcnv  23176  ordtrest  23177  ordtrest2  23179  cnpfval  23209  kqval  23701  fmval  23918  fmf  23920  flffval  23964  fcfval  24008  cnextval  24036  tsmsval2  24105  nmfval  24563  nmpropd  24569  nmpropd2  24570  subgnm  24608  tngnm  24626  nmofval  24689  pi1xfrcnv  25034  iscph  25147  tcphval  25195  limcfval  25849  dvfval  25874  eldv  25875  mdegfval  26037  mdegmullem  26053  mdegpropd  26059  coe1mul3  26074  ig1pval  26151  taylfval  26335  ishlg  28684  mirval  28737  ishpg  28841  lmif  28867  islmib  28869  vtxdgfval  29551  vtxdeqd  29561  grpoinvfval  30608  nmoofval  30848  eigvalfval  31983  ressnm  33039  tocycval  33184  idlsrgval  33578  extvval  33690  extvfval  33691  mplvrpmrhm  33706  issply  33720  minplyval  33865  ordtprsval  34078  ordtprsuni  34079  ordtrestNEW  34081  ofcfval  34258  ofcfval3  34262  omsval  34453  sitgval  34492  issibf  34493  sitgfval  34501  signstfv  34723  cvmliftlem5  35487  cvmliftlem15  35496  mvrsval  35703  mrsubffval  35705  elmrsubrn  35718  msubffval  35721  mvhfval  35731  msrfval  35735  fwddifval  36360  fwddifnval  36361  tailfval  36570  bj-imdirvallem  37510  bj-endval  37645  cureq  37931  lsatset  39450  lkrfval  39547  pmapfval  40216  pclfvalN  40349  polfvalN  40364  watfvalN  40452  ldilfset  40568  ltrnfset  40577  dilfsetN  40612  trnfsetN  40615  trlfset  40620  trlset  40621  tgrpfset  41204  tendofset  41218  erngfset  41259  erngset  41260  erngfset-rN  41267  erngset-rN  41268  dvafset  41464  diaffval  41490  diafval  41491  dvhfset  41540  docaffvalN  41581  docafvalN  41582  djaffvalN  41593  dibffval  41600  dibfval  41601  dicffval  41634  dicfval  41635  dihffval  41690  dochffval  41809  dochfval  41810  djhffval  41856  lcdfval  42048  mapdffval  42086  mapdfval  42087  hvmapffval  42218  hvmapfval  42219  hdmap1ffval  42255  hdmap1fval  42256  hdmapffval  42286  hdmapfval  42287  hgmapffval  42345  hgmapfval  42346  hlhilset  42394  prjcrvfval  43078  hbtlem1  43569  hbtlem7  43571  cytpval  43648  rfovd  44446  fsovd  44453  fsovcnvlem  44458  dssmapfvd  44462  ntrneibex  44518  mnringvald  44658  ovnval  46987  hspmbllem2  47073  smflimsuplem1  47266  smflimsuplem3  47268  smflimsuplem7  47272  smflimsup  47274  ply1mulgsumlem3  48876  ply1mulgsumlem4  48877  ply1mulgsum  48878  lincval  48897  iinfprg  49546  fucofvalg  49805  precofval3  49858  prcofvalg  49863  lmdfval  50136  cmdfval  50137