Theorem mpteq12dv 4733

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	|- ( ph -> A = C )
mpteq12dv.2	|- ( ph -> B = D )

Assertion

Ref	Expression
mpteq12dv	|- ( ph -> ( x e. A |-> B ) = ( x e. C |-> D ) )

Distinct variable group:   ph, x

Allowed substitution hints:   A( x)   B( x)   C( x)   D( x)

Proof of Theorem mpteq12dv

Step	Hyp	Ref	Expression
1		mpteq12dv.1	. 2 |- ( ph -> A = C )
2		mpteq12dv.2	. . 3 |- ( ph -> B = D )
3	2	adantr 481	. 2 |- ( ( ph /\ x e. A ) -> B = D )
4	1, 3	mpteq12dva 4732	1 |- ( ph -> ( x e. A |-> B ) = ( x e. C |-> D ) )

Syntax hints:   -> wi 4   = wceq 1483   e. wcel 1990   |-> cmpt 4729

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-ral 2917  df-opab 4713  df-mpt 4730

This theorem is referenced by:  mpteq12i  4742  ovmpt3rab1  6891  offval  6904  offval3  7162  cantnffval  8560  cnfcomlem  8596  fseqenlem1  8847  dfac12lem1  8965  dfac12r  8968  ackbij2lem2  9062  ackbij2lem3  9063  r1om  9066  ccatfval  13358  swrdval  13417  revval  13509  odzval  15496  vdwpc  15684  restval  16087  prdsval  16115  imasval  16171  qusval  16202  mrcfval  16268  cidfval  16337  monfval  16392  ismon  16393  isepi  16400  idfuval  16536  resfval  16552  resfval2  16553  fucval  16618  homafval  16679  idafval  16707  prfval  16839  prf2fval  16841  curfval  16863  curfpropd  16873  hofval  16892  hof2fval  16895  yonedalem3a  16914  yonedalem4a  16915  yonedalem4c  16917  yonedainv  16921  lubfval  16978  glbfval  16991  ipoval  17154  grpinvfval  17460  grpinvpropd  17490  cntzfval  17753  pmtrfval  17870  psgnfval  17920  odfval  17952  sylow1lem2  18014  sylow1lem4  18016  sylow2blem1  18035  sylow3lem1  18042  sylow3lem2  18043  sylow3lem3  18044  sylow3lem6  18047  pj1fval  18107  vrgpfval  18179  gsum2dlem2  18370  gsum2d2  18373  dprdval  18402  dprd2dlem2  18439  dprd2dlem1  18440  dprd2da  18441  dprd2d2  18443  dpjfval  18454  srgbinom  18545  staffval  18847  lspfval  18973  lsppropd  19018  sraval  19176  aspval  19328  asclfval  19334  ressascl  19344  psrval  19362  psrass1lem  19377  psrmulval  19386  mvrfval  19420  opsrval  19474  mpfrcl  19518  evlsval  19519  coe1mul2  19639  cply1mul  19664  evls1fval  19684  evl1fval  19692  isphl  19973  ocvfval  20010  pjfval  20050  uvcfval  20123  mamufval  20191  mvmulfval  20348  marepvfval  20371  submafval  20385  mdetfval  20392  madufval  20443  minmar1fval  20452  mat2pmatfval  20528  cpm2mfval  20554  decpmatmullem  20576  decpmatmulsumfsupp  20578  pm2mpval  20600  pm2mpmhmlem1  20623  pm2mpmhmlem2  20624  chpmatfval  20635  ntrfval  20828  clsfval  20829  neifval  20903  lpfval  20942  ordtval  20993  ordtbas2  20995  ordtcnv  21005  ordtrest  21006  ordtrest2  21008  cnpfval  21038  kqval  21529  fmval  21747  fmf  21749  flffval  21793  fcfval  21837  cnextval  21865  tsmsval2  21933  nmfval  22393  nmpropd  22398  nmpropd2  22399  subgnm  22437  tngnm  22455  nmofval  22518  pi1xfrcnv  22857  iscph  22970  tchval  23017  limcfval  23636  dvfval  23661  eldv  23662  mdegfval  23822  mdegmullem  23838  mdegpropd  23844  coe1mul3  23859  ig1pval  23932  taylfval  24113  ishlg  25497  mirval  25550  ishpg  25651  lmif  25677  islmib  25679  vtxdgfval  26363  vtxdeqd  26373  grpoinvfval  27376  nmoofval  27617  eigvalfval  28756  ressnm  29651  ordtprsval  29964  ordtprsuni  29965  ordtrestNEW  29967  indv  30074  ofcfval  30160  ofcfval3  30164  omsval  30355  sitgval  30394  issibf  30395  sitgfval  30403  signstfv  30640  cvmliftlem5  31271  cvmliftlem15  31280  mvrsval  31402  mrsubffval  31404  elmrsubrn  31417  msubffval  31420  mvhfval  31430  msrfval  31434  fwddifval  32269  fwddifnval  32270  tailfval  32367  cureq  33385  lsatset  34277  lkrfval  34374  pmapfval  35042  pclfvalN  35175  polfvalN  35190  watfvalN  35278  ldilfset  35394  ltrnfset  35403  dilfsetN  35439  trnfsetN  35442  trlfset  35447  trlset  35448  tgrpfset  36032  tendofset  36046  erngfset  36087  erngset  36088  erngfset-rN  36095  erngset-rN  36096  dvafset  36292  diaffval  36319  diafval  36320  dvhfset  36369  docaffvalN  36410  docafvalN  36411  djaffvalN  36422  dibffval  36429  dibfval  36430  dicffval  36463  dicfval  36464  dihffval  36519  dochffval  36638  dochfval  36639  djhffval  36685  lcdfval  36877  mapdffval  36915  mapdfval  36916  hvmapffval  37047  hvmapfval  37048  hdmap1ffval  37085  hdmap1fval  37086  hdmapffval  37118  hdmapfval  37119  hgmapffval  37177  hgmapfval  37178  hlhilset  37226  hbtlem1  37693  hbtlem7  37695  rgspnval  37738  cytpval  37787  rfovd  38295  fsovd  38302  fsovcnvlem  38307  dssmapfvd  38311  ntrneibex  38371  ovnval  40755  hspmbllem2  40841  smflimsuplem1  41026  smflimsuplem7  41032  smflimsup  41034  ply1mulgsumlem3  42176  ply1mulgsumlem4  42177  ply1mulgsum  42178  lincval  42198  offval0  42299