Theorem mpteq12dv 5207

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108   ↦ cmpt 5201

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-opab 5182  df-mpt 5202

This theorem is referenced by:  mpteq1  5209  mpteq1i  5211  mpteq12i  5218  ovmpt3rab1  7665  offval  7680  offval3  7981  cantnffval  9677  cnfcomlem  9713  fseqenlem1  10038  dfac12lem1  10158  dfac12r  10161  ackbij2lem2  10253  ackbij2lem3  10254  r1om  10257  ccatfval  14591  swrdval  14661  revval  14778  odzval  16811  vdwpc  17000  restval  17440  prdsval  17469  imasval  17525  qusval  17556  mrcfval  17620  cidfval  17688  monfval  17745  ismon  17746  isepi  17753  idfuval  17889  resfval  17905  resfval2  17906  fucval  17974  homafval  18042  idafval  18070  prfval  18211  prf2fval  18213  curfval  18235  curfpropd  18245  hofval  18264  hof2fval  18267  yonedalem3a  18286  yonedalem4a  18287  yonedalem4c  18289  yonedainv  18293  lubfval  18360  glbfval  18373  ipoval  18540  grpinvfval  18961  grpinvfvalALT  18962  grpinvpropd  18998  mulgnn0gsum  19063  cntzfval  19303  pmtrfval  19431  psgnfval  19481  odfval  19513  odfvalALT  19514  sylow1lem2  19580  sylow1lem4  19582  sylow2blem1  19601  sylow3lem1  19608  sylow3lem2  19609  sylow3lem3  19610  sylow3lem6  19613  pj1fval  19675  vrgpfval  19747  gsum2dlem2  19952  gsum2d2  19955  dprdval  19986  dprd2dlem2  20023  dprd2dlem1  20024  dprd2da  20025  dprd2d2  20027  dpjfval  20038  srgbinom  20191  rgspnval  20572  staffval  20801  lspfval  20930  lsppropd  20976  sraval  21133  isphl  21588  ocvfval  21626  pjfval  21666  uvcfval  21744  aspval  21833  asclfval  21839  ressascl  21856  psrval  21875  psrass1lem  21892  psrmulval  21904  mvrfval  21941  opsrval  22004  mpfrcl  22043  evlsval  22044  selvffval  22071  mhpmulcl  22087  psdffval  22095  coe1mul2  22206  cply1mul  22234  evls1fval  22257  evl1fval  22266  evl1maprhm  22317  mamufval  22330  mvmulfval  22480  marepvfval  22503  submafval  22517  mdetfval  22524  madufval  22575  minmar1fval  22584  mat2pmatfval  22661  cpm2mfval  22687  decpmatmullem  22709  decpmatmulsumfsupp  22711  pm2mpval  22733  pm2mpmhmlem1  22756  pm2mpmhmlem2  22757  chpmatfval  22768  ntrfval  22962  clsfval  22963  neifval  23037  lpfval  23076  ordtval  23127  ordtbas2  23129  ordtcnv  23139  ordtrest  23140  ordtrest2  23142  cnpfval  23172  kqval  23664  fmval  23881  fmf  23883  flffval  23927  fcfval  23971  cnextval  23999  tsmsval2  24068  nmfval  24527  nmpropd  24533  nmpropd2  24534  subgnm  24572  tngnm  24590  nmofval  24653  pi1xfrcnv  25008  iscph  25122  tcphval  25170  limcfval  25825  dvfval  25850  eldv  25851  mdegfval  26019  mdegmullem  26035  mdegpropd  26041  coe1mul3  26056  ig1pval  26133  taylfval  26318  ishlg  28581  mirval  28634  ishpg  28738  lmif  28764  islmib  28766  vtxdgfval  29447  vtxdeqd  29457  grpoinvfval  30503  nmoofval  30743  eigvalfval  31878  indv  32829  ressnm  32940  tocycval  33119  idlsrgval  33518  minplyval  33739  ordtprsval  33949  ordtprsuni  33950  ordtrestNEW  33952  ofcfval  34129  ofcfval3  34133  omsval  34325  sitgval  34364  issibf  34365  sitgfval  34373  signstfv  34595  cvmliftlem5  35311  cvmliftlem15  35320  mvrsval  35527  mrsubffval  35529  elmrsubrn  35542  msubffval  35545  mvhfval  35555  msrfval  35559  fwddifval  36180  fwddifnval  36181  tailfval  36390  bj-imdirvallem  37198  bj-endval  37333  cureq  37620  lsatset  39008  lkrfval  39105  pmapfval  39775  pclfvalN  39908  polfvalN  39923  watfvalN  40011  ldilfset  40127  ltrnfset  40136  dilfsetN  40171  trnfsetN  40174  trlfset  40179  trlset  40180  tgrpfset  40763  tendofset  40777  erngfset  40818  erngset  40819  erngfset-rN  40826  erngset-rN  40827  dvafset  41023  diaffval  41049  diafval  41050  dvhfset  41099  docaffvalN  41140  docafvalN  41141  djaffvalN  41152  dibffval  41159  dibfval  41160  dicffval  41193  dicfval  41194  dihffval  41249  dochffval  41368  dochfval  41369  djhffval  41415  lcdfval  41607  mapdffval  41645  mapdfval  41646  hvmapffval  41777  hvmapfval  41778  hdmap1ffval  41814  hdmap1fval  41815  hdmapffval  41845  hdmapfval  41846  hgmapffval  41904  hgmapfval  41905  hlhilset  41953  prjcrvfval  42654  hbtlem1  43147  hbtlem7  43149  cytpval  43226  rfovd  44025  fsovd  44032  fsovcnvlem  44037  dssmapfvd  44041  ntrneibex  44097  mnringvald  44237  ovnval  46570  hspmbllem2  46656  smflimsuplem1  46849  smflimsuplem3  46851  smflimsuplem7  46855  smflimsup  46857  ply1mulgsumlem3  48364  ply1mulgsumlem4  48365  ply1mulgsum  48366  lincval  48385  iinfprg  49026  fucofvalg  49229  precofval3  49282  prcofvalg  49287  lmdfval  49523  cmdfval  49524