Theorem mpteq12dv 5115

Description: An equality inference for the maps-to notation. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 16-Dec-2013.) Drop ax-10 2142 while shortening its proof. (Revised by Steven Nguyen and Gino Giotto, 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		nfv 1915	. 2 ⊢ Ⅎ𝑥𝜑
2		mpteq12dv.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
3		mpteq12dv.2	. 2 ⊢ (𝜑 → 𝐵 = 𝐷)
4	1, 2, 3	mpteq12df 5112	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))

Syntax hints:   → wi 4   = wceq 1538   ↦ cmpt 5110

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-opab 5093  df-mpt 5111

This theorem is referenced by:  mpteq12i  5123  ovmpt3rab1  7383  offval  7396  offval3  7665  cantnffval  9110  cnfcomlem  9146  fseqenlem1  9435  dfac12lem1  9554  dfac12r  9557  ackbij2lem2  9651  ackbij2lem3  9652  r1om  9655  ccatfval  13916  swrdval  13996  revval  14113  odzval  16118  vdwpc  16306  restval  16692  prdsval  16720  imasval  16776  qusval  16807  mrcfval  16871  cidfval  16939  monfval  16994  ismon  16995  isepi  17002  idfuval  17138  resfval  17154  resfval2  17155  fucval  17220  homafval  17281  idafval  17309  prfval  17441  prf2fval  17443  curfval  17465  curfpropd  17475  hofval  17494  hof2fval  17497  yonedalem3a  17516  yonedalem4a  17517  yonedalem4c  17519  yonedainv  17523  lubfval  17580  glbfval  17593  ipoval  17756  grpinvfval  18134  grpinvfvalALT  18135  grpinvpropd  18166  mulgnn0gsum  18226  cntzfval  18442  pmtrfval  18570  psgnfval  18620  odfval  18652  odfvalALT  18653  sylow1lem2  18716  sylow1lem4  18718  sylow2blem1  18737  sylow3lem1  18744  sylow3lem2  18745  sylow3lem3  18746  sylow3lem6  18749  pj1fval  18812  vrgpfval  18884  gsum2dlem2  19084  gsum2d2  19087  dprdval  19118  dprd2dlem2  19155  dprd2dlem1  19156  dprd2da  19157  dprd2d2  19159  dpjfval  19170  srgbinom  19288  staffval  19611  lspfval  19738  lsppropd  19783  sraval  19941  isphl  20317  ocvfval  20355  pjfval  20395  uvcfval  20473  aspval  20559  asclfval  20565  ressascl  20582  psrval  20600  psrass1lem  20615  psrmulval  20624  mvrfval  20658  opsrval  20714  mpfrcl  20757  evlsval  20758  selvffval  20788  coe1mul2  20898  cply1mul  20923  evls1fval  20943  evl1fval  20952  mamufval  20992  mvmulfval  21147  marepvfval  21170  submafval  21184  mdetfval  21191  madufval  21242  minmar1fval  21251  mat2pmatfval  21328  cpm2mfval  21354  decpmatmullem  21376  decpmatmulsumfsupp  21378  pm2mpval  21400  pm2mpmhmlem1  21423  pm2mpmhmlem2  21424  chpmatfval  21435  ntrfval  21629  clsfval  21630  neifval  21704  lpfval  21743  ordtval  21794  ordtbas2  21796  ordtcnv  21806  ordtrest  21807  ordtrest2  21809  cnpfval  21839  kqval  22331  fmval  22548  fmf  22550  flffval  22594  fcfval  22638  cnextval  22666  tsmsval2  22735  nmfval  23195  nmpropd  23200  nmpropd2  23201  subgnm  23239  tngnm  23257  nmofval  23320  pi1xfrcnv  23662  iscph  23775  tcphval  23822  limcfval  24475  dvfval  24500  eldv  24501  mdegfval  24663  mdegmullem  24679  mdegpropd  24685  coe1mul3  24700  ig1pval  24773  taylfval  24954  ishlg  26396  mirval  26449  ishpg  26553  lmif  26579  islmib  26581  vtxdgfval  27257  vtxdeqd  27267  grpoinvfval  28305  nmoofval  28545  eigvalfval  29680  ressnm  30664  tocycval  30800  idlsrgval  31056  ordtprsval  31271  ordtprsuni  31272  ordtrestNEW  31274  indv  31381  ofcfval  31467  ofcfval3  31471  omsval  31661  sitgval  31700  issibf  31701  sitgfval  31709  signstfv  31943  cvmliftlem5  32649  cvmliftlem15  32658  mvrsval  32865  mrsubffval  32867  elmrsubrn  32880  msubffval  32883  mvhfval  32893  msrfval  32897  fwddifval  33736  fwddifnval  33737  tailfval  33833  bj-imdirvallem  34595  bj-endval  34729  cureq  35033  lsatset  36286  lkrfval  36383  pmapfval  37052  pclfvalN  37185  polfvalN  37200  watfvalN  37288  ldilfset  37404  ltrnfset  37413  dilfsetN  37448  trnfsetN  37451  trlfset  37456  trlset  37457  tgrpfset  38040  tendofset  38054  erngfset  38095  erngset  38096  erngfset-rN  38103  erngset-rN  38104  dvafset  38300  diaffval  38326  diafval  38327  dvhfset  38376  docaffvalN  38417  docafvalN  38418  djaffvalN  38429  dibffval  38436  dibfval  38437  dicffval  38470  dicfval  38471  dihffval  38526  dochffval  38645  dochfval  38646  djhffval  38692  lcdfval  38884  mapdffval  38922  mapdfval  38923  hvmapffval  39054  hvmapfval  39055  hdmap1ffval  39091  hdmap1fval  39092  hdmapffval  39122  hdmapfval  39123  hgmapffval  39181  hgmapfval  39182  hlhilset  39230  hbtlem1  40067  hbtlem7  40069  rgspnval  40112  cytpval  40153  rfovd  40702  fsovd  40709  fsovcnvlem  40714  dssmapfvd  40718  ntrneibex  40776  mnringvald  40921  ovnval  43180  hspmbllem2  43266  smflimsuplem1  43451  smflimsuplem3  43453  smflimsuplem7  43457  smflimsup  43459  ply1mulgsumlem3  44796  ply1mulgsumlem4  44797  ply1mulgsum  44798  lincval  44818