Theorem mpteq12dv 5239

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 2137, ax-12 2171. (Revised by SN 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		mpteq12dv.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
2		mpteq12dv.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐷)
3	2	adantr 481	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷)
4	1, 3	mpteq12dva 5237	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106   ↦ cmpt 5231

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-opab 5211  df-mpt 5232

This theorem is referenced by:  mpteq1  5241  mpteq1i  5244  mpteq12i  5254  ovmpt3rab1  7663  offval  7678  offval3  7968  cantnffval  9657  cnfcomlem  9693  fseqenlem1  10018  dfac12lem1  10137  dfac12r  10140  ackbij2lem2  10234  ackbij2lem3  10235  r1om  10238  ccatfval  14522  swrdval  14592  revval  14709  odzval  16723  vdwpc  16912  restval  17371  prdsval  17400  imasval  17456  qusval  17487  mrcfval  17551  cidfval  17619  monfval  17678  ismon  17679  isepi  17686  idfuval  17825  resfval  17841  resfval2  17842  fucval  17909  homafval  17978  idafval  18006  prfval  18150  prf2fval  18152  curfval  18175  curfpropd  18185  hofval  18204  hof2fval  18207  yonedalem3a  18226  yonedalem4a  18227  yonedalem4c  18229  yonedainv  18233  lubfval  18302  glbfval  18315  ipoval  18482  grpinvfval  18862  grpinvfvalALT  18863  grpinvpropd  18897  mulgnn0gsum  18959  cntzfval  19183  pmtrfval  19317  psgnfval  19367  odfval  19399  odfvalALT  19400  sylow1lem2  19466  sylow1lem4  19468  sylow2blem1  19487  sylow3lem1  19494  sylow3lem2  19495  sylow3lem3  19496  sylow3lem6  19499  pj1fval  19561  vrgpfval  19633  gsum2dlem2  19838  gsum2d2  19841  dprdval  19872  dprd2dlem2  19909  dprd2dlem1  19910  dprd2da  19911  dprd2d2  19913  dpjfval  19924  srgbinom  20053  staffval  20454  lspfval  20583  lsppropd  20628  sraval  20788  isphl  21180  ocvfval  21218  pjfval  21260  uvcfval  21338  aspval  21426  asclfval  21432  ressascl  21449  psrval  21467  psrass1lemOLD  21492  psrass1lem  21495  psrmulval  21504  mvrfval  21539  opsrval  21600  mpfrcl  21647  evlsval  21648  selvffval  21678  mhpmulcl  21691  coe1mul2  21790  cply1mul  21817  evls1fval  21837  evl1fval  21846  mamufval  21886  mvmulfval  22043  marepvfval  22066  submafval  22080  mdetfval  22087  madufval  22138  minmar1fval  22147  mat2pmatfval  22224  cpm2mfval  22250  decpmatmullem  22272  decpmatmulsumfsupp  22274  pm2mpval  22296  pm2mpmhmlem1  22319  pm2mpmhmlem2  22320  chpmatfval  22331  ntrfval  22527  clsfval  22528  neifval  22602  lpfval  22641  ordtval  22692  ordtbas2  22694  ordtcnv  22704  ordtrest  22705  ordtrest2  22707  cnpfval  22737  kqval  23229  fmval  23446  fmf  23448  flffval  23492  fcfval  23536  cnextval  23564  tsmsval2  23633  nmfval  24096  nmpropd  24102  nmpropd2  24103  subgnm  24141  tngnm  24167  nmofval  24230  pi1xfrcnv  24572  iscph  24686  tcphval  24734  limcfval  25388  dvfval  25413  eldv  25414  mdegfval  25579  mdegmullem  25595  mdegpropd  25601  coe1mul3  25616  ig1pval  25689  taylfval  25870  ishlg  27850  mirval  27903  ishpg  28007  lmif  28033  islmib  28035  vtxdgfval  28721  vtxdeqd  28731  grpoinvfval  29770  nmoofval  30010  eigvalfval  31145  ressnm  32123  tocycval  32262  idlsrgval  32612  minplyval  32761  ordtprsval  32893  ordtprsuni  32894  ordtrestNEW  32896  indv  33005  ofcfval  33091  ofcfval3  33095  omsval  33287  sitgval  33326  issibf  33327  sitgfval  33335  signstfv  33569  cvmliftlem5  34275  cvmliftlem15  34284  mvrsval  34491  mrsubffval  34493  elmrsubrn  34506  msubffval  34509  mvhfval  34519  msrfval  34523  fwddifval  35129  fwddifnval  35130  tailfval  35252  bj-imdirvallem  36056  bj-endval  36191  cureq  36459  lsatset  37855  lkrfval  37952  pmapfval  38622  pclfvalN  38755  polfvalN  38770  watfvalN  38858  ldilfset  38974  ltrnfset  38983  dilfsetN  39018  trnfsetN  39021  trlfset  39026  trlset  39027  tgrpfset  39610  tendofset  39624  erngfset  39665  erngset  39666  erngfset-rN  39673  erngset-rN  39674  dvafset  39870  diaffval  39896  diafval  39897  dvhfset  39946  docaffvalN  39987  docafvalN  39988  djaffvalN  39999  dibffval  40006  dibfval  40007  dicffval  40040  dicfval  40041  dihffval  40096  dochffval  40215  dochfval  40216  djhffval  40262  lcdfval  40454  mapdffval  40492  mapdfval  40493  hvmapffval  40624  hvmapfval  40625  hdmap1ffval  40661  hdmap1fval  40662  hdmapffval  40692  hdmapfval  40693  hgmapffval  40751  hgmapfval  40752  hlhilset  40800  prjcrvfval  41374  hbtlem1  41855  hbtlem7  41857  rgspnval  41900  cytpval  41941  rfovd  42742  fsovd  42749  fsovcnvlem  42754  dssmapfvd  42758  ntrneibex  42814  mnringvald  42957  ovnval  45247  hspmbllem2  45333  smflimsuplem1  45526  smflimsuplem3  45528  smflimsuplem7  45532  smflimsup  45534  ply1mulgsumlem3  47059  ply1mulgsumlem4  47060  ply1mulgsum  47061  lincval  47080