Theorem mpteq12dv 5186

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 2174, ax-12 2211. (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 484	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷)
4	1, 3	mpteq12dva 5185	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))

Syntax hints:   → wi 4   = wceq 1559   ∈ wcel 2141   ↦ cmpt 5180

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-opab 5162  df-mpt 5181

This theorem is referenced by:  mpteq1  5188  mpteq1i  5190  mpteq12i  5196  ovmpt3rab1  7650  offval  7665  offval3  7959  cantnffval  9615  cnfcomlem  9651  fseqenlem1  9977  dfac12lem1  10097  dfac12r  10100  ackbij2lem2  10192  ackbij2lem3  10193  r1om  10196  indv  12194  ccatfval  14583  swrdval  14654  revval  14770  odzval  16810  vdwpc  16999  restval  17438  prdsval  17467  imasval  17524  qusval  17555  mrcfval  17623  cidfval  17691  monfval  17748  ismon  17749  isepi  17756  idfuval  17892  resfval  17908  resfval2  17909  fucval  17977  homafval  18045  idafval  18073  prfval  18214  prf2fval  18216  curfval  18238  curfpropd  18248  hofval  18267  hof2fval  18270  yonedalem3a  18289  yonedalem4a  18290  yonedalem4c  18292  yonedainv  18296  lubfval  18363  glbfval  18376  ipoval  18545  grpinvfval  19003  grpinvfvalALT  19004  grpinvpropd  19040  mulgnn0gsum  19105  cntzfval  19343  pmtrfval  19473  psgnfval  19523  odfval  19555  odfvalALT  19556  sylow1lem2  19622  sylow1lem4  19624  sylow2blem1  19643  sylow3lem1  19650  sylow3lem2  19651  sylow3lem3  19652  sylow3lem6  19655  pj1fval  19717  vrgpfval  19789  gsum2dlem2  19994  gsum2d2  19997  dprdval  20028  dprd2dlem2  20065  dprd2dlem1  20066  dprd2da  20067  dprd2d2  20069  dpjfval  20080  srgbinom  20260  rgspnval  20641  staffval  20870  lspfval  21020  lsppropd  21065  sraval  21222  isphl  21660  ocvfval  21698  pjfval  21738  uvcfval  21816  aspval  21904  asclfval  21910  ressascl  21928  psrval  21947  psrass1lem  21965  psrmulval  21976  mvrfval  22012  opsrval  22079  mpfrcl  22118  evlsval  22119  selvffval  22151  mhpmulcl  22194  psdffval  22202  coe1mul2  22312  cply1mul  22339  evls1fval  22362  evl1fval  22371  evl1maprhm  22422  mamufval  22432  mvmulfval  22582  marepvfval  22605  submafval  22619  mdetfval  22626  madufval  22677  minmar1fval  22686  mat2pmatfval  22763  cpm2mfval  22789  decpmatmullem  22811  decpmatmulsumfsupp  22813  pm2mpval  22835  pm2mpmhmlem1  22858  pm2mpmhmlem2  22859  chpmatfval  22870  ntrfval  23064  clsfval  23065  neifval  23139  lpfval  23178  ordtval  23229  ordtbas2  23231  ordtcnv  23241  ordtrest  23242  ordtrest2  23244  cnpfval  23274  kqval  23766  fmval  23983  fmf  23985  flffval  24029  fcfval  24073  cnextval  24101  tsmsval2  24170  nmfval  24628  nmpropd  24634  nmpropd2  24635  subgnm  24673  tngnm  24691  nmofval  24754  pi1xfrcnv  25099  iscph  25212  tcphval  25260  limcfval  25914  dvfval  25939  eldv  25940  mdegfval  26102  mdegmullem  26118  mdegpropd  26124  coe1mul3  26139  ig1pval  26216  taylfval  26399  ishlg  28748  mirval  28801  ishpg  28905  lmif  28931  islmib  28933  vtxdgfval  29614  vtxdeqd  29624  grpoinvfval  30671  nmoofval  30911  eigvalfval  32046  ressnm  33103  tocycval  33249  idlsrgval  33660  selvply1rhmlemb  33777  extvval  33789  extvfval  33790  mplvrpmrhm  33805  issply  33819  minplyval  33963  ordtprsval  34176  ordtprsuni  34177  ordtrestNEW  34179  ofcfval  34356  ofcfval3  34360  omsval  34551  sitgval  34590  issibf  34591  sitgfval  34599  signstfv  34821  cvmliftlem5  35603  cvmliftlem15  35612  mvrsval  35819  mrsubffval  35821  elmrsubrn  35834  msubffval  35837  mvhfval  35847  msrfval  35851  fwddifval  36476  fwddifnval  36477  tailfval  36696  bj-imdirvallem  37636  bj-endval  37771  cureq  38059  lsatset  39578  lkrfval  39675  pmapfval  40344  pclfvalN  40477  polfvalN  40492  watfvalN  40580  ldilfset  40696  ltrnfset  40705  dilfsetN  40740  trnfsetN  40743  trlfset  40748  trlset  40749  tgrpfset  41332  tendofset  41346  erngfset  41387  erngset  41388  erngfset-rN  41395  erngset-rN  41396  dvafset  41592  diaffval  41618  diafval  41619  dvhfset  41668  docaffvalN  41709  docafvalN  41710  djaffvalN  41721  dibffval  41728  dibfval  41729  dicffval  41762  dicfval  41763  dihffval  41818  dochffval  41937  dochfval  41938  djhffval  41984  lcdfval  42176  mapdffval  42214  mapdfval  42215  hvmapffval  42346  hvmapfval  42347  hdmap1ffval  42383  hdmap1fval  42384  hdmapffval  42414  hdmapfval  42415  hgmapffval  42473  hgmapfval  42474  hlhilset  42522  prjcrvfval  43177  hbtlem1  43664  hbtlem7  43666  cytpval  43743  rfovd  44541  fsovd  44548  fsovcnvlem  44553  dssmapfvd  44557  ntrneibex  44613  mnringvald  44753  ovnval  47079  hspmbllem2  47165  smflimsuplem1  47358  smflimsuplem3  47360  smflimsuplem7  47364  smflimsup  47366  ply1mulgsumlem3  48974  ply1mulgsumlem4  48975  ply1mulgsum  48976  lincval  48995  iinfprg  49644  fucofvalg  49903  precofval3  49956  prcofvalg  49961  lmdfval  50234  cmdfval  50235