Theorem mpteq12dv 5240

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 2138, ax-12 2172. (Revised by SN 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		mpteq12dv.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
2		mpteq12dv.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐷)
3	2	adantr 482	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷)
4	1, 3	mpteq12dva 5238	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107   ↦ cmpt 5232

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-opab 5212  df-mpt 5233

This theorem is referenced by:  mpteq1  5242  mpteq1i  5245  mpteq12i  5255  ovmpt3rab1  7664  offval  7679  offval3  7969  cantnffval  9658  cnfcomlem  9694  fseqenlem1  10019  dfac12lem1  10138  dfac12r  10141  ackbij2lem2  10235  ackbij2lem3  10236  r1om  10239  ccatfval  14523  swrdval  14593  revval  14710  odzval  16724  vdwpc  16913  restval  17372  prdsval  17401  imasval  17457  qusval  17488  mrcfval  17552  cidfval  17620  monfval  17679  ismon  17680  isepi  17687  idfuval  17826  resfval  17842  resfval2  17843  fucval  17910  homafval  17979  idafval  18007  prfval  18151  prf2fval  18153  curfval  18176  curfpropd  18186  hofval  18205  hof2fval  18208  yonedalem3a  18227  yonedalem4a  18228  yonedalem4c  18230  yonedainv  18234  lubfval  18303  glbfval  18316  ipoval  18483  grpinvfval  18863  grpinvfvalALT  18864  grpinvpropd  18898  mulgnn0gsum  18960  cntzfval  19184  pmtrfval  19318  psgnfval  19368  odfval  19400  odfvalALT  19401  sylow1lem2  19467  sylow1lem4  19469  sylow2blem1  19488  sylow3lem1  19495  sylow3lem2  19496  sylow3lem3  19497  sylow3lem6  19500  pj1fval  19562  vrgpfval  19634  gsum2dlem2  19839  gsum2d2  19842  dprdval  19873  dprd2dlem2  19910  dprd2dlem1  19911  dprd2da  19912  dprd2d2  19914  dpjfval  19925  srgbinom  20054  staffval  20455  lspfval  20584  lsppropd  20629  sraval  20789  isphl  21181  ocvfval  21219  pjfval  21261  uvcfval  21339  aspval  21427  asclfval  21433  ressascl  21450  psrval  21468  psrass1lemOLD  21493  psrass1lem  21496  psrmulval  21505  mvrfval  21540  opsrval  21601  mpfrcl  21648  evlsval  21649  selvffval  21679  mhpmulcl  21692  coe1mul2  21791  cply1mul  21818  evls1fval  21838  evl1fval  21847  mamufval  21887  mvmulfval  22044  marepvfval  22067  submafval  22081  mdetfval  22088  madufval  22139  minmar1fval  22148  mat2pmatfval  22225  cpm2mfval  22251  decpmatmullem  22273  decpmatmulsumfsupp  22275  pm2mpval  22297  pm2mpmhmlem1  22320  pm2mpmhmlem2  22321  chpmatfval  22332  ntrfval  22528  clsfval  22529  neifval  22603  lpfval  22642  ordtval  22693  ordtbas2  22695  ordtcnv  22705  ordtrest  22706  ordtrest2  22708  cnpfval  22738  kqval  23230  fmval  23447  fmf  23449  flffval  23493  fcfval  23537  cnextval  23565  tsmsval2  23634  nmfval  24097  nmpropd  24103  nmpropd2  24104  subgnm  24142  tngnm  24168  nmofval  24231  pi1xfrcnv  24573  iscph  24687  tcphval  24735  limcfval  25389  dvfval  25414  eldv  25415  mdegfval  25580  mdegmullem  25596  mdegpropd  25602  coe1mul3  25617  ig1pval  25690  taylfval  25871  ishlg  27853  mirval  27906  ishpg  28010  lmif  28036  islmib  28038  vtxdgfval  28724  vtxdeqd  28734  grpoinvfval  29775  nmoofval  30015  eigvalfval  31150  ressnm  32128  tocycval  32267  idlsrgval  32617  minplyval  32766  ordtprsval  32898  ordtprsuni  32899  ordtrestNEW  32901  indv  33010  ofcfval  33096  ofcfval3  33100  omsval  33292  sitgval  33331  issibf  33332  sitgfval  33340  signstfv  33574  cvmliftlem5  34280  cvmliftlem15  34289  mvrsval  34496  mrsubffval  34498  elmrsubrn  34511  msubffval  34514  mvhfval  34524  msrfval  34528  fwddifval  35134  fwddifnval  35135  tailfval  35257  bj-imdirvallem  36061  bj-endval  36196  cureq  36464  lsatset  37860  lkrfval  37957  pmapfval  38627  pclfvalN  38760  polfvalN  38775  watfvalN  38863  ldilfset  38979  ltrnfset  38988  dilfsetN  39023  trnfsetN  39026  trlfset  39031  trlset  39032  tgrpfset  39615  tendofset  39629  erngfset  39670  erngset  39671  erngfset-rN  39678  erngset-rN  39679  dvafset  39875  diaffval  39901  diafval  39902  dvhfset  39951  docaffvalN  39992  docafvalN  39993  djaffvalN  40004  dibffval  40011  dibfval  40012  dicffval  40045  dicfval  40046  dihffval  40101  dochffval  40220  dochfval  40221  djhffval  40267  lcdfval  40459  mapdffval  40497  mapdfval  40498  hvmapffval  40629  hvmapfval  40630  hdmap1ffval  40666  hdmap1fval  40667  hdmapffval  40697  hdmapfval  40698  hgmapffval  40756  hgmapfval  40757  hlhilset  40805  prjcrvfval  41373  hbtlem1  41865  hbtlem7  41867  rgspnval  41910  cytpval  41951  rfovd  42752  fsovd  42759  fsovcnvlem  42764  dssmapfvd  42768  ntrneibex  42824  mnringvald  42967  ovnval  45257  hspmbllem2  45343  smflimsuplem1  45536  smflimsuplem3  45538  smflimsuplem7  45542  smflimsup  45544  ply1mulgsumlem3  47069  ply1mulgsumlem4  47070  ply1mulgsum  47071  lincval  47090