Theorem mpteq12dv 5166

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107   ↦ cmpt 5158

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 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-opab 5138  df-mpt 5159

This theorem is referenced by:  mpteq1  5168  mpteq1i  5171  mpteq12i  5181  ovmpt3rab1  7536  offval  7551  offval3  7834  cantnffval  9430  cnfcomlem  9466  fseqenlem1  9789  dfac12lem1  9908  dfac12r  9911  ackbij2lem2  10005  ackbij2lem3  10006  r1om  10009  ccatfval  14285  swrdval  14365  revval  14482  odzval  16501  vdwpc  16690  restval  17146  prdsval  17175  imasval  17231  qusval  17262  mrcfval  17326  cidfval  17394  monfval  17453  ismon  17454  isepi  17461  idfuval  17600  resfval  17616  resfval2  17617  fucval  17684  homafval  17753  idafval  17781  prfval  17925  prf2fval  17927  curfval  17950  curfpropd  17960  hofval  17979  hof2fval  17982  yonedalem3a  18001  yonedalem4a  18002  yonedalem4c  18004  yonedainv  18008  lubfval  18077  glbfval  18090  ipoval  18257  grpinvfval  18627  grpinvfvalALT  18628  grpinvpropd  18659  mulgnn0gsum  18719  cntzfval  18935  pmtrfval  19067  psgnfval  19117  odfval  19149  odfvalALT  19150  sylow1lem2  19213  sylow1lem4  19215  sylow2blem1  19234  sylow3lem1  19241  sylow3lem2  19242  sylow3lem3  19243  sylow3lem6  19246  pj1fval  19309  vrgpfval  19381  gsum2dlem2  19581  gsum2d2  19584  dprdval  19615  dprd2dlem2  19652  dprd2dlem1  19653  dprd2da  19654  dprd2d2  19656  dpjfval  19667  srgbinom  19790  staffval  20116  lspfval  20244  lsppropd  20289  sraval  20447  isphl  20842  ocvfval  20880  pjfval  20922  uvcfval  21000  aspval  21086  asclfval  21092  ressascl  21109  psrval  21127  psrass1lemOLD  21152  psrass1lem  21155  psrmulval  21164  mvrfval  21198  opsrval  21256  mpfrcl  21304  evlsval  21305  selvffval  21335  mhpmulcl  21348  coe1mul2  21449  cply1mul  21474  evls1fval  21494  evl1fval  21503  mamufval  21543  mvmulfval  21700  marepvfval  21723  submafval  21737  mdetfval  21744  madufval  21795  minmar1fval  21804  mat2pmatfval  21881  cpm2mfval  21907  decpmatmullem  21929  decpmatmulsumfsupp  21931  pm2mpval  21953  pm2mpmhmlem1  21976  pm2mpmhmlem2  21977  chpmatfval  21988  ntrfval  22184  clsfval  22185  neifval  22259  lpfval  22298  ordtval  22349  ordtbas2  22351  ordtcnv  22361  ordtrest  22362  ordtrest2  22364  cnpfval  22394  kqval  22886  fmval  23103  fmf  23105  flffval  23149  fcfval  23193  cnextval  23221  tsmsval2  23290  nmfval  23753  nmpropd  23759  nmpropd2  23760  subgnm  23798  tngnm  23824  nmofval  23887  pi1xfrcnv  24229  iscph  24343  tcphval  24391  limcfval  25045  dvfval  25070  eldv  25071  mdegfval  25236  mdegmullem  25252  mdegpropd  25258  coe1mul3  25273  ig1pval  25346  taylfval  25527  ishlg  26972  mirval  27025  ishpg  27129  lmif  27155  islmib  27157  vtxdgfval  27843  vtxdeqd  27853  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  37011  lkrfval  37108  pmapfval  37777  pclfvalN  37910  polfvalN  37925  watfvalN  38013  ldilfset  38129  ltrnfset  38138  dilfsetN  38173  trnfsetN  38176  trlfset  38181  trlset  38182  tgrpfset  38765  tendofset  38779  erngfset  38820  erngset  38821  erngfset-rN  38828  erngset-rN  38829  dvafset  39025  diaffval  39051  diafval  39052  dvhfset  39101  docaffvalN  39142  docafvalN  39143  djaffvalN  39154  dibffval  39161  dibfval  39162  dicffval  39195  dicfval  39196  dihffval  39251  dochffval  39370  dochfval  39371  djhffval  39417  lcdfval  39609  mapdffval  39647  mapdfval  39648  hvmapffval  39779  hvmapfval  39780  hdmap1ffval  39816  hdmap1fval  39817  hdmapffval  39847  hdmapfval  39848  hgmapffval  39906  hgmapfval  39907  hlhilset  39955  prjcrvfval  40475  hbtlem1  40955  hbtlem7  40957  rgspnval  41000  cytpval  41041  rfovd  41616  fsovd  41623  fsovcnvlem  41628  dssmapfvd  41632  ntrneibex  41690  mnringvald  41833  ovnval  44086  hspmbllem2  44172  smflimsuplem1  44364  smflimsuplem3  44366  smflimsuplem7  44370  smflimsup  44372  ply1mulgsumlem3  45740  ply1mulgsumlem4  45741  ply1mulgsum  45742  lincval  45761