Theorem mpteq12dv 5166

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 2152, ax-12 2189. (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 481	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷)
4	1, 3	mpteq12dva 5165	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119   ↦ cmpt 5160

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-opab 5142  df-mpt 5161

This theorem is referenced by:  mpteq1  5168  mpteq1i  5170  mpteq12i  5176  ovmpt3rab1  7621  offval  7636  offval3  7931  cantnffval  9582  cnfcomlem  9618  fseqenlem1  9944  dfac12lem1  10064  dfac12r  10067  ackbij2lem2  10159  ackbij2lem3  10160  r1om  10163  indv  12159  ccatfval  14533  swrdval  14604  revval  14720  odzval  16760  vdwpc  16949  restval  17387  prdsval  17416  imasval  17473  qusval  17504  mrcfval  17572  cidfval  17640  monfval  17697  ismon  17698  isepi  17705  idfuval  17841  resfval  17857  resfval2  17858  fucval  17926  homafval  17994  idafval  18022  prfval  18163  prf2fval  18165  curfval  18187  curfpropd  18197  hofval  18216  hof2fval  18219  yonedalem3a  18238  yonedalem4a  18239  yonedalem4c  18241  yonedainv  18245  lubfval  18312  glbfval  18325  ipoval  18494  grpinvfval  18952  grpinvfvalALT  18953  grpinvpropd  18989  mulgnn0gsum  19054  cntzfval  19293  pmtrfval  19423  psgnfval  19473  odfval  19505  odfvalALT  19506  sylow1lem2  19572  sylow1lem4  19574  sylow2blem1  19593  sylow3lem1  19600  sylow3lem2  19601  sylow3lem3  19602  sylow3lem6  19605  pj1fval  19667  vrgpfval  19739  gsum2dlem2  19944  gsum2d2  19947  dprdval  19978  dprd2dlem2  20015  dprd2dlem1  20016  dprd2da  20017  dprd2d2  20019  dpjfval  20030  srgbinom  20210  rgspnval  20591  staffval  20820  lspfval  20970  lsppropd  21015  sraval  21172  isphl  21610  ocvfval  21648  pjfval  21688  uvcfval  21766  aspval  21854  asclfval  21860  ressascl  21878  psrval  21897  psrass1lem  21915  psrmulval  21926  mvrfval  21962  opsrval  22029  mpfrcl  22068  evlsval  22069  selvffval  22101  mhpmulcl  22144  psdffval  22152  coe1mul2  22262  cply1mul  22289  evls1fval  22312  evl1fval  22321  evl1maprhm  22372  mamufval  22382  mvmulfval  22532  marepvfval  22555  submafval  22569  mdetfval  22576  madufval  22627  minmar1fval  22636  mat2pmatfval  22713  cpm2mfval  22739  decpmatmullem  22761  decpmatmulsumfsupp  22763  pm2mpval  22785  pm2mpmhmlem1  22808  pm2mpmhmlem2  22809  chpmatfval  22820  ntrfval  23014  clsfval  23015  neifval  23089  lpfval  23128  ordtval  23179  ordtbas2  23181  ordtcnv  23191  ordtrest  23192  ordtrest2  23194  cnpfval  23224  kqval  23716  fmval  23933  fmf  23935  flffval  23979  fcfval  24023  cnextval  24051  tsmsval2  24120  nmfval  24578  nmpropd  24584  nmpropd2  24585  subgnm  24623  tngnm  24641  nmofval  24704  pi1xfrcnv  25049  iscph  25162  tcphval  25210  limcfval  25864  dvfval  25889  eldv  25890  mdegfval  26052  mdegmullem  26068  mdegpropd  26074  coe1mul3  26089  ig1pval  26166  taylfval  26349  ishlg  28695  mirval  28748  ishpg  28852  lmif  28878  islmib  28880  vtxdgfval  29561  vtxdeqd  29571  grpoinvfval  30618  nmoofval  30858  eigvalfval  31993  ressnm  33050  tocycval  33196  idlsrgval  33593  selvply1rhmlemb  33710  extvval  33722  extvfval  33723  mplvrpmrhm  33738  issply  33752  minplyval  33896  ordtprsval  34109  ordtprsuni  34110  ordtrestNEW  34112  ofcfval  34289  ofcfval3  34293  omsval  34484  sitgval  34523  issibf  34524  sitgfval  34532  signstfv  34754  cvmliftlem5  35524  cvmliftlem15  35533  mvrsval  35740  mrsubffval  35742  elmrsubrn  35755  msubffval  35758  mvhfval  35768  msrfval  35772  fwddifval  36397  fwddifnval  36398  tailfval  36607  bj-imdirvallem  37547  bj-endval  37682  cureq  37970  lsatset  39489  lkrfval  39586  pmapfval  40255  pclfvalN  40388  polfvalN  40403  watfvalN  40491  ldilfset  40607  ltrnfset  40616  dilfsetN  40651  trnfsetN  40654  trlfset  40659  trlset  40660  tgrpfset  41243  tendofset  41257  erngfset  41298  erngset  41299  erngfset-rN  41306  erngset-rN  41307  dvafset  41503  diaffval  41529  diafval  41530  dvhfset  41579  docaffvalN  41620  docafvalN  41621  djaffvalN  41632  dibffval  41639  dibfval  41640  dicffval  41673  dicfval  41674  dihffval  41729  dochffval  41848  dochfval  41849  djhffval  41895  lcdfval  42087  mapdffval  42125  mapdfval  42126  hvmapffval  42257  hvmapfval  42258  hdmap1ffval  42294  hdmap1fval  42295  hdmapffval  42325  hdmapfval  42326  hgmapffval  42384  hgmapfval  42385  hlhilset  42433  prjcrvfval  43088  hbtlem1  43575  hbtlem7  43577  cytpval  43654  rfovd  44452  fsovd  44459  fsovcnvlem  44464  dssmapfvd  44468  ntrneibex  44524  mnringvald  44664  ovnval  46991  hspmbllem2  47077  smflimsuplem1  47270  smflimsuplem3  47272  smflimsuplem7  47276  smflimsup  47278  ply1mulgsumlem3  48886  ply1mulgsumlem4  48887  ply1mulgsum  48888  lincval  48907  iinfprg  49556  fucofvalg  49815  precofval3  49868  prcofvalg  49873  lmdfval  50146  cmdfval  50147