Theorem mpteq12dv 5192

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 2178, ax-12 2213. (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 486	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷)
4	1, 3	mpteq12dva 5191	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145   ↦ cmpt 5186

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-opab 5168  df-mpt 5187

This theorem is used by:  mpteq1  5194  mpteq1i  5196  mpteq12i  5202  ovmpt3rab1  7671  offval  7691  offval3  7983  cureq  8873  cantnffval  9648  cnfcomlem  9684  fseqenlem1  10084  dfac12lem1  10203  dfac12r  10206  ackbij2lem2  10298  ackbij2lem3  10299  hfom  10302  indv  12303  ccatfval  14698  swrdval  14771  revval  14889  odzval  16949  vdwpc  17138  restval  17577  prdsval  17606  imasval  17663  qusval  17694  mrcfval  17762  cidfval  17830  monfval  17887  ismon  17888  isepi  17895  idfuval  18031  resfval  18047  resfval2  18048  fucval  18116  homafval  18184  idafval  18212  prfval  18353  prf2fval  18355  curfval  18377  curfpropd  18387  hofval  18406  hof2fval  18409  yonedalem3a  18428  yonedalem4a  18429  yonedalem4c  18431  yonedainv  18435  lubfval  18502  glbfval  18515  ipoval  18684  grpinvfval  19169  grpinvfvalALT  19170  grpinvpropd  19205  mulgnn0gsum  19270  cntzfval  19514  pmtrfval  19644  psgnfval  19694  odfval  19726  odfvalALT  19727  sylow1lem2  19793  sylow1lem4  19795  sylow2blem1  19814  sylow3lem1  19821  sylow3lem2  19822  sylow3lem3  19823  sylow3lem6  19826  pj1fval  19888  vrgpfval  19960  gsum2dlem2  20165  gsum2d2  20168  dprdval  20199  dprd2dlem2  20236  dprd2dlem1  20237  dprd2da  20238  dprd2d2  20240  dpjfval  20251  srgbinom  20437  rgspnval  20844  staffval  21078  lspfval  21228  lsppropd  21273  sraval  21430  isphl  21914  ocvfval  21952  pjfval  21992  uvcfval  22070  aspval  22160  asclfval  22166  ressascl  22184  psrval  22203  psrass1lem  22221  psrmulval  22232  mvrfval  22268  opsrval  22335  mpfrcl  22374  evlsval  22375  selvffval  22407  mhpmulcl  22450  psdffval  22458  coe1mul2  22568  cply1mul  22594  evls1fval  22617  evl1fval  22626  evl1maprhm  22677  mamufval  22687  mvmulfval  22837  marepvfval  22860  submafval  22874  mdetfval  22881  madufval  22932  minmar1fval  22941  mat2pmatfval  23021  cpm2mfval  23047  decpmatmullem  23069  decpmatmulsumfsupp  23071  pm2mpval  23093  pm2mpmhmlem1  23116  pm2mpmhmlem2  23117  chpmatfval  23128  ntrfval  23322  clsfval  23323  neifval  23397  lpfval  23436  ordtval  23487  ordtbas2  23489  ordtcnv  23499  ordtrest  23500  ordtrest2  23502  cnpfval  23532  kqval  24025  fmval  24242  fmf  24244  flffval  24288  fcfval  24332  cnextval  24360  tsmsval2  24429  nmfval  24887  nmpropd  24893  nmpropd2  24894  subgnm  24932  tngnm  24950  nmofval  25013  pi1xfrcnv  25358  iscph  25471  tcphval  25519  limcfval  26172  dvfval  26197  eldv  26198  mdegfval  26360  mdegmullem  26376  mdegpropd  26382  coe1mul3  26397  ig1pval  26474  taylfval  26668  ishlg2  29047  ishlg  29050  mirval  29109  ishpg  29219  lmif  29272  islmib  29274  vtxdgfval  30030  vtxdeqd  30040  grpoinvfval  31106  nmoofval  31346  eigvalfval  32481  ressnm  33507  tocycval  33651  idlsrgval  34017  selvply1rhmlemb  34133  extvval  34145  extvfval  34146  mplvrpmrhm  34161  issply  34175  minplyval  34319  ordtprsval  34532  ordtprsuni  34533  ordtrestNEW  34535  ofcfval  34712  ofcfval3  34716  omsval  34908  sitgval  34947  issibf  34948  sitgfval  34956  signstfv  35175  cvmliftlem5  36023  cvmliftlem15  36032  mvrsval  36239  mrsubffval  36241  elmrsubrn  36254  msubffval  36257  mvhfval  36267  msrfval  36271  fwddifval  36897  fwddifnval  36898  tailfval  37130  bj-imdirvallem  38069  bj-endval  38204  lsatset  40015  lkrfval  40112  pmapfval  40781  pclfvalN  40914  polfvalN  40929  watfvalN  41017  ldilfset  41133  ltrnfset  41142  dilfsetN  41177  trnfsetN  41180  trlfset  41185  trlset  41186  tgrpfset  41769  tendofset  41783  erngfset  41824  erngset  41825  erngfset-rN  41832  erngset-rN  41833  dvafset  42029  diaffval  42055  diafval  42056  dvhfset  42105  docaffvalN  42146  docafvalN  42147  djaffvalN  42158  dibffval  42165  dibfval  42166  dicffval  42199  dicfval  42200  dihffval  42255  dochffval  42374  dochfval  42375  djhffval  42421  lcdfval  42613  mapdffval  42651  mapdfval  42652  hvmapffval  42783  hvmapfval  42784  hdmap1ffval  42820  hdmap1fval  42821  hdmapffval  42851  hdmapfval  42852  hgmapffval  42910  hgmapfval  42911  hlhilset  42959  prjcrvfval  43621  hbtlem1  44083  hbtlem7  44085  cytpval  44162  rfovd  44960  fsovd  44967  fsovcnvlem  44972  dssmapfvd  44976  ntrneibex  45032  mnringvald  45170  ovnval  47495  hspmbllem2  47581  smflimsuplem1  47774  smflimsuplem3  47776  smflimsuplem7  47780  smflimsup  47782  ply1mulgsumlem3  49444  ply1mulgsumlem4  49445  ply1mulgsum  49446  lincval  49465  iinfprg  50111  fucofvalg  50370  precofval3  50423  prcofvalg  50428  lmdfval  50701  cmdfval  50702