Theorem mpteq12dv 4663

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

Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977   ↦ cmpt 4643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-ral 2901  df-opab 4644  df-mpt 4645

This theorem is referenced by:  mpteq12i  4670  ovmpt3rab1  6789  offval  6802  offval3  7053  cantnffval  8443  cnfcomlem  8479  fseqenlem1  8730  dfac12lem1  8848  dfac12r  8851  ackbij2lem2  8945  ackbij2lem3  8946  r1om  8949  ccatfval  13211  swrdval  13269  revval  13360  odzval  15334  vdwpc  15522  restval  15910  prdsval  15938  imasval  15994  qusval  16025  mrcfval  16091  cidfval  16160  monfval  16215  ismon  16216  isepi  16223  idfuval  16359  resfval  16375  resfval2  16376  fucval  16441  homafval  16502  idafval  16530  prfval  16662  prf2fval  16664  curfval  16686  curfpropd  16696  hofval  16715  hof2fval  16718  yonedalem3a  16737  yonedalem4a  16738  yonedalem4c  16740  yonedainv  16744  lubfval  16801  glbfval  16814  ipoval  16977  grpinvfval  17283  grpinvpropd  17313  cntzfval  17576  pmtrfval  17693  psgnfval  17743  odfval  17775  sylow1lem2  17837  sylow1lem4  17839  sylow2blem1  17858  sylow3lem1  17865  sylow3lem2  17866  sylow3lem3  17867  sylow3lem6  17870  pj1fval  17930  vrgpfval  18002  gsum2dlem2  18193  gsum2d2  18196  dprdval  18225  dprd2dlem2  18262  dprd2dlem1  18263  dprd2da  18264  dprd2d2  18266  dpjfval  18277  srgbinom  18368  staffval  18670  lspfval  18794  lsppropd  18839  sraval  18997  aspval  19149  asclfval  19155  ressascl  19165  psrval  19183  psrass1lem  19198  psrmulval  19207  mvrfval  19241  opsrval  19295  mpfrcl  19339  evlsval  19340  coe1mul2  19460  cply1mul  19485  evls1fval  19505  evl1fval  19513  isphl  19792  ocvfval  19829  pjfval  19869  uvcfval  19942  mamufval  20010  mvmulfval  20167  marepvfval  20190  submafval  20204  mdetfval  20211  madufval  20262  minmar1fval  20271  mat2pmatfval  20347  cpm2mfval  20373  decpmatmullem  20395  decpmatmulsumfsupp  20397  pm2mpval  20419  pm2mpmhmlem1  20442  pm2mpmhmlem2  20443  chpmatfval  20454  ntrfval  20638  clsfval  20639  neifval  20713  lpfval  20752  ordtval  20803  ordtbas2  20805  ordtcnv  20815  ordtrest  20816  ordtrest2  20818  cnpfval  20848  kqval  21339  fmval  21557  fmf  21559  flffval  21603  fcfval  21647  cnextval  21675  tsmsval2  21743  nmfval  22203  nmpropd  22208  nmpropd2  22209  subgnm  22247  tngnm  22265  nmofval  22328  pi1xfrcnv  22665  iscph  22778  tchval  22825  limcfval  23442  dvfval  23467  eldv  23468  mdegfval  23626  mdegmullem  23642  mdegpropd  23648  coe1mul3  23663  ig1pval  23736  taylfval  23917  ishlg  25297  mirval  25350  ishpg  25451  lmif  25477  islmib  25479  vdgrfval  26422  grpoinvfval  26760  nmoofval  27001  eigvalfval  28140  ressnm  28982  ordtprsval  29292  ordtprsuni  29293  ordtrestNEW  29295  indv  29402  ofcfval  29487  ofcfval3  29491  omsval  29682  sitgval  29721  issibf  29722  sitgfval  29730  signstfv  29966  cvmliftlem5  30525  cvmliftlem15  30534  mvrsval  30656  mrsubffval  30658  elmrsubrn  30671  msubffval  30674  mvhfval  30684  msrfval  30688  fwddifval  31439  fwddifnval  31440  tailfval  31537  cureq  32555  lsatset  33295  lkrfval  33392  pmapfval  34060  pclfvalN  34193  polfvalN  34208  watfvalN  34296  ldilfset  34412  ltrnfset  34421  dilfsetN  34457  trnfsetN  34460  trlfset  34465  trlset  34466  tgrpfset  35050  tendofset  35064  erngfset  35105  erngset  35106  erngfset-rN  35113  erngset-rN  35114  dvafset  35310  diaffval  35337  diafval  35338  dvhfset  35387  docaffvalN  35428  docafvalN  35429  djaffvalN  35440  dibffval  35447  dibfval  35448  dicffval  35481  dicfval  35482  dihffval  35537  dochffval  35656  dochfval  35657  djhffval  35703  lcdfval  35895  mapdffval  35933  mapdfval  35934  hvmapffval  36065  hvmapfval  36066  hdmap1ffval  36103  hdmap1fval  36104  hdmapffval  36136  hdmapfval  36137  hgmapffval  36195  hgmapfval  36196  hlhilset  36244  hbtlem1  36712  hbtlem7  36714  rgspnval  36757  cytpval  36806  rfovd  37315  fsovd  37322  fsovcnvlem  37327  dssmapfvd  37331  ntrneibex  37391  ovnval  39431  hspmbllem2  39517  vtxdgfval  40683  vtxdeqd  40692  ply1mulgsumlem3  41970  ply1mulgsumlem4  41971  ply1mulgsum  41972  lincval  41992  offval0  42093