Theorem mpteq12dv 5161

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 2139, ax-12 2173. (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 480	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷)
4	1, 3	mpteq12dva 5159	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108   ↦ cmpt 5153

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-opab 5133  df-mpt 5154

This theorem is referenced by:  mpteq1  5163  mpteq1i  5166  mpteq12i  5176  ovmpt3rab1  7505  offval  7520  offval3  7798  cantnffval  9351  cnfcomlem  9387  fseqenlem1  9711  dfac12lem1  9830  dfac12r  9833  ackbij2lem2  9927  ackbij2lem3  9928  r1om  9931  ccatfval  14204  swrdval  14284  revval  14401  odzval  16420  vdwpc  16609  restval  17054  prdsval  17083  imasval  17139  qusval  17170  mrcfval  17234  cidfval  17302  monfval  17361  ismon  17362  isepi  17369  idfuval  17507  resfval  17523  resfval2  17524  fucval  17591  homafval  17660  idafval  17688  prfval  17832  prf2fval  17834  curfval  17857  curfpropd  17867  hofval  17886  hof2fval  17889  yonedalem3a  17908  yonedalem4a  17909  yonedalem4c  17911  yonedainv  17915  lubfval  17983  glbfval  17996  ipoval  18163  grpinvfval  18533  grpinvfvalALT  18534  grpinvpropd  18565  mulgnn0gsum  18625  cntzfval  18841  pmtrfval  18973  psgnfval  19023  odfval  19055  odfvalALT  19056  sylow1lem2  19119  sylow1lem4  19121  sylow2blem1  19140  sylow3lem1  19147  sylow3lem2  19148  sylow3lem3  19149  sylow3lem6  19152  pj1fval  19215  vrgpfval  19287  gsum2dlem2  19487  gsum2d2  19490  dprdval  19521  dprd2dlem2  19558  dprd2dlem1  19559  dprd2da  19560  dprd2d2  19562  dpjfval  19573  srgbinom  19696  staffval  20022  lspfval  20150  lsppropd  20195  sraval  20353  isphl  20745  ocvfval  20783  pjfval  20823  uvcfval  20901  aspval  20987  asclfval  20993  ressascl  21010  psrval  21028  psrass1lemOLD  21053  psrass1lem  21056  psrmulval  21065  mvrfval  21099  opsrval  21157  mpfrcl  21205  evlsval  21206  selvffval  21236  mhpmulcl  21249  coe1mul2  21350  cply1mul  21375  evls1fval  21395  evl1fval  21404  mamufval  21444  mvmulfval  21599  marepvfval  21622  submafval  21636  mdetfval  21643  madufval  21694  minmar1fval  21703  mat2pmatfval  21780  cpm2mfval  21806  decpmatmullem  21828  decpmatmulsumfsupp  21830  pm2mpval  21852  pm2mpmhmlem1  21875  pm2mpmhmlem2  21876  chpmatfval  21887  ntrfval  22083  clsfval  22084  neifval  22158  lpfval  22197  ordtval  22248  ordtbas2  22250  ordtcnv  22260  ordtrest  22261  ordtrest2  22263  cnpfval  22293  kqval  22785  fmval  23002  fmf  23004  flffval  23048  fcfval  23092  cnextval  23120  tsmsval2  23189  nmfval  23650  nmpropd  23656  nmpropd2  23657  subgnm  23695  tngnm  23721  nmofval  23784  pi1xfrcnv  24126  iscph  24239  tcphval  24287  limcfval  24941  dvfval  24966  eldv  24967  mdegfval  25132  mdegmullem  25148  mdegpropd  25154  coe1mul3  25169  ig1pval  25242  taylfval  25423  ishlg  26867  mirval  26920  ishpg  27024  lmif  27050  islmib  27052  vtxdgfval  27737  vtxdeqd  27747  grpoinvfval  28785  nmoofval  29025  eigvalfval  30160  ressnm  31138  tocycval  31277  idlsrgval  31550  ordtprsval  31770  ordtprsuni  31771  ordtrestNEW  31773  indv  31880  ofcfval  31966  ofcfval3  31970  omsval  32160  sitgval  32199  issibf  32200  sitgfval  32208  signstfv  32442  cvmliftlem5  33151  cvmliftlem15  33160  mvrsval  33367  mrsubffval  33369  elmrsubrn  33382  msubffval  33385  mvhfval  33395  msrfval  33399  fwddifval  34391  fwddifnval  34392  tailfval  34488  bj-imdirvallem  35278  bj-endval  35413  cureq  35680  lsatset  36931  lkrfval  37028  pmapfval  37697  pclfvalN  37830  polfvalN  37845  watfvalN  37933  ldilfset  38049  ltrnfset  38058  dilfsetN  38093  trnfsetN  38096  trlfset  38101  trlset  38102  tgrpfset  38685  tendofset  38699  erngfset  38740  erngset  38741  erngfset-rN  38748  erngset-rN  38749  dvafset  38945  diaffval  38971  diafval  38972  dvhfset  39021  docaffvalN  39062  docafvalN  39063  djaffvalN  39074  dibffval  39081  dibfval  39082  dicffval  39115  dicfval  39116  dihffval  39171  dochffval  39290  dochfval  39291  djhffval  39337  lcdfval  39529  mapdffval  39567  mapdfval  39568  hvmapffval  39699  hvmapfval  39700  hdmap1ffval  39736  hdmap1fval  39737  hdmapffval  39767  hdmapfval  39768  hgmapffval  39826  hgmapfval  39827  hlhilset  39875  hbtlem1  40864  hbtlem7  40866  rgspnval  40909  cytpval  40950  rfovd  41498  fsovd  41505  fsovcnvlem  41510  dssmapfvd  41514  ntrneibex  41572  mnringvald  41715  ovnval  43969  hspmbllem2  44055  smflimsuplem1  44240  smflimsuplem3  44242  smflimsuplem7  44246  smflimsup  44248  ply1mulgsumlem3  45617  ply1mulgsumlem4  45618  ply1mulgsum  45619  lincval  45638