Theorem mpt2eq123dv 6350

Description: An equality deduction for the maps to notation. (Contributed by NM, 12-Sep-2011.)

Hypotheses

Ref	Expression
mpt2eq123dv.1	|- ( ph -> A = D )
mpt2eq123dv.2	|- ( ph -> B = E )
mpt2eq123dv.3	|- ( ph -> C = F )

Assertion

Ref	Expression
mpt2eq123dv	|- ( ph -> ( x e. A , y e. B |-> C ) = ( x e. D , y e. E |-> F ) )

Distinct variable groups:   ph, x   ph, y

Allowed substitution hints:   A( x, y)   B( x, y)   C( x, y)   D( x, y)   E( x, y)   F( x, y)

Proof of Theorem mpt2eq123dv

Step	Hyp	Ref	Expression
1		mpt2eq123dv.1	. 2 |- ( ph -> A = D )
2		mpt2eq123dv.2	. . 3 |- ( ph -> B = E )
3	2	adantr 467	. 2 |- ( ( ph /\ x e. A ) -> B = E )
4		mpt2eq123dv.3	. . 3 |- ( ph -> C = F )
5	4	adantr 467	. 2 |- ( ( ph /\ ( x e. A /\ y e. B ) ) -> C = F )
6	1, 3, 5	mpt2eq123dva 6349	1 |- ( ph -> ( x e. A , y e. B |-> C ) = ( x e. D , y e. E |-> F ) )

Syntax hints:   -> wi 4   /\ wa 371   = wceq 1443   e. wcel 1886   |-> cmpt2 6290

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-oprab 6292  df-mpt2 6293

This theorem is referenced by:  mpt2eq123i  6351  bropopvvv  6871  bropfvvvv  6873  prdsval  15346  imasval  15404  imasvalOLD  15405  imasvscaval  15437  homffval  15588  homfeq  15592  comfffval  15596  comffval  15597  comfffval2  15599  comffval2  15600  comfeq  15604  oppcval  15611  monfval  15630  sectffval  15648  invffval  15656  isofn  15673  cofuval  15780  natfval  15844  fucval  15856  fucco  15860  coafval  15952  setcval  15965  setcco  15971  catcval  15984  catcco  15989  estrcval  16002  estrcco  16008  xpcval  16055  xpchomfval  16057  xpccofval  16060  1stfval  16069  2ndfval  16072  prfval  16077  evlfval  16095  evlf2  16096  curfval  16101  hofval  16130  hof2fval  16133  plusffval  16486  grpsubfval  16701  grpsubpropd  16749  mulgfval  16752  mulgpropd  16784  symgval  17013  lsmfval  17283  pj1fval  17337  efgtf  17365  prdsmgp  17831  dvrfval  17905  scaffval  18102  psrval  18579  ipffval  19208  frlmip  19329  mamufval  19403  mvmulfval  19560  marrepfval  19578  marepvfval  19583  submafval  19597  submaval  19599  madufval  19655  minmar1fval  19664  mat2pmatfval  19740  cpm2mfval  19766  decpmatval0  19781  decpmatval  19782  pmatcollpw3lem  19800  xkoval  20595  xkopt  20663  xpstopnlem1  20817  submtmd  21112  blfvalps  21391  ishtpy  21996  isphtpy  22005  pcofval  22034  rrxip  22342  q1pval  23097  r1pval  23100  taylfval  23307  midf  24811  ismidb  24813  ttgval  24898  wlkon  25254  trlon  25263  pthon  25298  spthon  25305  is2wlkonot  25584  is2spthonot  25585  2wlkonot3v  25596  2spthonot3v  25597  grpodivfval  25963  gxfval  25978  dipfval  26331  submatres  28625  lmatval  28632  lmatcl  28635  qqhval  28771  sxval  29005  sitmval  29175  cndprobval  29259  mclsval  30194  csbfinxpg  31773  rrnval  32152  ldualset  32685  paddfval  33356  tgrpfset  34305  tgrpset  34306  erngfset  34360  erngset  34361  erngfset-rN  34368  erngset-rN  34369  dvafset  34565  dvaset  34566  dvhfset  34642  dvhset  34643  djaffvalN  34695  djafvalN  34696  djhffval  34958  djhfval  34959  hlhilset  35499  eldiophb  35593  mendval  36043  hoidmvval  38393  ovnhoi  38419  hspval  38425  hspmbllem2  38443  hoimbl  38447  wlkson  39640  rngcvalALTV  39950  rngccoALTV  39977  funcrngcsetcALT  39988  ringcvalALTV  39996  ringccoALTV  40040  lincop  40188