Theorem mpteq12dv 4958

Description: An equality inference for the maps-to notation. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 16-Dec-2013.)

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 474	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷)
4	1, 3	mpteq12dva 4957	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))

Syntax hints:   → wi 4   = wceq 1656   ∈ wcel 2164   ↦ cmpt 4954

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-ral 3122  df-opab 4938  df-mpt 4955

This theorem is referenced by:  mpteq12i  4967  ovmpt3rab1  7156  offval  7169  offval3  7427  cantnffval  8844  cnfcomlem  8880  fseqenlem1  9167  dfac12lem1  9287  dfac12r  9290  ackbij2lem2  9384  ackbij2lem3  9385  r1om  9388  ccatfval  13640  swrdval  13710  revval  13883  odzval  15874  vdwpc  16062  restval  16447  prdsval  16475  imasval  16531  qusval  16562  mrcfval  16628  cidfval  16696  monfval  16751  ismon  16752  isepi  16759  idfuval  16895  resfval  16911  resfval2  16912  fucval  16977  homafval  17038  idafval  17066  prfval  17199  prf2fval  17201  curfval  17223  curfpropd  17233  hofval  17252  hof2fval  17255  yonedalem3a  17274  yonedalem4a  17275  yonedalem4c  17277  yonedainv  17281  lubfval  17338  glbfval  17351  ipoval  17514  grpinvfval  17821  grpinvpropd  17851  cntzfval  18110  pmtrfval  18227  psgnfval  18278  odfval  18310  sylow1lem2  18372  sylow1lem4  18374  sylow2blem1  18393  sylow3lem1  18400  sylow3lem2  18401  sylow3lem3  18402  sylow3lem6  18405  pj1fval  18465  vrgpfval  18539  gsum2dlem2  18730  gsum2d2  18733  dprdval  18763  dprd2dlem2  18800  dprd2dlem1  18801  dprd2da  18802  dprd2d2  18804  dpjfval  18815  srgbinom  18906  staffval  19210  lspfval  19339  lsppropd  19384  sraval  19544  aspval  19696  asclfval  19702  ressascl  19712  psrval  19730  psrass1lem  19745  psrmulval  19754  mvrfval  19788  opsrval  19842  mpfrcl  19885  evlsval  19886  coe1mul2  20006  cply1mul  20031  evls1fval  20051  evl1fval  20059  isphl  20342  ocvfval  20380  pjfval  20420  uvcfval  20497  mamufval  20565  mvmulfval  20723  marepvfval  20746  submafval  20760  mdetfval  20767  madufval  20818  minmar1fval  20827  mat2pmatfval  20905  cpm2mfval  20931  decpmatmullem  20953  decpmatmulsumfsupp  20955  pm2mpval  20977  pm2mpmhmlem1  21000  pm2mpmhmlem2  21001  chpmatfval  21012  ntrfval  21206  clsfval  21207  neifval  21281  lpfval  21320  ordtval  21371  ordtbas2  21373  ordtcnv  21383  ordtrest  21384  ordtrest2  21386  cnpfval  21416  kqval  21907  fmval  22124  fmf  22126  flffval  22170  fcfval  22214  cnextval  22242  tsmsval2  22310  nmfval  22770  nmpropd  22775  nmpropd2  22776  subgnm  22814  tngnm  22832  nmofval  22895  pi1xfrcnv  23233  iscph  23346  tcphval  23393  limcfval  24042  dvfval  24067  eldv  24068  mdegfval  24228  mdegmullem  24244  mdegpropd  24250  coe1mul3  24265  ig1pval  24338  taylfval  24519  ishlg  25921  mirval  25974  ishpg  26075  lmif  26101  islmib  26103  vtxdgfval  26772  vtxdeqd  26782  grpoinvfval  27928  nmoofval  28168  eigvalfval  29307  ressnm  30192  ordtprsval  30505  ordtprsuni  30506  ordtrestNEW  30508  indv  30615  ofcfval  30701  ofcfval3  30705  omsval  30896  sitgval  30935  issibf  30936  sitgfval  30944  signstfv  31183  cvmliftlem5  31813  cvmliftlem15  31822  mvrsval  31944  mrsubffval  31946  elmrsubrn  31959  msubffval  31962  mvhfval  31972  msrfval  31976  fwddifval  32803  fwddifnval  32804  tailfval  32900  cureq  33927  lsatset  35064  lkrfval  35161  pmapfval  35830  pclfvalN  35963  polfvalN  35978  watfvalN  36066  ldilfset  36182  ltrnfset  36191  dilfsetN  36226  trnfsetN  36229  trlfset  36234  trlset  36235  tgrpfset  36818  tendofset  36832  erngfset  36873  erngset  36874  erngfset-rN  36881  erngset-rN  36882  dvafset  37078  diaffval  37104  diafval  37105  dvhfset  37154  docaffvalN  37195  docafvalN  37196  djaffvalN  37207  dibffval  37214  dibfval  37215  dicffval  37248  dicfval  37249  dihffval  37304  dochffval  37423  dochfval  37424  djhffval  37470  lcdfval  37662  mapdffval  37700  mapdfval  37701  hvmapffval  37832  hvmapfval  37833  hdmap1ffval  37869  hdmap1fval  37870  hdmapffval  37900  hdmapfval  37901  hgmapffval  37959  hgmapfval  37960  hlhilset  38008  hbtlem1  38535  hbtlem7  38537  rgspnval  38580  cytpval  38629  rfovd  39134  fsovd  39141  fsovcnvlem  39146  dssmapfvd  39150  ntrneibex  39210  ovnval  41547  hspmbllem2  41633  smflimsuplem1  41818  smflimsuplem3  41820  smflimsuplem7  41824  smflimsup  41826  ply1mulgsumlem3  43041  ply1mulgsumlem4  43042  ply1mulgsum  43043  lincval  43063  offval0  43164