Theorem mpteq12dv 5191

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144   ↦ cmpt 5185

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-opab 5167  df-mpt 5186

This theorem is used by:  mpteq1  5193  mpteq1i  5195  mpteq12i  5201  ovmpt3rab1  7679  offval  7702  offval3  7994  cureq  8892  cantnffval  9667  cnfcomlem  9703  fseqenlem1  10106  dfac12lem1  10225  dfac12r  10228  ackbij2lem2  10320  ackbij2lem3  10321  hfom  10324  indv  12325  ccatfval  14721  swrdval  14795  revval  14913  odzval  16974  vdwpc  17163  restval  17602  prdsval  17631  imasval  17688  qusval  17719  mrcfval  17787  cidfval  17855  monfval  17912  ismon  17913  isepi  17920  idfuval  18056  resfval  18072  resfval2  18073  fucval  18141  homafval  18209  idafval  18237  prfval  18378  prf2fval  18380  curfval  18402  curfpropd  18412  hofval  18431  hof2fval  18434  yonedalem3a  18453  yonedalem4a  18454  yonedalem4c  18456  yonedainv  18460  lubfval  18527  glbfval  18540  ipoval  18709  grpinvfval  19194  grpinvfvalALT  19195  grpinvpropd  19230  mulgnn0gsum  19295  cntzfval  19539  pmtrfval  19669  psgnfval  19719  odfval  19751  odfvalALT  19752  sylow1lem2  19818  sylow1lem4  19820  sylow2blem1  19839  sylow3lem1  19846  sylow3lem2  19847  sylow3lem3  19848  sylow3lem6  19851  pj1fval  19913  vrgpfval  19985  gsum2dlem2  20190  gsum2d2  20193  dprdval  20224  dprd2dlem2  20261  dprd2dlem1  20262  dprd2da  20263  dprd2d2  20265  dpjfval  20276  srgbinom  20462  rgspnval  20869  staffval  21103  lspfval  21253  lsppropd  21298  sraval  21455  isphl  21939  ocvfval  21977  pjfval  22017  uvcfval  22095  aspval  22185  asclfval  22191  ressascl  22209  psrval  22228  psrass1lem  22246  psrmulval  22257  mvrfval  22293  opsrval  22360  mpfrcl  22399  evlsval  22400  selvffval  22432  mhpmulcl  22475  psdffval  22483  coe1mul2  22593  cply1mul  22619  evls1fval  22642  evl1fval  22651  evl1maprhm  22702  mamufval  22712  mvmulfval  22862  marepvfval  22885  submafval  22899  mdetfval  22906  madufval  22957  minmar1fval  22966  mat2pmatfval  23046  cpm2mfval  23072  decpmatmullem  23094  decpmatmulsumfsupp  23096  pm2mpval  23118  pm2mpmhmlem1  23141  pm2mpmhmlem2  23142  chpmatfval  23153  ntrfval  23347  clsfval  23348  neifval  23422  lpfval  23461  ordtval  23512  ordtbas2  23514  ordtcnv  23524  ordtrest  23525  ordtrest2  23527  cnpfval  23557  kqval  24050  fmval  24267  fmf  24269  flffval  24313  fcfval  24357  cnextval  24385  tsmsval2  24454  nmfval  24912  nmpropd  24918  nmpropd2  24919  subgnm  24957  tngnm  24975  nmofval  25038  pi1xfrcnv  25383  iscph  25496  tcphval  25544  limcfval  26197  dvfval  26222  eldv  26223  mdegfval  26385  mdegmullem  26401  mdegpropd  26407  coe1mul3  26422  ig1pval  26499  taylfval  26691  ishlg2  29070  ishlg  29073  mirval  29132  ishpg  29242  lmif  29295  islmib  29297  vtxdgfval  30053  vtxdeqd  30063  grpoinvfval  31129  nmoofval  31369  eigvalfval  32504  ressnm  33571  tocycval  33715  idlsrgval  34081  selvply1rhmlemb  34197  extvval  34209  extvfval  34210  mplvrpmrhm  34225  issply  34239  minplyval  34383  ordtprsval  34596  ordtprsuni  34597  ordtrestNEW  34599  ofcfval  34776  ofcfval3  34780  omsval  34971  sitgval  35010  issibf  35011  sitgfval  35019  signstfv  35238  cvmliftlem5  36140  cvmliftlem15  36149  mvrsval  36356  mrsubffval  36358  elmrsubrn  36371  msubffval  36374  mvhfval  36384  msrfval  36388  fwddifval  37019  fwddifnval  37020  tailfval  37252  bj-imdirvallem  38194  bj-endval  38329  lsatset  40140  lkrfval  40237  pmapfval  40906  pclfvalN  41039  polfvalN  41054  watfvalN  41142  ldilfset  41258  ltrnfset  41267  dilfsetN  41302  trnfsetN  41305  trlfset  41310  trlset  41311  tgrpfset  41894  tendofset  41908  erngfset  41949  erngset  41950  erngfset-rN  41957  erngset-rN  41958  dvafset  42154  diaffval  42180  diafval  42181  dvhfset  42230  docaffvalN  42271  docafvalN  42272  djaffvalN  42283  dibffval  42290  dibfval  42291  dicffval  42324  dicfval  42325  dihffval  42380  dochffval  42499  dochfval  42500  djhffval  42546  lcdfval  42738  mapdffval  42776  mapdfval  42777  hvmapffval  42908  hvmapfval  42909  hdmap1ffval  42945  hdmap1fval  42946  hdmapffval  42976  hdmapfval  42977  hgmapffval  43035  hgmapfval  43036  hlhilset  43084  prjcrvfval  43760  hbtlem1  44218  hbtlem7  44220  cytpval  44297  rfovd  45094  fsovd  45101  fsovcnvlem  45106  dssmapfvd  45110  ntrneibex  45166  mnringvald  45304  ovnval  47644  hspmbllem2  47730  smflimsuplem1  47923  smflimsuplem3  47925  smflimsuplem7  47929  smflimsup  47931  ply1mulgsumlem3  49593  ply1mulgsumlem4  49594  ply1mulgsum  49595  lincval  49614  iinfprg  50266  fucofvalg  50533  postcof2  50593  precofval3  50599  prcofvalg  50604  lmdfval  50925  cmdfval  50926