Theorem mpteq12dv 4925

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

Syntax hints:   → wi 4   = wceq 1637   ∈ wcel 2156   ↦ cmpt 4921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-ext 2782

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2791  df-cleq 2797  df-clel 2800  df-ral 3099  df-opab 4905  df-mpt 4922

This theorem is referenced by:  mpteq12i  4934  ovmpt3rab1  7119  offval  7132  offval3  7390  cantnffval  8805  cnfcomlem  8841  fseqenlem1  9128  dfac12lem1  9248  dfac12r  9251  ackbij2lem2  9345  ackbij2lem3  9346  r1om  9349  ccatfval  13568  swrdval  13638  revval  13731  odzval  15711  vdwpc  15899  restval  16290  prdsval  16318  imasval  16374  qusval  16405  mrcfval  16471  cidfval  16539  monfval  16594  ismon  16595  isepi  16602  idfuval  16738  resfval  16754  resfval2  16755  fucval  16820  homafval  16881  idafval  16909  prfval  17042  prf2fval  17044  curfval  17066  curfpropd  17076  hofval  17095  hof2fval  17098  yonedalem3a  17117  yonedalem4a  17118  yonedalem4c  17120  yonedainv  17124  lubfval  17181  glbfval  17194  ipoval  17357  grpinvfval  17663  grpinvpropd  17693  cntzfval  17952  pmtrfval  18069  psgnfval  18119  odfval  18151  sylow1lem2  18213  sylow1lem4  18215  sylow2blem1  18234  sylow3lem1  18241  sylow3lem2  18242  sylow3lem3  18243  sylow3lem6  18246  pj1fval  18306  vrgpfval  18378  gsum2dlem2  18569  gsum2d2  18572  dprdval  18602  dprd2dlem2  18639  dprd2dlem1  18640  dprd2da  18641  dprd2d2  18643  dpjfval  18654  srgbinom  18745  staffval  19049  lspfval  19178  lsppropd  19223  sraval  19383  aspval  19535  asclfval  19541  ressascl  19551  psrval  19569  psrass1lem  19584  psrmulval  19593  mvrfval  19627  opsrval  19681  mpfrcl  19724  evlsval  19725  coe1mul2  19845  cply1mul  19870  evls1fval  19890  evl1fval  19898  isphl  20181  ocvfval  20218  pjfval  20258  uvcfval  20331  mamufval  20399  mvmulfval  20557  marepvfval  20580  submafval  20594  mdetfval  20601  madufval  20652  minmar1fval  20661  mat2pmatfval  20739  cpm2mfval  20765  decpmatmullem  20787  decpmatmulsumfsupp  20789  pm2mpval  20811  pm2mpmhmlem1  20834  pm2mpmhmlem2  20835  chpmatfval  20846  ntrfval  21040  clsfval  21041  neifval  21115  lpfval  21154  ordtval  21205  ordtbas2  21207  ordtcnv  21217  ordtrest  21218  ordtrest2  21220  cnpfval  21250  kqval  21741  fmval  21958  fmf  21960  flffval  22004  fcfval  22048  cnextval  22076  tsmsval2  22144  nmfval  22604  nmpropd  22609  nmpropd2  22610  subgnm  22648  tngnm  22666  nmofval  22729  pi1xfrcnv  23067  iscph  23180  tchval  23227  limcfval  23848  dvfval  23873  eldv  23874  mdegfval  24034  mdegmullem  24050  mdegpropd  24056  coe1mul3  24071  ig1pval  24144  taylfval  24325  ishlg  25709  mirval  25762  ishpg  25863  lmif  25889  islmib  25891  vtxdgfval  26589  vtxdeqd  26599  grpoinvfval  27703  nmoofval  27943  eigvalfval  29082  ressnm  29974  ordtprsval  30287  ordtprsuni  30288  ordtrestNEW  30290  indv  30397  ofcfval  30483  ofcfval3  30487  omsval  30678  sitgval  30717  issibf  30718  sitgfval  30726  signstfv  30963  cvmliftlem5  31592  cvmliftlem15  31601  mvrsval  31723  mrsubffval  31725  elmrsubrn  31738  msubffval  31741  mvhfval  31751  msrfval  31755  fwddifval  32588  fwddifnval  32589  tailfval  32686  cureq  33696  lsatset  34768  lkrfval  34865  pmapfval  35534  pclfvalN  35667  polfvalN  35682  watfvalN  35770  ldilfset  35886  ltrnfset  35895  dilfsetN  35931  trnfsetN  35934  trlfset  35939  trlset  35940  tgrpfset  36523  tendofset  36537  erngfset  36578  erngset  36579  erngfset-rN  36586  erngset-rN  36587  dvafset  36783  diaffval  36809  diafval  36810  dvhfset  36859  docaffvalN  36900  docafvalN  36901  djaffvalN  36912  dibffval  36919  dibfval  36920  dicffval  36953  dicfval  36954  dihffval  37009  dochffval  37128  dochfval  37129  djhffval  37175  lcdfval  37367  mapdffval  37405  mapdfval  37406  hvmapffval  37537  hvmapfval  37538  hdmap1ffval  37574  hdmap1fval  37575  hdmapffval  37605  hdmapfval  37606  hgmapffval  37664  hgmapfval  37665  hlhilset  37713  hbtlem1  38192  hbtlem7  38194  rgspnval  38237  cytpval  38286  rfovd  38793  fsovd  38800  fsovcnvlem  38805  dssmapfvd  38809  ntrneibex  38869  ovnval  41235  hspmbllem2  41321  smflimsuplem1  41506  smflimsuplem3  41508  smflimsuplem7  41512  smflimsup  41514  ply1mulgsumlem3  42742  ply1mulgsumlem4  42743  ply1mulgsum  42744  lincval  42764  offval0  42865