Theorem mpteq12dv 5233

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-opab 5206  df-mpt 5226

This theorem is referenced by:  mpteq1  5235  mpteq1i  5238  mpteq12i  5248  ovmpt3rab1  7691  offval  7706  offval3  8007  cantnffval  9703  cnfcomlem  9739  fseqenlem1  10064  dfac12lem1  10184  dfac12r  10187  ackbij2lem2  10279  ackbij2lem3  10280  r1om  10283  ccatfval  14611  swrdval  14681  revval  14798  odzval  16829  vdwpc  17018  restval  17471  prdsval  17500  imasval  17556  qusval  17587  mrcfval  17651  cidfval  17719  monfval  17776  ismon  17777  isepi  17784  idfuval  17921  resfval  17937  resfval2  17938  fucval  18006  homafval  18074  idafval  18102  prfval  18244  prf2fval  18246  curfval  18268  curfpropd  18278  hofval  18297  hof2fval  18300  yonedalem3a  18319  yonedalem4a  18320  yonedalem4c  18322  yonedainv  18326  lubfval  18395  glbfval  18408  ipoval  18575  grpinvfval  18996  grpinvfvalALT  18997  grpinvpropd  19033  mulgnn0gsum  19098  cntzfval  19338  pmtrfval  19468  psgnfval  19518  odfval  19550  odfvalALT  19551  sylow1lem2  19617  sylow1lem4  19619  sylow2blem1  19638  sylow3lem1  19645  sylow3lem2  19646  sylow3lem3  19647  sylow3lem6  19650  pj1fval  19712  vrgpfval  19784  gsum2dlem2  19989  gsum2d2  19992  dprdval  20023  dprd2dlem2  20060  dprd2dlem1  20061  dprd2da  20062  dprd2d2  20064  dpjfval  20075  srgbinom  20228  rgspnval  20612  staffval  20842  lspfval  20971  lsppropd  21017  sraval  21174  isphl  21646  ocvfval  21684  pjfval  21726  uvcfval  21804  aspval  21893  asclfval  21899  ressascl  21916  psrval  21935  psrass1lem  21952  psrmulval  21964  mvrfval  22001  opsrval  22064  mpfrcl  22109  evlsval  22110  selvffval  22137  mhpmulcl  22153  psdffval  22161  coe1mul2  22272  cply1mul  22300  evls1fval  22323  evl1fval  22332  evl1maprhm  22383  mamufval  22396  mvmulfval  22548  marepvfval  22571  submafval  22585  mdetfval  22592  madufval  22643  minmar1fval  22652  mat2pmatfval  22729  cpm2mfval  22755  decpmatmullem  22777  decpmatmulsumfsupp  22779  pm2mpval  22801  pm2mpmhmlem1  22824  pm2mpmhmlem2  22825  chpmatfval  22836  ntrfval  23032  clsfval  23033  neifval  23107  lpfval  23146  ordtval  23197  ordtbas2  23199  ordtcnv  23209  ordtrest  23210  ordtrest2  23212  cnpfval  23242  kqval  23734  fmval  23951  fmf  23953  flffval  23997  fcfval  24041  cnextval  24069  tsmsval2  24138  nmfval  24601  nmpropd  24607  nmpropd2  24608  subgnm  24646  tngnm  24672  nmofval  24735  pi1xfrcnv  25090  iscph  25204  tcphval  25252  limcfval  25907  dvfval  25932  eldv  25933  mdegfval  26101  mdegmullem  26117  mdegpropd  26123  coe1mul3  26138  ig1pval  26215  taylfval  26400  ishlg  28610  mirval  28663  ishpg  28767  lmif  28793  islmib  28795  vtxdgfval  29485  vtxdeqd  29495  grpoinvfval  30541  nmoofval  30781  eigvalfval  31916  indv  32837  ressnm  32949  tocycval  33128  idlsrgval  33531  minplyval  33748  ordtprsval  33917  ordtprsuni  33918  ordtrestNEW  33920  ofcfval  34099  ofcfval3  34103  omsval  34295  sitgval  34334  issibf  34335  sitgfval  34343  signstfv  34578  cvmliftlem5  35294  cvmliftlem15  35303  mvrsval  35510  mrsubffval  35512  elmrsubrn  35525  msubffval  35528  mvhfval  35538  msrfval  35542  fwddifval  36163  fwddifnval  36164  tailfval  36373  bj-imdirvallem  37181  bj-endval  37316  cureq  37603  lsatset  38991  lkrfval  39088  pmapfval  39758  pclfvalN  39891  polfvalN  39906  watfvalN  39994  ldilfset  40110  ltrnfset  40119  dilfsetN  40154  trnfsetN  40157  trlfset  40162  trlset  40163  tgrpfset  40746  tendofset  40760  erngfset  40801  erngset  40802  erngfset-rN  40809  erngset-rN  40810  dvafset  41006  diaffval  41032  diafval  41033  dvhfset  41082  docaffvalN  41123  docafvalN  41124  djaffvalN  41135  dibffval  41142  dibfval  41143  dicffval  41176  dicfval  41177  dihffval  41232  dochffval  41351  dochfval  41352  djhffval  41398  lcdfval  41590  mapdffval  41628  mapdfval  41629  hvmapffval  41760  hvmapfval  41761  hdmap1ffval  41797  hdmap1fval  41798  hdmapffval  41828  hdmapfval  41829  hgmapffval  41887  hgmapfval  41888  hlhilset  41936  prjcrvfval  42641  hbtlem1  43135  hbtlem7  43137  cytpval  43214  rfovd  44014  fsovd  44021  fsovcnvlem  44026  dssmapfvd  44030  ntrneibex  44086  mnringvald  44227  ovnval  46556  hspmbllem2  46642  smflimsuplem1  46835  smflimsuplem3  46837  smflimsuplem7  46841  smflimsup  46843  ply1mulgsumlem3  48305  ply1mulgsumlem4  48306  ply1mulgsum  48307  lincval  48326  fucofvalg  49013  precoffunc  49066