Theorem mpteq12dv 5203

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 2179, ax-12 2216. (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 486	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷)
4	1, 3	mpteq12dva 5202	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146   ↦ cmpt 5197

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-opab 5179  df-mpt 5198

This theorem is used by:  mpteq1  5205  mpteq1i  5207  mpteq12i  5213  ovmpt3rab1  7681  offval  7696  offval3  7988  cantnffval  9642  cnfcomlem  9678  fseqenlem1  10027  dfac12lem1  10146  dfac12r  10149  ackbij2lem2  10241  ackbij2lem3  10242  r1om  10245  indv  12238  ccatfval  14630  swrdval  14703  revval  14821  odzval  16876  vdwpc  17065  restval  17504  prdsval  17533  imasval  17590  qusval  17621  mrcfval  17689  cidfval  17757  monfval  17814  ismon  17815  isepi  17822  idfuval  17958  resfval  17974  resfval2  17975  fucval  18043  homafval  18111  idafval  18139  prfval  18280  prf2fval  18282  curfval  18304  curfpropd  18314  hofval  18333  hof2fval  18336  yonedalem3a  18355  yonedalem4a  18356  yonedalem4c  18358  yonedainv  18362  lubfval  18429  glbfval  18442  ipoval  18611  grpinvfval  19076  grpinvfvalALT  19077  grpinvpropd  19112  mulgnn0gsum  19177  cntzfval  19421  pmtrfval  19551  psgnfval  19601  odfval  19633  odfvalALT  19634  sylow1lem2  19700  sylow1lem4  19702  sylow2blem1  19721  sylow3lem1  19728  sylow3lem2  19729  sylow3lem3  19730  sylow3lem6  19733  pj1fval  19795  vrgpfval  19867  gsum2dlem2  20072  gsum2d2  20075  dprdval  20106  dprd2dlem2  20143  dprd2dlem1  20144  dprd2da  20145  dprd2d2  20147  dpjfval  20158  srgbinom  20344  rgspnval  20748  staffval  20981  lspfval  21131  lsppropd  21176  sraval  21333  isphl  21815  ocvfval  21853  pjfval  21893  uvcfval  21971  aspval  22059  asclfval  22065  ressascl  22083  psrval  22102  psrass1lem  22120  psrmulval  22131  mvrfval  22167  opsrval  22234  mpfrcl  22273  evlsval  22274  selvffval  22306  mhpmulcl  22349  psdffval  22357  coe1mul2  22467  cply1mul  22493  evls1fval  22516  evl1fval  22525  evl1maprhm  22576  mamufval  22586  mvmulfval  22736  marepvfval  22759  submafval  22773  mdetfval  22780  madufval  22831  minmar1fval  22840  mat2pmatfval  22917  cpm2mfval  22943  decpmatmullem  22965  decpmatmulsumfsupp  22967  pm2mpval  22989  pm2mpmhmlem1  23012  pm2mpmhmlem2  23013  chpmatfval  23024  ntrfval  23218  clsfval  23219  neifval  23293  lpfval  23332  ordtval  23383  ordtbas2  23385  ordtcnv  23395  ordtrest  23396  ordtrest2  23398  cnpfval  23428  kqval  23920  fmval  24137  fmf  24139  flffval  24183  fcfval  24227  cnextval  24255  tsmsval2  24324  nmfval  24782  nmpropd  24788  nmpropd2  24789  subgnm  24827  tngnm  24845  nmofval  24908  pi1xfrcnv  25253  iscph  25366  tcphval  25414  limcfval  26068  dvfval  26093  eldv  26094  mdegfval  26256  mdegmullem  26272  mdegpropd  26278  coe1mul3  26293  ig1pval  26370  taylfval  26559  ishlg2  28908  ishlg  28911  mirval  28969  ishpg  29078  lmif  29131  islmib  29133  vtxdgfval  29854  vtxdeqd  29864  grpoinvfval  30911  nmoofval  31151  eigvalfval  32286  ressnm  33315  tocycval  33459  idlsrgval  33824  selvply1rhmlemb  33940  extvval  33952  extvfval  33953  mplvrpmrhm  33968  issply  33982  minplyval  34126  ordtprsval  34339  ordtprsuni  34340  ordtrestNEW  34342  ofcfval  34519  ofcfval3  34523  omsval  34715  sitgval  34754  issibf  34755  sitgfval  34763  signstfv  34982  cvmliftlem5  35802  cvmliftlem15  35811  mvrsval  36018  mrsubffval  36020  elmrsubrn  36033  msubffval  36036  mvhfval  36046  msrfval  36050  fwddifval  36675  fwddifnval  36676  tailfval  36924  bj-imdirvallem  37865  bj-endval  38000  cureq  38288  lsatset  39805  lkrfval  39902  pmapfval  40571  pclfvalN  40704  polfvalN  40719  watfvalN  40807  ldilfset  40923  ltrnfset  40932  dilfsetN  40967  trnfsetN  40970  trlfset  40975  trlset  40976  tgrpfset  41559  tendofset  41573  erngfset  41614  erngset  41615  erngfset-rN  41622  erngset-rN  41623  dvafset  41819  diaffval  41845  diafval  41846  dvhfset  41895  docaffvalN  41936  docafvalN  41937  djaffvalN  41948  dibffval  41955  dibfval  41956  dicffval  41989  dicfval  41990  dihffval  42045  dochffval  42164  dochfval  42165  djhffval  42211  lcdfval  42403  mapdffval  42441  mapdfval  42442  hvmapffval  42573  hvmapfval  42574  hdmap1ffval  42610  hdmap1fval  42611  hdmapffval  42641  hdmapfval  42642  hgmapffval  42700  hgmapfval  42701  hlhilset  42749  prjcrvfval  43404  hbtlem1  43891  hbtlem7  43893  cytpval  43970  rfovd  44768  fsovd  44775  fsovcnvlem  44780  dssmapfvd  44784  ntrneibex  44840  mnringvald  44978  ovnval  47296  hspmbllem2  47382  smflimsuplem1  47575  smflimsuplem3  47577  smflimsuplem7  47581  smflimsup  47583  ply1mulgsumlem3  49209  ply1mulgsumlem4  49210  ply1mulgsum  49211  lincval  49230  iinfprg  49878  fucofvalg  50137  precofval3  50190  prcofvalg  50195  lmdfval  50468  cmdfval  50469