Theorem mpt2eq3dv 6721

Description: An equality deduction for the maps to notation restricted to the value of the operation. (Contributed by SO, 16-Jul-2018.)

Hypothesis

Ref	Expression
mpt2eq3dv.1	|- ( ph -> C = D )

Assertion

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

Distinct variable groups:   ph, x   ph, y

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

Proof of Theorem mpt2eq3dv

Step	Hyp	Ref	Expression
1		mpt2eq3dv.1	. . 3 |- ( ph -> C = D )
2	1	3ad2ant1 1082	. 2 |- ( ( ph /\ x e. A /\ y e. B ) -> C = D )
3	2	mpt2eq3dva 6719	1 |- ( ph -> ( x e. A , y e. B |-> C ) = ( x e. A , y e. B |-> D ) )

Syntax hints:   -> wi 4   = wceq 1483   e. wcel 1990   |-> cmpt2 6652

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-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-oprab 6654  df-mpt2 6655

This theorem is referenced by:  seqomeq12  7549  cantnfval  8565  seqeq2  12805  seqeq3  12806  relexpsucnnr  13765  lsmfval  18053  phssip  20003  mamuval  20192  matsc  20256  marrepval0  20367  marrepval  20368  marepvval0  20372  marepvval  20373  submaval0  20386  mdetr0  20411  mdet0  20412  mdetunilem7  20424  mdetunilem8  20425  madufval  20443  maduval  20444  maducoeval2  20446  madutpos  20448  madugsum  20449  madurid  20450  minmar1val0  20453  minmar1val  20454  pmat0opsc  20503  pmat1opsc  20504  mat2pmatval  20529  cpm2mval  20555  decpmatid  20575  pmatcollpw2lem  20582  pmatcollpw3lem  20588  mply1topmatval  20609  mp2pm2mplem1  20611  mp2pm2mplem4  20614  ttgval  25755  smatfval  29861  ofceq  30159  reprval  30688  finxpeq1  33223  matunitlindflem1  33405  idfusubc  41866  digfval  42391