Theorem mpteq12dv 5180

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 2182. (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 5179	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))

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

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 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-opab 5156  df-mpt 5175

This theorem is referenced by:  mpteq1  5182  mpteq1i  5184  mpteq12i  5190  ovmpt3rab1  7610  offval  7625  offval3  7920  cantnffval  9560  cnfcomlem  9596  fseqenlem1  9922  dfac12lem1  10042  dfac12r  10045  ackbij2lem2  10137  ackbij2lem3  10138  r1om  10141  ccatfval  14482  swrdval  14553  revval  14669  odzval  16705  vdwpc  16894  restval  17332  prdsval  17361  imasval  17417  qusval  17448  mrcfval  17516  cidfval  17584  monfval  17641  ismon  17642  isepi  17649  idfuval  17785  resfval  17801  resfval2  17802  fucval  17870  homafval  17938  idafval  17966  prfval  18107  prf2fval  18109  curfval  18131  curfpropd  18141  hofval  18160  hof2fval  18163  yonedalem3a  18182  yonedalem4a  18183  yonedalem4c  18185  yonedainv  18189  lubfval  18256  glbfval  18269  ipoval  18438  grpinvfval  18893  grpinvfvalALT  18894  grpinvpropd  18930  mulgnn0gsum  18995  cntzfval  19234  pmtrfval  19364  psgnfval  19414  odfval  19446  odfvalALT  19447  sylow1lem2  19513  sylow1lem4  19515  sylow2blem1  19534  sylow3lem1  19541  sylow3lem2  19542  sylow3lem3  19543  sylow3lem6  19546  pj1fval  19608  vrgpfval  19680  gsum2dlem2  19885  gsum2d2  19888  dprdval  19919  dprd2dlem2  19956  dprd2dlem1  19957  dprd2da  19958  dprd2d2  19960  dpjfval  19971  srgbinom  20151  rgspnval  20529  staffval  20758  lspfval  20908  lsppropd  20954  sraval  21111  isphl  21567  ocvfval  21605  pjfval  21645  uvcfval  21723  aspval  21812  asclfval  21818  ressascl  21835  psrval  21854  psrass1lem  21871  psrmulval  21883  mvrfval  21919  opsrval  21982  mpfrcl  22021  evlsval  22022  selvffval  22049  mhpmulcl  22065  psdffval  22073  coe1mul2  22184  cply1mul  22212  evls1fval  22235  evl1fval  22244  evl1maprhm  22295  mamufval  22308  mvmulfval  22458  marepvfval  22481  submafval  22495  mdetfval  22502  madufval  22553  minmar1fval  22562  mat2pmatfval  22639  cpm2mfval  22665  decpmatmullem  22687  decpmatmulsumfsupp  22689  pm2mpval  22711  pm2mpmhmlem1  22734  pm2mpmhmlem2  22735  chpmatfval  22746  ntrfval  22940  clsfval  22941  neifval  23015  lpfval  23054  ordtval  23105  ordtbas2  23107  ordtcnv  23117  ordtrest  23118  ordtrest2  23120  cnpfval  23150  kqval  23642  fmval  23859  fmf  23861  flffval  23905  fcfval  23949  cnextval  23977  tsmsval2  24046  nmfval  24504  nmpropd  24510  nmpropd2  24511  subgnm  24549  tngnm  24567  nmofval  24630  pi1xfrcnv  24985  iscph  25098  tcphval  25146  limcfval  25801  dvfval  25826  eldv  25827  mdegfval  25995  mdegmullem  26011  mdegpropd  26017  coe1mul3  26032  ig1pval  26109  taylfval  26294  ishlg  28581  mirval  28634  ishpg  28738  lmif  28764  islmib  28766  vtxdgfval  29448  vtxdeqd  29458  grpoinvfval  30504  nmoofval  30744  eigvalfval  31879  indv  32838  ressnm  32952  tocycval  33084  idlsrgval  33475  extvval  33582  extvfval  33583  mplvrpmrhm  33595  issply  33602  minplyval  33739  ordtprsval  33952  ordtprsuni  33953  ordtrestNEW  33955  ofcfval  34132  ofcfval3  34136  omsval  34327  sitgval  34366  issibf  34367  sitgfval  34375  signstfv  34597  cvmliftlem5  35354  cvmliftlem15  35363  mvrsval  35570  mrsubffval  35572  elmrsubrn  35585  msubffval  35588  mvhfval  35598  msrfval  35602  fwddifval  36227  fwddifnval  36228  tailfval  36437  bj-imdirvallem  37245  bj-endval  37380  cureq  37657  lsatset  39110  lkrfval  39207  pmapfval  39876  pclfvalN  40009  polfvalN  40024  watfvalN  40112  ldilfset  40228  ltrnfset  40237  dilfsetN  40272  trnfsetN  40275  trlfset  40280  trlset  40281  tgrpfset  40864  tendofset  40878  erngfset  40919  erngset  40920  erngfset-rN  40927  erngset-rN  40928  dvafset  41124  diaffval  41150  diafval  41151  dvhfset  41200  docaffvalN  41241  docafvalN  41242  djaffvalN  41253  dibffval  41260  dibfval  41261  dicffval  41294  dicfval  41295  dihffval  41350  dochffval  41469  dochfval  41470  djhffval  41516  lcdfval  41708  mapdffval  41746  mapdfval  41747  hvmapffval  41878  hvmapfval  41879  hdmap1ffval  41915  hdmap1fval  41916  hdmapffval  41946  hdmapfval  41947  hgmapffval  42005  hgmapfval  42006  hlhilset  42054  prjcrvfval  42750  hbtlem1  43241  hbtlem7  43243  cytpval  43320  rfovd  44119  fsovd  44126  fsovcnvlem  44131  dssmapfvd  44135  ntrneibex  44191  mnringvald  44331  ovnval  46664  hspmbllem2  46750  smflimsuplem1  46943  smflimsuplem3  46945  smflimsuplem7  46949  smflimsup  46951  ply1mulgsumlem3  48514  ply1mulgsumlem4  48515  ply1mulgsum  48516  lincval  48535  iinfprg  49185  fucofvalg  49444  precofval3  49497  prcofvalg  49502  lmdfval  49775  cmdfval  49776