Theorem mpteq12dv 5170

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 2141, ax-12 2175. (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 481	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷)
4	1, 3	mpteq12dva 5168	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2110   ↦ cmpt 5162

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-opab 5142  df-mpt 5163

This theorem is referenced by:  mpteq1  5172  mpteq1i  5175  mpteq12i  5185  ovmpt3rab1  7522  offval  7537  offval3  7819  cantnffval  9409  cnfcomlem  9445  fseqenlem1  9791  dfac12lem1  9910  dfac12r  9913  ackbij2lem2  10007  ackbij2lem3  10008  r1om  10011  ccatfval  14287  swrdval  14367  revval  14484  odzval  16503  vdwpc  16692  restval  17148  prdsval  17177  imasval  17233  qusval  17264  mrcfval  17328  cidfval  17396  monfval  17455  ismon  17456  isepi  17463  idfuval  17602  resfval  17618  resfval2  17619  fucval  17686  homafval  17755  idafval  17783  prfval  17927  prf2fval  17929  curfval  17952  curfpropd  17962  hofval  17981  hof2fval  17984  yonedalem3a  18003  yonedalem4a  18004  yonedalem4c  18006  yonedainv  18010  lubfval  18079  glbfval  18092  ipoval  18259  grpinvfval  18629  grpinvfvalALT  18630  grpinvpropd  18661  mulgnn0gsum  18721  cntzfval  18937  pmtrfval  19069  psgnfval  19119  odfval  19151  odfvalALT  19152  sylow1lem2  19215  sylow1lem4  19217  sylow2blem1  19236  sylow3lem1  19243  sylow3lem2  19244  sylow3lem3  19245  sylow3lem6  19248  pj1fval  19311  vrgpfval  19383  gsum2dlem2  19583  gsum2d2  19586  dprdval  19617  dprd2dlem2  19654  dprd2dlem1  19655  dprd2da  19656  dprd2d2  19658  dpjfval  19669  srgbinom  19792  staffval  20118  lspfval  20246  lsppropd  20291  sraval  20449  isphl  20844  ocvfval  20882  pjfval  20924  uvcfval  21002  aspval  21088  asclfval  21094  ressascl  21111  psrval  21129  psrass1lemOLD  21154  psrass1lem  21157  psrmulval  21166  mvrfval  21200  opsrval  21258  mpfrcl  21306  evlsval  21307  selvffval  21337  mhpmulcl  21350  coe1mul2  21451  cply1mul  21476  evls1fval  21496  evl1fval  21505  mamufval  21545  mvmulfval  21702  marepvfval  21725  submafval  21739  mdetfval  21746  madufval  21797  minmar1fval  21806  mat2pmatfval  21883  cpm2mfval  21909  decpmatmullem  21931  decpmatmulsumfsupp  21933  pm2mpval  21955  pm2mpmhmlem1  21978  pm2mpmhmlem2  21979  chpmatfval  21990  ntrfval  22186  clsfval  22187  neifval  22261  lpfval  22300  ordtval  22351  ordtbas2  22353  ordtcnv  22363  ordtrest  22364  ordtrest2  22366  cnpfval  22396  kqval  22888  fmval  23105  fmf  23107  flffval  23151  fcfval  23195  cnextval  23223  tsmsval2  23292  nmfval  23755  nmpropd  23761  nmpropd2  23762  subgnm  23800  tngnm  23826  nmofval  23889  pi1xfrcnv  24231  iscph  24345  tcphval  24393  limcfval  25047  dvfval  25072  eldv  25073  mdegfval  25238  mdegmullem  25254  mdegpropd  25260  coe1mul3  25275  ig1pval  25348  taylfval  25529  ishlg  26974  mirval  27027  ishpg  27131  lmif  27157  islmib  27159  vtxdgfval  27845  vtxdeqd  27855  grpoinvfval  28893  nmoofval  29133  eigvalfval  30268  ressnm  31245  tocycval  31384  idlsrgval  31657  ordtprsval  31877  ordtprsuni  31878  ordtrestNEW  31880  indv  31989  ofcfval  32075  ofcfval3  32079  omsval  32269  sitgval  32308  issibf  32309  sitgfval  32317  signstfv  32551  cvmliftlem5  33260  cvmliftlem15  33269  mvrsval  33476  mrsubffval  33478  elmrsubrn  33491  msubffval  33494  mvhfval  33504  msrfval  33508  fwddifval  34473  fwddifnval  34474  tailfval  34570  bj-imdirvallem  35360  bj-endval  35495  cureq  35762  lsatset  37013  lkrfval  37110  pmapfval  37779  pclfvalN  37912  polfvalN  37927  watfvalN  38015  ldilfset  38131  ltrnfset  38140  dilfsetN  38175  trnfsetN  38178  trlfset  38183  trlset  38184  tgrpfset  38767  tendofset  38781  erngfset  38822  erngset  38823  erngfset-rN  38830  erngset-rN  38831  dvafset  39027  diaffval  39053  diafval  39054  dvhfset  39103  docaffvalN  39144  docafvalN  39145  djaffvalN  39156  dibffval  39163  dibfval  39164  dicffval  39197  dicfval  39198  dihffval  39253  dochffval  39372  dochfval  39373  djhffval  39419  lcdfval  39611  mapdffval  39649  mapdfval  39650  hvmapffval  39781  hvmapfval  39782  hdmap1ffval  39818  hdmap1fval  39819  hdmapffval  39849  hdmapfval  39850  hgmapffval  39908  hgmapfval  39909  hlhilset  39957  prjcrvfval  40477  hbtlem1  40957  hbtlem7  40959  rgspnval  41002  cytpval  41043  rfovd  41591  fsovd  41598  fsovcnvlem  41603  dssmapfvd  41607  ntrneibex  41665  mnringvald  41808  ovnval  44061  hspmbllem2  44147  smflimsuplem1  44332  smflimsuplem3  44334  smflimsuplem7  44338  smflimsup  44340  ply1mulgsumlem3  45708  ply1mulgsumlem4  45709  ply1mulgsum  45710  lincval  45729