Theorem mpteq12dv 5199

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 2176, ax-12 2213. (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 485	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷)
4	1, 3	mpteq12dva 5198	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143   ↦ cmpt 5193

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-opab 5175  df-mpt 5194

This theorem is referenced by:  mpteq1  5201  mpteq1i  5203  mpteq12i  5209  ovmpt3rab1  7670  offval  7685  offval3  7980  cantnffval  9633  cnfcomlem  9669  fseqenlem1  10009  dfac12lem1  10128  dfac12r  10131  ackbij2lem2  10223  ackbij2lem3  10224  r1om  10227  indv  12221  ccatfval  14612  swrdval  14683  revval  14799  odzval  16852  vdwpc  17041  restval  17480  prdsval  17509  imasval  17566  qusval  17597  mrcfval  17665  cidfval  17733  monfval  17790  ismon  17791  isepi  17798  idfuval  17934  resfval  17950  resfval2  17951  fucval  18019  homafval  18087  idafval  18115  prfval  18256  prf2fval  18258  curfval  18280  curfpropd  18290  hofval  18309  hof2fval  18312  yonedalem3a  18331  yonedalem4a  18332  yonedalem4c  18334  yonedainv  18338  lubfval  18405  glbfval  18418  ipoval  18587  grpinvfval  19046  grpinvfvalALT  19047  grpinvpropd  19082  mulgnn0gsum  19147  cntzfval  19391  pmtrfval  19521  psgnfval  19571  odfval  19603  odfvalALT  19604  sylow1lem2  19670  sylow1lem4  19672  sylow2blem1  19691  sylow3lem1  19698  sylow3lem2  19699  sylow3lem3  19700  sylow3lem6  19703  pj1fval  19765  vrgpfval  19837  gsum2dlem2  20042  gsum2d2  20045  dprdval  20076  dprd2dlem2  20113  dprd2dlem1  20114  dprd2da  20115  dprd2d2  20117  dpjfval  20128  srgbinom  20314  rgspnval  20698  staffval  20925  lspfval  21075  lsppropd  21120  sraval  21277  isphl  21759  ocvfval  21797  pjfval  21837  uvcfval  21915  aspval  22003  asclfval  22009  ressascl  22027  psrval  22046  psrass1lem  22064  psrmulval  22075  mvrfval  22111  opsrval  22178  mpfrcl  22217  evlsval  22218  selvffval  22250  mhpmulcl  22293  psdffval  22301  coe1mul2  22411  cply1mul  22437  evls1fval  22460  evl1fval  22469  evl1maprhm  22520  mamufval  22530  mvmulfval  22680  marepvfval  22703  submafval  22717  mdetfval  22724  madufval  22775  minmar1fval  22784  mat2pmatfval  22861  cpm2mfval  22887  decpmatmullem  22909  decpmatmulsumfsupp  22911  pm2mpval  22933  pm2mpmhmlem1  22956  pm2mpmhmlem2  22957  chpmatfval  22968  ntrfval  23162  clsfval  23163  neifval  23237  lpfval  23276  ordtval  23327  ordtbas2  23329  ordtcnv  23339  ordtrest  23340  ordtrest2  23342  cnpfval  23372  kqval  23864  fmval  24081  fmf  24083  flffval  24127  fcfval  24171  cnextval  24199  tsmsval2  24268  nmfval  24726  nmpropd  24732  nmpropd2  24733  subgnm  24771  tngnm  24789  nmofval  24852  pi1xfrcnv  25197  iscph  25310  tcphval  25358  limcfval  26012  dvfval  26037  eldv  26038  mdegfval  26200  mdegmullem  26216  mdegpropd  26222  coe1mul3  26237  ig1pval  26314  taylfval  26503  ishlg2  28852  ishlg  28855  mirval  28913  ishpg  29022  lmif  29075  islmib  29077  vtxdgfval  29798  vtxdeqd  29808  grpoinvfval  30855  nmoofval  31095  eigvalfval  32230  ressnm  33265  tocycval  33409  idlsrgval  33774  selvply1rhmlemb  33890  extvval  33902  extvfval  33903  mplvrpmrhm  33918  issply  33932  minplyval  34076  ordtprsval  34289  ordtprsuni  34290  ordtrestNEW  34292  ofcfval  34469  ofcfval3  34473  omsval  34664  sitgval  34703  issibf  34704  sitgfval  34712  signstfv  34931  cvmliftlem5  35762  cvmliftlem15  35771  mvrsval  35978  mrsubffval  35980  elmrsubrn  35993  msubffval  35996  mvhfval  36006  msrfval  36010  fwddifval  36635  fwddifnval  36636  tailfval  36864  bj-imdirvallem  37805  bj-endval  37940  cureq  38228  lsatset  39745  lkrfval  39842  pmapfval  40511  pclfvalN  40644  polfvalN  40659  watfvalN  40747  ldilfset  40863  ltrnfset  40872  dilfsetN  40907  trnfsetN  40910  trlfset  40915  trlset  40916  tgrpfset  41499  tendofset  41513  erngfset  41554  erngset  41555  erngfset-rN  41562  erngset-rN  41563  dvafset  41759  diaffval  41785  diafval  41786  dvhfset  41835  docaffvalN  41876  docafvalN  41877  djaffvalN  41888  dibffval  41895  dibfval  41896  dicffval  41929  dicfval  41930  dihffval  41985  dochffval  42104  dochfval  42105  djhffval  42151  lcdfval  42343  mapdffval  42381  mapdfval  42382  hvmapffval  42513  hvmapfval  42514  hdmap1ffval  42550  hdmap1fval  42551  hdmapffval  42581  hdmapfval  42582  hgmapffval  42640  hgmapfval  42641  hlhilset  42689  prjcrvfval  43346  hbtlem1  43833  hbtlem7  43835  cytpval  43912  rfovd  44710  fsovd  44717  fsovcnvlem  44722  dssmapfvd  44726  ntrneibex  44782  mnringvald  44920  ovnval  47238  hspmbllem2  47324  smflimsuplem1  47517  smflimsuplem3  47519  smflimsuplem7  47523  smflimsup  47525  ply1mulgsumlem3  49151  ply1mulgsumlem4  49152  ply1mulgsum  49153  lincval  49172  iinfprg  49820  fucofvalg  50079  precofval3  50132  prcofvalg  50137  lmdfval  50410  cmdfval  50411