Theorem mpteq12dv 5178

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 2144, ax-12 2180. (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 5177	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111   ↦ cmpt 5172

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-opab 5154  df-mpt 5173

This theorem is referenced by:  mpteq1  5180  mpteq1i  5182  mpteq12i  5188  ovmpt3rab1  7604  offval  7619  offval3  7914  cantnffval  9553  cnfcomlem  9589  fseqenlem1  9912  dfac12lem1  10032  dfac12r  10035  ackbij2lem2  10127  ackbij2lem3  10128  r1om  10131  ccatfval  14477  swrdval  14548  revval  14664  odzval  16700  vdwpc  16889  restval  17327  prdsval  17356  imasval  17412  qusval  17443  mrcfval  17511  cidfval  17579  monfval  17636  ismon  17637  isepi  17644  idfuval  17780  resfval  17796  resfval2  17797  fucval  17865  homafval  17933  idafval  17961  prfval  18102  prf2fval  18104  curfval  18126  curfpropd  18136  hofval  18155  hof2fval  18158  yonedalem3a  18177  yonedalem4a  18178  yonedalem4c  18180  yonedainv  18184  lubfval  18251  glbfval  18264  ipoval  18433  grpinvfval  18888  grpinvfvalALT  18889  grpinvpropd  18925  mulgnn0gsum  18990  cntzfval  19230  pmtrfval  19360  psgnfval  19410  odfval  19442  odfvalALT  19443  sylow1lem2  19509  sylow1lem4  19511  sylow2blem1  19530  sylow3lem1  19537  sylow3lem2  19538  sylow3lem3  19539  sylow3lem6  19542  pj1fval  19604  vrgpfval  19676  gsum2dlem2  19881  gsum2d2  19884  dprdval  19915  dprd2dlem2  19952  dprd2dlem1  19953  dprd2da  19954  dprd2d2  19956  dpjfval  19967  srgbinom  20147  rgspnval  20525  staffval  20754  lspfval  20904  lsppropd  20950  sraval  21107  isphl  21563  ocvfval  21601  pjfval  21641  uvcfval  21719  aspval  21808  asclfval  21814  ressascl  21831  psrval  21850  psrass1lem  21867  psrmulval  21879  mvrfval  21916  opsrval  21979  mpfrcl  22018  evlsval  22019  selvffval  22046  mhpmulcl  22062  psdffval  22070  coe1mul2  22181  cply1mul  22209  evls1fval  22232  evl1fval  22241  evl1maprhm  22292  mamufval  22305  mvmulfval  22455  marepvfval  22478  submafval  22492  mdetfval  22499  madufval  22550  minmar1fval  22559  mat2pmatfval  22636  cpm2mfval  22662  decpmatmullem  22684  decpmatmulsumfsupp  22686  pm2mpval  22708  pm2mpmhmlem1  22731  pm2mpmhmlem2  22732  chpmatfval  22743  ntrfval  22937  clsfval  22938  neifval  23012  lpfval  23051  ordtval  23102  ordtbas2  23104  ordtcnv  23114  ordtrest  23115  ordtrest2  23117  cnpfval  23147  kqval  23639  fmval  23856  fmf  23858  flffval  23902  fcfval  23946  cnextval  23974  tsmsval2  24043  nmfval  24501  nmpropd  24507  nmpropd2  24508  subgnm  24546  tngnm  24564  nmofval  24627  pi1xfrcnv  24982  iscph  25095  tcphval  25143  limcfval  25798  dvfval  25823  eldv  25824  mdegfval  25992  mdegmullem  26008  mdegpropd  26014  coe1mul3  26029  ig1pval  26106  taylfval  26291  ishlg  28578  mirval  28631  ishpg  28735  lmif  28761  islmib  28763  vtxdgfval  29444  vtxdeqd  29454  grpoinvfval  30497  nmoofval  30737  eigvalfval  31872  indv  32828  ressnm  32940  tocycval  33072  idlsrgval  33463  mplvrpmrhm  33572  issply  33579  minplyval  33713  ordtprsval  33926  ordtprsuni  33927  ordtrestNEW  33929  ofcfval  34106  ofcfval3  34110  omsval  34301  sitgval  34340  issibf  34341  sitgfval  34349  signstfv  34571  cvmliftlem5  35321  cvmliftlem15  35330  mvrsval  35537  mrsubffval  35539  elmrsubrn  35552  msubffval  35555  mvhfval  35565  msrfval  35569  fwddifval  36195  fwddifnval  36196  tailfval  36405  bj-imdirvallem  37213  bj-endval  37348  cureq  37635  lsatset  39028  lkrfval  39125  pmapfval  39794  pclfvalN  39927  polfvalN  39942  watfvalN  40030  ldilfset  40146  ltrnfset  40155  dilfsetN  40190  trnfsetN  40193  trlfset  40198  trlset  40199  tgrpfset  40782  tendofset  40796  erngfset  40837  erngset  40838  erngfset-rN  40845  erngset-rN  40846  dvafset  41042  diaffval  41068  diafval  41069  dvhfset  41118  docaffvalN  41159  docafvalN  41160  djaffvalN  41171  dibffval  41178  dibfval  41179  dicffval  41212  dicfval  41213  dihffval  41268  dochffval  41387  dochfval  41388  djhffval  41434  lcdfval  41626  mapdffval  41664  mapdfval  41665  hvmapffval  41796  hvmapfval  41797  hdmap1ffval  41833  hdmap1fval  41834  hdmapffval  41864  hdmapfval  41865  hgmapffval  41923  hgmapfval  41924  hlhilset  41972  prjcrvfval  42663  hbtlem1  43155  hbtlem7  43157  cytpval  43234  rfovd  44033  fsovd  44040  fsovcnvlem  44045  dssmapfvd  44049  ntrneibex  44105  mnringvald  44245  ovnval  46578  hspmbllem2  46664  smflimsuplem1  46857  smflimsuplem3  46859  smflimsuplem7  46863  smflimsup  46865  ply1mulgsumlem3  48419  ply1mulgsumlem4  48420  ply1mulgsum  48421  lincval  48440  iinfprg  49090  fucofvalg  49349  precofval3  49402  prcofvalg  49407  lmdfval  49680  cmdfval  49681