Theorem mpteq12dv 5196

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 2180, ax-12 2216. (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 486	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷)
4	1, 3	mpteq12dva 5195	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147   ↦ cmpt 5190

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-opab 5172  df-mpt 5191

This theorem is used by:  mpteq1  5198  mpteq1i  5200  mpteq12i  5206  ovmpt3rab1  7706  offval  7729  offval3  8021  cureq  8920  cantnffval  9694  cnfcomlem  9730  fseqenlem1  10133  dfac12lem1  10252  dfac12r  10255  ackbij2lem2  10347  ackbij2lem3  10348  hfom  10351  indv  12352  ccatfval  14748  swrdval  14822  revval  14940  odzval  17001  vdwpc  17190  restval  17629  prdsval  17658  imasval  17715  qusval  17746  mrcfval  17814  cidfval  17882  monfval  17939  ismon  17940  isepi  17947  idfuval  18083  resfval  18099  resfval2  18100  fucval  18168  homafval  18236  idafval  18264  prfval  18405  prf2fval  18407  curfval  18429  curfpropd  18439  hofval  18458  hof2fval  18461  yonedalem3a  18480  yonedalem4a  18481  yonedalem4c  18483  yonedainv  18487  lubfval  18554  glbfval  18567  ipoval  18736  grpinvfval  19221  grpinvfvalALT  19222  grpinvpropd  19257  mulgnn0gsum  19322  cntzfval  19567  pmtrfval  19697  psgnfval  19747  odfval  19779  odfvalALT  19780  sylow1lem2  19846  sylow1lem4  19848  sylow2blem1  19867  sylow3lem1  19874  sylow3lem2  19875  sylow3lem3  19876  sylow3lem6  19879  pj1fval  19941  vrgpfval  20013  gsum2dlem2  20218  gsum2d2  20221  dprdval  20252  dprd2dlem2  20289  dprd2dlem1  20290  dprd2da  20291  dprd2d2  20293  dpjfval  20304  srgbinom  20490  rgspnval  20897  staffval  21131  lspfval  21281  lsppropd  21326  sraval  21483  isphl  21967  ocvfval  22005  pjfval  22045  uvcfval  22123  aspval  22213  asclfval  22219  ressascl  22237  psrval  22256  psrass1lem  22274  psrmulval  22285  mvrfval  22321  opsrval  22388  mpfrcl  22427  evlsval  22428  selvffval  22460  mhpmulcl  22503  psdffval  22511  coe1mul2  22621  cply1mul  22647  evls1fval  22670  evl1fval  22679  evl1maprhm  22730  mamufval  22740  mvmulfval  22890  marepvfval  22913  submafval  22927  mdetfval  22934  madufval  22985  minmar1fval  22994  mat2pmatfval  23074  cpm2mfval  23100  decpmatmullem  23122  decpmatmulsumfsupp  23124  pm2mpval  23146  pm2mpmhmlem1  23169  pm2mpmhmlem2  23170  chpmatfval  23181  ntrfval  23375  clsfval  23376  neifval  23450  lpfval  23489  ordtval  23540  ordtbas2  23542  ordtcnv  23552  ordtrest  23553  ordtrest2  23555  cnpfval  23585  kqval  24078  fmval  24295  fmf  24297  flffval  24341  fcfval  24385  cnextval  24413  tsmsval2  24482  nmfval  24940  nmpropd  24946  nmpropd2  24947  subgnm  24985  tngnm  25003  nmofval  25066  pi1xfrcnv  25411  iscph  25524  tcphval  25572  limcfval  26225  dvfval  26250  eldv  26251  mdegfval  26413  mdegmullem  26429  mdegpropd  26435  coe1mul3  26450  ig1pval  26527  taylfval  26719  ishlg2  29098  ishlg  29101  mirval  29160  ishpg  29270  lmif  29323  islmib  29325  vtxdgfval  30081  vtxdeqd  30091  grpoinvfval  31157  nmoofval  31397  eigvalfval  32532  ressnm  33598  tocycval  33745  idlsrgval  34119  selvply1rhmlemb  34234  extvval  34246  extvfval  34247  mplvrpmrhm  34262  issply  34276  minplyval  34420  ordtprsval  34633  ordtprsuni  34634  ordtrestNEW  34636  ofcfval  34813  ofcfval3  34817  omsval  35008  sitgval  35047  issibf  35048  sitgfval  35056  signstfv  35275  cvmliftlem5  36234  cvmliftlem15  36243  mvrsval  36450  mrsubffval  36452  elmrsubrn  36465  msubffval  36468  mvhfval  36478  msrfval  36482  fwddifval  37118  fwddifnval  37119  tailfval  37351  bj-imdirvallem  38306  bj-endval  38441  lsatset  40250  lkrfval  40347  pmapfval  41016  pclfvalN  41149  polfvalN  41164  watfvalN  41252  ldilfset  41368  ltrnfset  41377  dilfsetN  41412  trnfsetN  41415  trlfset  41420  trlset  41421  tgrpfset  42004  tendofset  42018  erngfset  42059  erngset  42060  erngfset-rN  42067  erngset-rN  42068  dvafset  42264  diaffval  42290  diafval  42291  dvhfset  42340  docaffvalN  42381  docafvalN  42382  djaffvalN  42393  dibffval  42400  dibfval  42401  dicffval  42434  dicfval  42435  dihffval  42490  dochffval  42609  dochfval  42610  djhffval  42656  lcdfval  42848  mapdffval  42886  mapdfval  42887  hvmapffval  43018  hvmapfval  43019  hdmap1ffval  43055  hdmap1fval  43056  hdmapffval  43086  hdmapfval  43087  hgmapffval  43145  hgmapfval  43146  hlhilset  43194  prjcrvfval  43871  hbtlem1  44328  hbtlem7  44330  cytpval  44407  rfovd  45204  fsovd  45211  fsovcnvlem  45216  dssmapfvd  45220  ntrneibex  45276  mnringvald  45414  ackbij3  46231  ovnval  47766  hspmbllem2  47852  smflimsuplem1  48045  smflimsuplem3  48047  smflimsuplem7  48051  smflimsup  48053  ply1mulgsumlem3  49715  ply1mulgsumlem4  49716  ply1mulgsum  49717  lincval  49736  iinfprg  50388  fucofvalg  50655  postcof2  50715  precofval3  50721  prcofvalg  50726  lmdfval  51047  cmdfval  51048