Theorem mpteq12dv 5192

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 2178, ax-12 2215. (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 485	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷)
4	1, 3	mpteq12dva 5191	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))

Syntax hints:   → wi 4   = wceq 1563   ∈ wcel 2145   ↦ cmpt 5186

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-opab 5168  df-mpt 5187

This theorem is referenced by:  mpteq1  5194  mpteq1i  5196  mpteq12i  5202  ovmpt3rab1  7658  offval  7673  offval3  7967  cantnffval  9620  cnfcomlem  9656  fseqenlem1  9996  dfac12lem1  10115  dfac12r  10118  ackbij2lem2  10210  ackbij2lem3  10211  r1om  10214  indv  12211  ccatfval  14600  swrdval  14671  revval  14787  odzval  16841  vdwpc  17030  restval  17469  prdsval  17498  imasval  17555  qusval  17586  mrcfval  17654  cidfval  17722  monfval  17779  ismon  17780  isepi  17787  idfuval  17923  resfval  17939  resfval2  17940  fucval  18008  homafval  18076  idafval  18104  prfval  18245  prf2fval  18247  curfval  18269  curfpropd  18279  hofval  18298  hof2fval  18301  yonedalem3a  18320  yonedalem4a  18321  yonedalem4c  18323  yonedainv  18327  lubfval  18394  glbfval  18407  ipoval  18576  grpinvfval  19035  grpinvfvalALT  19036  grpinvpropd  19072  mulgnn0gsum  19137  cntzfval  19381  pmtrfval  19511  psgnfval  19561  odfval  19593  odfvalALT  19594  sylow1lem2  19660  sylow1lem4  19662  sylow2blem1  19681  sylow3lem1  19688  sylow3lem2  19689  sylow3lem3  19690  sylow3lem6  19693  pj1fval  19755  vrgpfval  19827  gsum2dlem2  20032  gsum2d2  20035  dprdval  20066  dprd2dlem2  20103  dprd2dlem1  20104  dprd2da  20105  dprd2d2  20107  dpjfval  20118  srgbinom  20304  rgspnval  20688  staffval  20913  lspfval  21063  lsppropd  21108  sraval  21265  isphl  21738  ocvfval  21776  pjfval  21816  uvcfval  21894  aspval  21982  asclfval  21988  ressascl  22006  psrval  22025  psrass1lem  22043  psrmulval  22054  mvrfval  22090  opsrval  22157  mpfrcl  22196  evlsval  22197  selvffval  22229  mhpmulcl  22272  psdffval  22280  coe1mul2  22390  cply1mul  22417  evls1fval  22440  evl1fval  22449  evl1maprhm  22500  mamufval  22510  mvmulfval  22660  marepvfval  22683  submafval  22697  mdetfval  22704  madufval  22755  minmar1fval  22764  mat2pmatfval  22841  cpm2mfval  22867  decpmatmullem  22889  decpmatmulsumfsupp  22891  pm2mpval  22913  pm2mpmhmlem1  22936  pm2mpmhmlem2  22937  chpmatfval  22948  ntrfval  23142  clsfval  23143  neifval  23217  lpfval  23256  ordtval  23307  ordtbas2  23309  ordtcnv  23319  ordtrest  23320  ordtrest2  23322  cnpfval  23352  kqval  23844  fmval  24061  fmf  24063  flffval  24107  fcfval  24151  cnextval  24179  tsmsval2  24248  nmfval  24706  nmpropd  24712  nmpropd2  24713  subgnm  24751  tngnm  24769  nmofval  24832  pi1xfrcnv  25177  iscph  25290  tcphval  25338  limcfval  25992  dvfval  26017  eldv  26018  mdegfval  26180  mdegmullem  26196  mdegpropd  26202  coe1mul3  26217  ig1pval  26294  taylfval  26480  ishlg  28829  mirval  28886  ishpg  28990  lmif  29037  islmib  29039  vtxdgfval  29726  vtxdeqd  29736  grpoinvfval  30783  nmoofval  31023  eigvalfval  32158  ressnm  33197  tocycval  33341  idlsrgval  33710  selvply1rhmlemb  33826  extvval  33838  extvfval  33839  mplvrpmrhm  33854  issply  33868  minplyval  34012  ordtprsval  34225  ordtprsuni  34226  ordtrestNEW  34228  ofcfval  34405  ofcfval3  34409  omsval  34600  sitgval  34639  issibf  34640  sitgfval  34648  signstfv  34867  cvmliftlem5  35652  cvmliftlem15  35661  mvrsval  35868  mrsubffval  35870  elmrsubrn  35883  msubffval  35886  mvhfval  35896  msrfval  35900  fwddifval  36525  fwddifnval  36526  tailfval  36745  bj-imdirvallem  37684  bj-endval  37819  cureq  38107  lsatset  39626  lkrfval  39723  pmapfval  40392  pclfvalN  40525  polfvalN  40540  watfvalN  40628  ldilfset  40744  ltrnfset  40753  dilfsetN  40788  trnfsetN  40791  trlfset  40796  trlset  40797  tgrpfset  41380  tendofset  41394  erngfset  41435  erngset  41436  erngfset-rN  41443  erngset-rN  41444  dvafset  41640  diaffval  41666  diafval  41667  dvhfset  41716  docaffvalN  41757  docafvalN  41758  djaffvalN  41769  dibffval  41776  dibfval  41777  dicffval  41810  dicfval  41811  dihffval  41866  dochffval  41985  dochfval  41986  djhffval  42032  lcdfval  42224  mapdffval  42262  mapdfval  42263  hvmapffval  42394  hvmapfval  42395  hdmap1ffval  42431  hdmap1fval  42432  hdmapffval  42462  hdmapfval  42463  hgmapffval  42521  hgmapfval  42522  hlhilset  42570  prjcrvfval  43225  hbtlem1  43712  hbtlem7  43714  cytpval  43791  rfovd  44589  fsovd  44596  fsovcnvlem  44601  dssmapfvd  44605  ntrneibex  44661  mnringvald  44801  ovnval  47113  hspmbllem2  47199  smflimsuplem1  47392  smflimsuplem3  47394  smflimsuplem7  47398  smflimsup  47400  ply1mulgsumlem3  49019  ply1mulgsumlem4  49020  ply1mulgsum  49021  lincval  49040  iinfprg  49688  fucofvalg  49947  precofval3  50000  prcofvalg  50005  lmdfval  50278  cmdfval  50279