Theorem mpteq12dv 5197

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   ↦ cmpt 5191

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-opab 5173  df-mpt 5192

This theorem is referenced by:  mpteq1  5199  mpteq1i  5201  mpteq12i  5207  ovmpt3rab1  7650  offval  7665  offval3  7964  cantnffval  9623  cnfcomlem  9659  fseqenlem1  9984  dfac12lem1  10104  dfac12r  10107  ackbij2lem2  10199  ackbij2lem3  10200  r1om  10203  ccatfval  14545  swrdval  14615  revval  14732  odzval  16769  vdwpc  16958  restval  17396  prdsval  17425  imasval  17481  qusval  17512  mrcfval  17576  cidfval  17644  monfval  17701  ismon  17702  isepi  17709  idfuval  17845  resfval  17861  resfval2  17862  fucval  17930  homafval  17998  idafval  18026  prfval  18167  prf2fval  18169  curfval  18191  curfpropd  18201  hofval  18220  hof2fval  18223  yonedalem3a  18242  yonedalem4a  18243  yonedalem4c  18245  yonedainv  18249  lubfval  18316  glbfval  18329  ipoval  18496  grpinvfval  18917  grpinvfvalALT  18918  grpinvpropd  18954  mulgnn0gsum  19019  cntzfval  19259  pmtrfval  19387  psgnfval  19437  odfval  19469  odfvalALT  19470  sylow1lem2  19536  sylow1lem4  19538  sylow2blem1  19557  sylow3lem1  19564  sylow3lem2  19565  sylow3lem3  19566  sylow3lem6  19569  pj1fval  19631  vrgpfval  19703  gsum2dlem2  19908  gsum2d2  19911  dprdval  19942  dprd2dlem2  19979  dprd2dlem1  19980  dprd2da  19981  dprd2d2  19983  dpjfval  19994  srgbinom  20147  rgspnval  20528  staffval  20757  lspfval  20886  lsppropd  20932  sraval  21089  isphl  21544  ocvfval  21582  pjfval  21622  uvcfval  21700  aspval  21789  asclfval  21795  ressascl  21812  psrval  21831  psrass1lem  21848  psrmulval  21860  mvrfval  21897  opsrval  21960  mpfrcl  21999  evlsval  22000  selvffval  22027  mhpmulcl  22043  psdffval  22051  coe1mul2  22162  cply1mul  22190  evls1fval  22213  evl1fval  22222  evl1maprhm  22273  mamufval  22286  mvmulfval  22436  marepvfval  22459  submafval  22473  mdetfval  22480  madufval  22531  minmar1fval  22540  mat2pmatfval  22617  cpm2mfval  22643  decpmatmullem  22665  decpmatmulsumfsupp  22667  pm2mpval  22689  pm2mpmhmlem1  22712  pm2mpmhmlem2  22713  chpmatfval  22724  ntrfval  22918  clsfval  22919  neifval  22993  lpfval  23032  ordtval  23083  ordtbas2  23085  ordtcnv  23095  ordtrest  23096  ordtrest2  23098  cnpfval  23128  kqval  23620  fmval  23837  fmf  23839  flffval  23883  fcfval  23927  cnextval  23955  tsmsval2  24024  nmfval  24483  nmpropd  24489  nmpropd2  24490  subgnm  24528  tngnm  24546  nmofval  24609  pi1xfrcnv  24964  iscph  25077  tcphval  25125  limcfval  25780  dvfval  25805  eldv  25806  mdegfval  25974  mdegmullem  25990  mdegpropd  25996  coe1mul3  26011  ig1pval  26088  taylfval  26273  ishlg  28536  mirval  28589  ishpg  28693  lmif  28719  islmib  28721  vtxdgfval  29402  vtxdeqd  29412  grpoinvfval  30458  nmoofval  30698  eigvalfval  31833  indv  32782  ressnm  32893  tocycval  33072  idlsrgval  33481  minplyval  33702  ordtprsval  33915  ordtprsuni  33916  ordtrestNEW  33918  ofcfval  34095  ofcfval3  34099  omsval  34291  sitgval  34330  issibf  34331  sitgfval  34339  signstfv  34561  cvmliftlem5  35283  cvmliftlem15  35292  mvrsval  35499  mrsubffval  35501  elmrsubrn  35514  msubffval  35517  mvhfval  35527  msrfval  35531  fwddifval  36157  fwddifnval  36158  tailfval  36367  bj-imdirvallem  37175  bj-endval  37310  cureq  37597  lsatset  38990  lkrfval  39087  pmapfval  39757  pclfvalN  39890  polfvalN  39905  watfvalN  39993  ldilfset  40109  ltrnfset  40118  dilfsetN  40153  trnfsetN  40156  trlfset  40161  trlset  40162  tgrpfset  40745  tendofset  40759  erngfset  40800  erngset  40801  erngfset-rN  40808  erngset-rN  40809  dvafset  41005  diaffval  41031  diafval  41032  dvhfset  41081  docaffvalN  41122  docafvalN  41123  djaffvalN  41134  dibffval  41141  dibfval  41142  dicffval  41175  dicfval  41176  dihffval  41231  dochffval  41350  dochfval  41351  djhffval  41397  lcdfval  41589  mapdffval  41627  mapdfval  41628  hvmapffval  41759  hvmapfval  41760  hdmap1ffval  41796  hdmap1fval  41797  hdmapffval  41827  hdmapfval  41828  hgmapffval  41886  hgmapfval  41887  hlhilset  41935  prjcrvfval  42626  hbtlem1  43119  hbtlem7  43121  cytpval  43198  rfovd  43997  fsovd  44004  fsovcnvlem  44009  dssmapfvd  44013  ntrneibex  44069  mnringvald  44209  ovnval  46546  hspmbllem2  46632  smflimsuplem1  46825  smflimsuplem3  46827  smflimsuplem7  46831  smflimsup  46833  ply1mulgsumlem3  48381  ply1mulgsumlem4  48382  ply1mulgsum  48383  lincval  48402  iinfprg  49052  fucofvalg  49311  precofval3  49364  prcofvalg  49369  lmdfval  49642  cmdfval  49643