Theorem mpteq12dv 5185

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113   ↦ cmpt 5179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-opab 5161  df-mpt 5180

This theorem is referenced by:  mpteq1  5187  mpteq1i  5189  mpteq12i  5195  ovmpt3rab1  7616  offval  7631  offval3  7926  cantnffval  9572  cnfcomlem  9608  fseqenlem1  9934  dfac12lem1  10054  dfac12r  10057  ackbij2lem2  10149  ackbij2lem3  10150  r1om  10153  ccatfval  14496  swrdval  14567  revval  14683  odzval  16719  vdwpc  16908  restval  17346  prdsval  17375  imasval  17432  qusval  17463  mrcfval  17531  cidfval  17599  monfval  17656  ismon  17657  isepi  17664  idfuval  17800  resfval  17816  resfval2  17817  fucval  17885  homafval  17953  idafval  17981  prfval  18122  prf2fval  18124  curfval  18146  curfpropd  18156  hofval  18175  hof2fval  18178  yonedalem3a  18197  yonedalem4a  18198  yonedalem4c  18200  yonedainv  18204  lubfval  18271  glbfval  18284  ipoval  18453  grpinvfval  18908  grpinvfvalALT  18909  grpinvpropd  18945  mulgnn0gsum  19010  cntzfval  19249  pmtrfval  19379  psgnfval  19429  odfval  19461  odfvalALT  19462  sylow1lem2  19528  sylow1lem4  19530  sylow2blem1  19549  sylow3lem1  19556  sylow3lem2  19557  sylow3lem3  19558  sylow3lem6  19561  pj1fval  19623  vrgpfval  19695  gsum2dlem2  19900  gsum2d2  19903  dprdval  19934  dprd2dlem2  19971  dprd2dlem1  19972  dprd2da  19973  dprd2d2  19975  dpjfval  19986  srgbinom  20166  rgspnval  20545  staffval  20774  lspfval  20924  lsppropd  20970  sraval  21127  isphl  21583  ocvfval  21621  pjfval  21661  uvcfval  21739  aspval  21828  asclfval  21834  ressascl  21852  psrval  21871  psrass1lem  21888  psrmulval  21900  mvrfval  21936  opsrval  22001  mpfrcl  22040  evlsval  22041  selvffval  22076  mhpmulcl  22092  psdffval  22100  coe1mul2  22211  cply1mul  22240  evls1fval  22263  evl1fval  22272  evl1maprhm  22323  mamufval  22336  mvmulfval  22486  marepvfval  22509  submafval  22523  mdetfval  22530  madufval  22581  minmar1fval  22590  mat2pmatfval  22667  cpm2mfval  22693  decpmatmullem  22715  decpmatmulsumfsupp  22717  pm2mpval  22739  pm2mpmhmlem1  22762  pm2mpmhmlem2  22763  chpmatfval  22774  ntrfval  22968  clsfval  22969  neifval  23043  lpfval  23082  ordtval  23133  ordtbas2  23135  ordtcnv  23145  ordtrest  23146  ordtrest2  23148  cnpfval  23178  kqval  23670  fmval  23887  fmf  23889  flffval  23933  fcfval  23977  cnextval  24005  tsmsval2  24074  nmfval  24532  nmpropd  24538  nmpropd2  24539  subgnm  24577  tngnm  24595  nmofval  24658  pi1xfrcnv  25013  iscph  25126  tcphval  25174  limcfval  25829  dvfval  25854  eldv  25855  mdegfval  26023  mdegmullem  26039  mdegpropd  26045  coe1mul3  26060  ig1pval  26137  taylfval  26322  ishlg  28674  mirval  28727  ishpg  28831  lmif  28857  islmib  28859  vtxdgfval  29541  vtxdeqd  29551  grpoinvfval  30597  nmoofval  30837  eigvalfval  31972  indv  32931  ressnm  33046  tocycval  33190  idlsrgval  33584  extvval  33696  extvfval  33697  mplvrpmrhm  33712  issply  33719  minplyval  33862  ordtprsval  34075  ordtprsuni  34076  ordtrestNEW  34078  ofcfval  34255  ofcfval3  34259  omsval  34450  sitgval  34489  issibf  34490  sitgfval  34498  signstfv  34720  cvmliftlem5  35483  cvmliftlem15  35492  mvrsval  35699  mrsubffval  35701  elmrsubrn  35714  msubffval  35717  mvhfval  35727  msrfval  35731  fwddifval  36356  fwddifnval  36357  tailfval  36566  bj-imdirvallem  37381  bj-endval  37516  cureq  37793  lsatset  39246  lkrfval  39343  pmapfval  40012  pclfvalN  40145  polfvalN  40160  watfvalN  40248  ldilfset  40364  ltrnfset  40373  dilfsetN  40408  trnfsetN  40411  trlfset  40416  trlset  40417  tgrpfset  41000  tendofset  41014  erngfset  41055  erngset  41056  erngfset-rN  41063  erngset-rN  41064  dvafset  41260  diaffval  41286  diafval  41287  dvhfset  41336  docaffvalN  41377  docafvalN  41378  djaffvalN  41389  dibffval  41396  dibfval  41397  dicffval  41430  dicfval  41431  dihffval  41486  dochffval  41605  dochfval  41606  djhffval  41652  lcdfval  41844  mapdffval  41882  mapdfval  41883  hvmapffval  42014  hvmapfval  42015  hdmap1ffval  42051  hdmap1fval  42052  hdmapffval  42082  hdmapfval  42083  hgmapffval  42141  hgmapfval  42142  hlhilset  42190  prjcrvfval  42870  hbtlem1  43361  hbtlem7  43363  cytpval  43440  rfovd  44238  fsovd  44245  fsovcnvlem  44250  dssmapfvd  44254  ntrneibex  44310  mnringvald  44450  ovnval  46781  hspmbllem2  46867  smflimsuplem1  47060  smflimsuplem3  47062  smflimsuplem7  47066  smflimsup  47068  ply1mulgsumlem3  48630  ply1mulgsumlem4  48631  ply1mulgsum  48632  lincval  48651  iinfprg  49300  fucofvalg  49559  precofval3  49612  prcofvalg  49617  lmdfval  49890  cmdfval  49891