Theorem mpteq12dv 5239

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 2137, ax-12 2171. (Revised by SN and Gino Giotto, 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 481	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷)
4	1, 3	mpteq12dva 5237	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106   ↦ cmpt 5231

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-opab 5211  df-mpt 5232

This theorem is referenced by:  mpteq1  5241  mpteq1i  5244  mpteq12i  5254  ovmpt3rab1  7666  offval  7681  offval3  7971  cantnffval  9660  cnfcomlem  9696  fseqenlem1  10021  dfac12lem1  10140  dfac12r  10143  ackbij2lem2  10237  ackbij2lem3  10238  r1om  10241  ccatfval  14525  swrdval  14595  revval  14712  odzval  16726  vdwpc  16915  restval  17374  prdsval  17403  imasval  17459  qusval  17490  mrcfval  17554  cidfval  17622  monfval  17681  ismon  17682  isepi  17689  idfuval  17828  resfval  17844  resfval2  17845  fucval  17912  homafval  17981  idafval  18009  prfval  18153  prf2fval  18155  curfval  18178  curfpropd  18188  hofval  18207  hof2fval  18210  yonedalem3a  18229  yonedalem4a  18230  yonedalem4c  18232  yonedainv  18236  lubfval  18305  glbfval  18318  ipoval  18485  grpinvfval  18865  grpinvfvalALT  18866  grpinvpropd  18900  mulgnn0gsum  18962  cntzfval  19186  pmtrfval  19320  psgnfval  19370  odfval  19402  odfvalALT  19403  sylow1lem2  19469  sylow1lem4  19471  sylow2blem1  19490  sylow3lem1  19497  sylow3lem2  19498  sylow3lem3  19499  sylow3lem6  19502  pj1fval  19564  vrgpfval  19636  gsum2dlem2  19841  gsum2d2  19844  dprdval  19875  dprd2dlem2  19912  dprd2dlem1  19913  dprd2da  19914  dprd2d2  19916  dpjfval  19927  srgbinom  20056  staffval  20459  lspfval  20589  lsppropd  20634  sraval  20795  isphl  21187  ocvfval  21225  pjfval  21267  uvcfval  21345  aspval  21433  asclfval  21439  ressascl  21456  psrval  21474  psrass1lemOLD  21499  psrass1lem  21502  psrmulval  21511  mvrfval  21546  opsrval  21607  mpfrcl  21654  evlsval  21655  selvffval  21685  mhpmulcl  21698  coe1mul2  21798  cply1mul  21825  evls1fval  21845  evl1fval  21854  mamufval  21894  mvmulfval  22051  marepvfval  22074  submafval  22088  mdetfval  22095  madufval  22146  minmar1fval  22155  mat2pmatfval  22232  cpm2mfval  22258  decpmatmullem  22280  decpmatmulsumfsupp  22282  pm2mpval  22304  pm2mpmhmlem1  22327  pm2mpmhmlem2  22328  chpmatfval  22339  ntrfval  22535  clsfval  22536  neifval  22610  lpfval  22649  ordtval  22700  ordtbas2  22702  ordtcnv  22712  ordtrest  22713  ordtrest2  22715  cnpfval  22745  kqval  23237  fmval  23454  fmf  23456  flffval  23500  fcfval  23544  cnextval  23572  tsmsval2  23641  nmfval  24104  nmpropd  24110  nmpropd2  24111  subgnm  24149  tngnm  24175  nmofval  24238  pi1xfrcnv  24580  iscph  24694  tcphval  24742  limcfval  25396  dvfval  25421  eldv  25422  mdegfval  25587  mdegmullem  25603  mdegpropd  25609  coe1mul3  25624  ig1pval  25697  taylfval  25878  ishlg  27891  mirval  27944  ishpg  28048  lmif  28074  islmib  28076  vtxdgfval  28762  vtxdeqd  28772  grpoinvfval  29813  nmoofval  30053  eigvalfval  31188  ressnm  32166  tocycval  32308  idlsrgval  32662  minplyval  32826  ordtprsval  32967  ordtprsuni  32968  ordtrestNEW  32970  indv  33079  ofcfval  33165  ofcfval3  33169  omsval  33361  sitgval  33400  issibf  33401  sitgfval  33409  signstfv  33643  cvmliftlem5  34349  cvmliftlem15  34358  mvrsval  34565  mrsubffval  34567  elmrsubrn  34580  msubffval  34583  mvhfval  34593  msrfval  34597  fwddifval  35203  fwddifnval  35204  tailfval  35343  bj-imdirvallem  36147  bj-endval  36282  cureq  36550  lsatset  37946  lkrfval  38043  pmapfval  38713  pclfvalN  38846  polfvalN  38861  watfvalN  38949  ldilfset  39065  ltrnfset  39074  dilfsetN  39109  trnfsetN  39112  trlfset  39117  trlset  39118  tgrpfset  39701  tendofset  39715  erngfset  39756  erngset  39757  erngfset-rN  39764  erngset-rN  39765  dvafset  39961  diaffval  39987  diafval  39988  dvhfset  40037  docaffvalN  40078  docafvalN  40079  djaffvalN  40090  dibffval  40097  dibfval  40098  dicffval  40131  dicfval  40132  dihffval  40187  dochffval  40306  dochfval  40307  djhffval  40353  lcdfval  40545  mapdffval  40583  mapdfval  40584  hvmapffval  40715  hvmapfval  40716  hdmap1ffval  40752  hdmap1fval  40753  hdmapffval  40783  hdmapfval  40784  hgmapffval  40842  hgmapfval  40843  hlhilset  40891  prjcrvfval  41455  hbtlem1  41947  hbtlem7  41949  rgspnval  41992  cytpval  42033  rfovd  42834  fsovd  42841  fsovcnvlem  42846  dssmapfvd  42850  ntrneibex  42906  mnringvald  43049  ovnval  45336  hspmbllem2  45422  smflimsuplem1  45615  smflimsuplem3  45617  smflimsuplem7  45621  smflimsup  45623  ply1mulgsumlem3  47147  ply1mulgsumlem4  47148  ply1mulgsum  47149  lincval  47168