Theorem mpteq12dv 5144

Description: An equality inference for the maps-to notation. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 16-Dec-2013.) Drop ax-10 2141 while shortening its proof. (Revised by Steven Nguyen and Gino Giotto, 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		nfv 1911	. 2 ⊢ Ⅎ𝑥𝜑
2		mpteq12dv.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
3		mpteq12dv.2	. 2 ⊢ (𝜑 → 𝐵 = 𝐷)
4	1, 2, 3	mpteq12df 5141	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))

Syntax hints:   → wi 4   = wceq 1533   ↦ cmpt 5139

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-12 2172  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-opab 5122  df-mpt 5140

This theorem is referenced by:  mpteq12i  5152  ovmpt3rab1  7397  offval  7410  offval3  7677  cantnffval  9120  cnfcomlem  9156  fseqenlem1  9444  dfac12lem1  9563  dfac12r  9566  ackbij2lem2  9656  ackbij2lem3  9657  r1om  9660  ccatfval  13919  swrdval  13999  revval  14116  odzval  16122  vdwpc  16310  restval  16694  prdsval  16722  imasval  16778  qusval  16809  mrcfval  16873  cidfval  16941  monfval  16996  ismon  16997  isepi  17004  idfuval  17140  resfval  17156  resfval2  17157  fucval  17222  homafval  17283  idafval  17311  prfval  17443  prf2fval  17445  curfval  17467  curfpropd  17477  hofval  17496  hof2fval  17499  yonedalem3a  17518  yonedalem4a  17519  yonedalem4c  17521  yonedainv  17525  lubfval  17582  glbfval  17595  ipoval  17758  grpinvfval  18136  grpinvfvalALT  18137  grpinvpropd  18168  mulgnn0gsum  18228  cntzfval  18444  pmtrfval  18572  psgnfval  18622  odfval  18654  odfvalALT  18655  sylow1lem2  18718  sylow1lem4  18720  sylow2blem1  18739  sylow3lem1  18746  sylow3lem2  18747  sylow3lem3  18748  sylow3lem6  18751  pj1fval  18814  vrgpfval  18886  gsum2dlem2  19085  gsum2d2  19088  dprdval  19119  dprd2dlem2  19156  dprd2dlem1  19157  dprd2da  19158  dprd2d2  19160  dpjfval  19171  srgbinom  19289  staffval  19612  lspfval  19739  lsppropd  19784  sraval  19942  aspval  20096  asclfval  20102  ressascl  20119  psrval  20136  psrass1lem  20151  psrmulval  20160  mvrfval  20194  opsrval  20249  mpfrcl  20292  evlsval  20293  selvffval  20323  coe1mul2  20431  cply1mul  20456  evls1fval  20476  evl1fval  20485  isphl  20766  ocvfval  20804  pjfval  20844  uvcfval  20922  mamufval  20990  mvmulfval  21145  marepvfval  21168  submafval  21182  mdetfval  21189  madufval  21240  minmar1fval  21249  mat2pmatfval  21325  cpm2mfval  21351  decpmatmullem  21373  decpmatmulsumfsupp  21375  pm2mpval  21397  pm2mpmhmlem1  21420  pm2mpmhmlem2  21421  chpmatfval  21432  ntrfval  21626  clsfval  21627  neifval  21701  lpfval  21740  ordtval  21791  ordtbas2  21793  ordtcnv  21803  ordtrest  21804  ordtrest2  21806  cnpfval  21836  kqval  22328  fmval  22545  fmf  22547  flffval  22591  fcfval  22635  cnextval  22663  tsmsval2  22732  nmfval  23192  nmpropd  23197  nmpropd2  23198  subgnm  23236  tngnm  23254  nmofval  23317  pi1xfrcnv  23655  iscph  23768  tcphval  23815  limcfval  24464  dvfval  24489  eldv  24490  mdegfval  24650  mdegmullem  24666  mdegpropd  24672  coe1mul3  24687  ig1pval  24760  taylfval  24941  ishlg  26382  mirval  26435  ishpg  26539  lmif  26565  islmib  26567  vtxdgfval  27243  vtxdeqd  27253  grpoinvfval  28293  nmoofval  28533  eigvalfval  29668  ressnm  30633  tocycval  30745  ordtprsval  31156  ordtprsuni  31157  ordtrestNEW  31159  indv  31266  ofcfval  31352  ofcfval3  31356  omsval  31546  sitgval  31585  issibf  31586  sitgfval  31594  signstfv  31828  cvmliftlem5  32531  cvmliftlem15  32540  mvrsval  32747  mrsubffval  32749  elmrsubrn  32762  msubffval  32765  mvhfval  32775  msrfval  32779  fwddifval  33618  fwddifnval  33619  tailfval  33715  bj-imdirval  34466  bj-endval  34590  cureq  34862  lsatset  36120  lkrfval  36217  pmapfval  36886  pclfvalN  37019  polfvalN  37034  watfvalN  37122  ldilfset  37238  ltrnfset  37247  dilfsetN  37282  trnfsetN  37285  trlfset  37290  trlset  37291  tgrpfset  37874  tendofset  37888  erngfset  37929  erngset  37930  erngfset-rN  37937  erngset-rN  37938  dvafset  38134  diaffval  38160  diafval  38161  dvhfset  38210  docaffvalN  38251  docafvalN  38252  djaffvalN  38263  dibffval  38270  dibfval  38271  dicffval  38304  dicfval  38305  dihffval  38360  dochffval  38479  dochfval  38480  djhffval  38526  lcdfval  38718  mapdffval  38756  mapdfval  38757  hvmapffval  38888  hvmapfval  38889  hdmap1ffval  38925  hdmap1fval  38926  hdmapffval  38956  hdmapfval  38957  hgmapffval  39015  hgmapfval  39016  hlhilset  39064  hbtlem1  39716  hbtlem7  39718  rgspnval  39761  cytpval  39802  rfovd  40340  fsovd  40347  fsovcnvlem  40352  dssmapfvd  40356  ntrneibex  40416  ovnval  42816  hspmbllem2  42902  smflimsuplem1  43087  smflimsuplem3  43089  smflimsuplem7  43093  smflimsup  43095  ply1mulgsumlem3  44435  ply1mulgsumlem4  44436  ply1mulgsum  44437  lincval  44457