Theorem mpteq12dv 5172

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   ↦ cmpt 5166

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-opab 5148  df-mpt 5167

This theorem is referenced by:  mpteq1  5174  mpteq1i  5176  mpteq12i  5182  ovmpt3rab1  7625  offval  7640  offval3  7935  cantnffval  9584  cnfcomlem  9620  fseqenlem1  9946  dfac12lem1  10066  dfac12r  10069  ackbij2lem2  10161  ackbij2lem3  10162  r1om  10165  indv  12161  ccatfval  14535  swrdval  14606  revval  14722  odzval  16762  vdwpc  16951  restval  17389  prdsval  17418  imasval  17475  qusval  17506  mrcfval  17574  cidfval  17642  monfval  17699  ismon  17700  isepi  17707  idfuval  17843  resfval  17859  resfval2  17860  fucval  17928  homafval  17996  idafval  18024  prfval  18165  prf2fval  18167  curfval  18189  curfpropd  18199  hofval  18218  hof2fval  18221  yonedalem3a  18240  yonedalem4a  18241  yonedalem4c  18243  yonedainv  18247  lubfval  18314  glbfval  18327  ipoval  18496  grpinvfval  18954  grpinvfvalALT  18955  grpinvpropd  18991  mulgnn0gsum  19056  cntzfval  19295  pmtrfval  19425  psgnfval  19475  odfval  19507  odfvalALT  19508  sylow1lem2  19574  sylow1lem4  19576  sylow2blem1  19595  sylow3lem1  19602  sylow3lem2  19603  sylow3lem3  19604  sylow3lem6  19607  pj1fval  19669  vrgpfval  19741  gsum2dlem2  19946  gsum2d2  19949  dprdval  19980  dprd2dlem2  20017  dprd2dlem1  20018  dprd2da  20019  dprd2d2  20021  dpjfval  20032  srgbinom  20212  rgspnval  20589  staffval  20818  lspfval  20968  lsppropd  21013  sraval  21170  isphl  21608  ocvfval  21646  pjfval  21686  uvcfval  21764  aspval  21852  asclfval  21858  ressascl  21876  psrval  21895  psrass1lem  21912  psrmulval  21923  mvrfval  21959  opsrval  22024  mpfrcl  22063  evlsval  22064  selvffval  22099  mhpmulcl  22115  psdffval  22123  coe1mul2  22234  cply1mul  22261  evls1fval  22284  evl1fval  22293  evl1maprhm  22344  mamufval  22357  mvmulfval  22507  marepvfval  22530  submafval  22544  mdetfval  22551  madufval  22602  minmar1fval  22611  mat2pmatfval  22688  cpm2mfval  22714  decpmatmullem  22736  decpmatmulsumfsupp  22738  pm2mpval  22760  pm2mpmhmlem1  22783  pm2mpmhmlem2  22784  chpmatfval  22795  ntrfval  22989  clsfval  22990  neifval  23064  lpfval  23103  ordtval  23154  ordtbas2  23156  ordtcnv  23166  ordtrest  23167  ordtrest2  23169  cnpfval  23199  kqval  23691  fmval  23908  fmf  23910  flffval  23954  fcfval  23998  cnextval  24026  tsmsval2  24095  nmfval  24553  nmpropd  24559  nmpropd2  24560  subgnm  24598  tngnm  24616  nmofval  24679  pi1xfrcnv  25024  iscph  25137  tcphval  25185  limcfval  25839  dvfval  25864  eldv  25865  mdegfval  26027  mdegmullem  26043  mdegpropd  26049  coe1mul3  26064  ig1pval  26141  taylfval  26324  ishlg  28670  mirval  28723  ishpg  28827  lmif  28853  islmib  28855  vtxdgfval  29536  vtxdeqd  29546  grpoinvfval  30593  nmoofval  30833  eigvalfval  31968  ressnm  33024  tocycval  33169  idlsrgval  33563  extvval  33675  extvfval  33676  mplvrpmrhm  33691  issply  33705  minplyval  33849  ordtprsval  34062  ordtprsuni  34063  ordtrestNEW  34065  ofcfval  34242  ofcfval3  34246  omsval  34437  sitgval  34476  issibf  34477  sitgfval  34485  signstfv  34707  cvmliftlem5  35471  cvmliftlem15  35480  mvrsval  35687  mrsubffval  35689  elmrsubrn  35702  msubffval  35705  mvhfval  35715  msrfval  35719  fwddifval  36344  fwddifnval  36345  tailfval  36554  bj-imdirvallem  37494  bj-endval  37629  cureq  37917  lsatset  39436  lkrfval  39533  pmapfval  40202  pclfvalN  40335  polfvalN  40350  watfvalN  40438  ldilfset  40554  ltrnfset  40563  dilfsetN  40598  trnfsetN  40601  trlfset  40606  trlset  40607  tgrpfset  41190  tendofset  41204  erngfset  41245  erngset  41246  erngfset-rN  41253  erngset-rN  41254  dvafset  41450  diaffval  41476  diafval  41477  dvhfset  41526  docaffvalN  41567  docafvalN  41568  djaffvalN  41579  dibffval  41586  dibfval  41587  dicffval  41620  dicfval  41621  dihffval  41676  dochffval  41795  dochfval  41796  djhffval  41842  lcdfval  42034  mapdffval  42072  mapdfval  42073  hvmapffval  42204  hvmapfval  42205  hdmap1ffval  42241  hdmap1fval  42242  hdmapffval  42272  hdmapfval  42273  hgmapffval  42331  hgmapfval  42332  hlhilset  42380  prjcrvfval  43064  hbtlem1  43551  hbtlem7  43553  cytpval  43630  rfovd  44428  fsovd  44435  fsovcnvlem  44440  dssmapfvd  44444  ntrneibex  44500  mnringvald  44640  ovnval  46969  hspmbllem2  47055  smflimsuplem1  47248  smflimsuplem3  47250  smflimsuplem7  47254  smflimsup  47256  ply1mulgsumlem3  48864  ply1mulgsumlem4  48865  ply1mulgsum  48866  lincval  48885  iinfprg  49534  fucofvalg  49793  precofval3  49846  prcofvalg  49851  lmdfval  50124  cmdfval  50125