Theorem mpteq12dv 5182

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 2142, ax-12 2178. (Revised by SN and GG, 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 5181	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   ↦ cmpt 5176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-opab 5158  df-mpt 5177

This theorem is referenced by:  mpteq1  5184  mpteq1i  5186  mpteq12i  5192  ovmpt3rab1  7611  offval  7626  offval3  7924  cantnffval  9578  cnfcomlem  9614  fseqenlem1  9937  dfac12lem1  10057  dfac12r  10060  ackbij2lem2  10152  ackbij2lem3  10153  r1om  10156  ccatfval  14498  swrdval  14568  revval  14684  odzval  16721  vdwpc  16910  restval  17348  prdsval  17377  imasval  17433  qusval  17464  mrcfval  17532  cidfval  17600  monfval  17657  ismon  17658  isepi  17665  idfuval  17801  resfval  17817  resfval2  17818  fucval  17886  homafval  17954  idafval  17982  prfval  18123  prf2fval  18125  curfval  18147  curfpropd  18157  hofval  18176  hof2fval  18179  yonedalem3a  18198  yonedalem4a  18199  yonedalem4c  18201  yonedainv  18205  lubfval  18272  glbfval  18285  ipoval  18454  grpinvfval  18875  grpinvfvalALT  18876  grpinvpropd  18912  mulgnn0gsum  18977  cntzfval  19217  pmtrfval  19347  psgnfval  19397  odfval  19429  odfvalALT  19430  sylow1lem2  19496  sylow1lem4  19498  sylow2blem1  19517  sylow3lem1  19524  sylow3lem2  19525  sylow3lem3  19526  sylow3lem6  19529  pj1fval  19591  vrgpfval  19663  gsum2dlem2  19868  gsum2d2  19871  dprdval  19902  dprd2dlem2  19939  dprd2dlem1  19940  dprd2da  19941  dprd2d2  19943  dpjfval  19954  srgbinom  20134  rgspnval  20515  staffval  20744  lspfval  20894  lsppropd  20940  sraval  21097  isphl  21553  ocvfval  21591  pjfval  21631  uvcfval  21709  aspval  21798  asclfval  21804  ressascl  21821  psrval  21840  psrass1lem  21857  psrmulval  21869  mvrfval  21906  opsrval  21969  mpfrcl  22008  evlsval  22009  selvffval  22036  mhpmulcl  22052  psdffval  22060  coe1mul2  22171  cply1mul  22199  evls1fval  22222  evl1fval  22231  evl1maprhm  22282  mamufval  22295  mvmulfval  22445  marepvfval  22468  submafval  22482  mdetfval  22489  madufval  22540  minmar1fval  22549  mat2pmatfval  22626  cpm2mfval  22652  decpmatmullem  22674  decpmatmulsumfsupp  22676  pm2mpval  22698  pm2mpmhmlem1  22721  pm2mpmhmlem2  22722  chpmatfval  22733  ntrfval  22927  clsfval  22928  neifval  23002  lpfval  23041  ordtval  23092  ordtbas2  23094  ordtcnv  23104  ordtrest  23105  ordtrest2  23107  cnpfval  23137  kqval  23629  fmval  23846  fmf  23848  flffval  23892  fcfval  23936  cnextval  23964  tsmsval2  24033  nmfval  24492  nmpropd  24498  nmpropd2  24499  subgnm  24537  tngnm  24555  nmofval  24618  pi1xfrcnv  24973  iscph  25086  tcphval  25134  limcfval  25789  dvfval  25814  eldv  25815  mdegfval  25983  mdegmullem  25999  mdegpropd  26005  coe1mul3  26020  ig1pval  26097  taylfval  26282  ishlg  28565  mirval  28618  ishpg  28722  lmif  28748  islmib  28750  vtxdgfval  29431  vtxdeqd  29441  grpoinvfval  30484  nmoofval  30724  eigvalfval  31859  indv  32808  ressnm  32919  tocycval  33063  idlsrgval  33450  minplyval  33671  ordtprsval  33884  ordtprsuni  33885  ordtrestNEW  33887  ofcfval  34064  ofcfval3  34068  omsval  34260  sitgval  34299  issibf  34300  sitgfval  34308  signstfv  34530  cvmliftlem5  35261  cvmliftlem15  35270  mvrsval  35477  mrsubffval  35479  elmrsubrn  35492  msubffval  35495  mvhfval  35505  msrfval  35509  fwddifval  36135  fwddifnval  36136  tailfval  36345  bj-imdirvallem  37153  bj-endval  37288  cureq  37575  lsatset  38968  lkrfval  39065  pmapfval  39735  pclfvalN  39868  polfvalN  39883  watfvalN  39971  ldilfset  40087  ltrnfset  40096  dilfsetN  40131  trnfsetN  40134  trlfset  40139  trlset  40140  tgrpfset  40723  tendofset  40737  erngfset  40778  erngset  40779  erngfset-rN  40786  erngset-rN  40787  dvafset  40983  diaffval  41009  diafval  41010  dvhfset  41059  docaffvalN  41100  docafvalN  41101  djaffvalN  41112  dibffval  41119  dibfval  41120  dicffval  41153  dicfval  41154  dihffval  41209  dochffval  41328  dochfval  41329  djhffval  41375  lcdfval  41567  mapdffval  41605  mapdfval  41606  hvmapffval  41737  hvmapfval  41738  hdmap1ffval  41774  hdmap1fval  41775  hdmapffval  41805  hdmapfval  41806  hgmapffval  41864  hgmapfval  41865  hlhilset  41913  prjcrvfval  42604  hbtlem1  43096  hbtlem7  43098  cytpval  43175  rfovd  43974  fsovd  43981  fsovcnvlem  43986  dssmapfvd  43990  ntrneibex  44046  mnringvald  44186  ovnval  46523  hspmbllem2  46609  smflimsuplem1  46802  smflimsuplem3  46804  smflimsuplem7  46808  smflimsup  46810  ply1mulgsumlem3  48374  ply1mulgsumlem4  48375  ply1mulgsum  48376  lincval  48395  iinfprg  49045  fucofvalg  49304  precofval3  49357  prcofvalg  49362  lmdfval  49635  cmdfval  49636