Theorem mpteq12dv 5238

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 2174. (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 5236	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105   ↦ cmpt 5230

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-opab 5210  df-mpt 5231

This theorem is referenced by:  mpteq1  5240  mpteq1i  5243  mpteq12i  5253  ovmpt3rab1  7690  offval  7705  offval3  8005  cantnffval  9700  cnfcomlem  9736  fseqenlem1  10061  dfac12lem1  10181  dfac12r  10184  ackbij2lem2  10276  ackbij2lem3  10277  r1om  10280  ccatfval  14607  swrdval  14677  revval  14794  odzval  16824  vdwpc  17013  restval  17472  prdsval  17501  imasval  17557  qusval  17588  mrcfval  17652  cidfval  17720  monfval  17779  ismon  17780  isepi  17787  idfuval  17926  resfval  17942  resfval2  17943  fucval  18013  homafval  18082  idafval  18110  prfval  18254  prf2fval  18256  curfval  18279  curfpropd  18289  hofval  18308  hof2fval  18311  yonedalem3a  18330  yonedalem4a  18331  yonedalem4c  18333  yonedainv  18337  lubfval  18407  glbfval  18420  ipoval  18587  grpinvfval  19008  grpinvfvalALT  19009  grpinvpropd  19045  mulgnn0gsum  19110  cntzfval  19350  pmtrfval  19482  psgnfval  19532  odfval  19564  odfvalALT  19565  sylow1lem2  19631  sylow1lem4  19633  sylow2blem1  19652  sylow3lem1  19659  sylow3lem2  19660  sylow3lem3  19661  sylow3lem6  19664  pj1fval  19726  vrgpfval  19798  gsum2dlem2  20003  gsum2d2  20006  dprdval  20037  dprd2dlem2  20074  dprd2dlem1  20075  dprd2da  20076  dprd2d2  20078  dpjfval  20089  srgbinom  20248  rgspnval  20628  staffval  20858  lspfval  20988  lsppropd  21034  sraval  21191  isphl  21663  ocvfval  21701  pjfval  21743  uvcfval  21821  aspval  21910  asclfval  21916  ressascl  21933  psrval  21952  psrass1lem  21969  psrmulval  21981  mvrfval  22018  opsrval  22081  mpfrcl  22126  evlsval  22127  selvffval  22154  mhpmulcl  22170  psdffval  22178  coe1mul2  22287  cply1mul  22315  evls1fval  22338  evl1fval  22347  evl1maprhm  22398  mamufval  22411  mvmulfval  22563  marepvfval  22586  submafval  22600  mdetfval  22607  madufval  22658  minmar1fval  22667  mat2pmatfval  22744  cpm2mfval  22770  decpmatmullem  22792  decpmatmulsumfsupp  22794  pm2mpval  22816  pm2mpmhmlem1  22839  pm2mpmhmlem2  22840  chpmatfval  22851  ntrfval  23047  clsfval  23048  neifval  23122  lpfval  23161  ordtval  23212  ordtbas2  23214  ordtcnv  23224  ordtrest  23225  ordtrest2  23227  cnpfval  23257  kqval  23749  fmval  23966  fmf  23968  flffval  24012  fcfval  24056  cnextval  24084  tsmsval2  24153  nmfval  24616  nmpropd  24622  nmpropd2  24623  subgnm  24661  tngnm  24687  nmofval  24750  pi1xfrcnv  25103  iscph  25217  tcphval  25265  limcfval  25921  dvfval  25946  eldv  25947  mdegfval  26115  mdegmullem  26131  mdegpropd  26137  coe1mul3  26152  ig1pval  26229  taylfval  26414  ishlg  28624  mirval  28677  ishpg  28781  lmif  28807  islmib  28809  vtxdgfval  29499  vtxdeqd  29509  grpoinvfval  30550  nmoofval  30790  eigvalfval  31925  ressnm  32933  tocycval  33110  idlsrgval  33510  minplyval  33712  ordtprsval  33878  ordtprsuni  33879  ordtrestNEW  33881  indv  33992  ofcfval  34078  ofcfval3  34082  omsval  34274  sitgval  34313  issibf  34314  sitgfval  34322  signstfv  34556  cvmliftlem5  35273  cvmliftlem15  35282  mvrsval  35489  mrsubffval  35491  elmrsubrn  35504  msubffval  35507  mvhfval  35517  msrfval  35521  fwddifval  36143  fwddifnval  36144  tailfval  36354  bj-imdirvallem  37162  bj-endval  37297  cureq  37582  lsatset  38971  lkrfval  39068  pmapfval  39738  pclfvalN  39871  polfvalN  39886  watfvalN  39974  ldilfset  40090  ltrnfset  40099  dilfsetN  40134  trnfsetN  40137  trlfset  40142  trlset  40143  tgrpfset  40726  tendofset  40740  erngfset  40781  erngset  40782  erngfset-rN  40789  erngset-rN  40790  dvafset  40986  diaffval  41012  diafval  41013  dvhfset  41062  docaffvalN  41103  docafvalN  41104  djaffvalN  41115  dibffval  41122  dibfval  41123  dicffval  41156  dicfval  41157  dihffval  41212  dochffval  41331  dochfval  41332  djhffval  41378  lcdfval  41570  mapdffval  41608  mapdfval  41609  hvmapffval  41740  hvmapfval  41741  hdmap1ffval  41777  hdmap1fval  41778  hdmapffval  41808  hdmapfval  41809  hgmapffval  41867  hgmapfval  41868  hlhilset  41916  prjcrvfval  42617  hbtlem1  43111  hbtlem7  43113  cytpval  43190  rfovd  43990  fsovd  43997  fsovcnvlem  44002  dssmapfvd  44006  ntrneibex  44062  mnringvald  44203  ovnval  46496  hspmbllem2  46582  smflimsuplem1  46775  smflimsuplem3  46777  smflimsuplem7  46781  smflimsup  46783  ply1mulgsumlem3  48233  ply1mulgsumlem4  48234  ply1mulgsum  48235  lincval  48254