Theorem mpt2eq3ia 6720

Description: An equality inference for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)

Hypothesis

Ref	Expression
mpt2eq3ia.1	|- ( ( x e. A /\ y e. B ) -> C = D )

Assertion

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

Proof of Theorem mpt2eq3ia

Step	Hyp	Ref	Expression
1		mpt2eq3ia.1	. . . 4 |- ( ( x e. A /\ y e. B ) -> C = D )
2	1	3adant1 1079	. . 3 |- ( ( T. /\ x e. A /\ y e. B ) -> C = D )
3	2	mpt2eq3dva 6719	. 2 |- ( T. -> ( x e. A , y e. B |-> C ) = ( x e. A , y e. B |-> D ) )
4	3	trud 1493	1 |- ( x e. A , y e. B |-> C ) = ( x e. A , y e. B |-> D )

Syntax hints:   -> wi 4   /\ wa 384   = wceq 1483   T. wtru 1484   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:  mpt2difsnif  6753  mpt2snif  6754  oprab2co  7262  cnfcomlem  8596  cnfcom2  8599  dfioo2  12274  elovmpt2wrd  13347  sadcom  15185  comfffval2  16361  oppchomf  16380  symgga  17826  oppglsm  18057  dfrhm2  18717  cnfldsub  19774  cnflddiv  19776  mat0op  20225  mattpos1  20262  mdetunilem7  20424  madufval  20443  maducoeval2  20446  madugsum  20449  mp2pm2mplem5  20615  mp2pm2mp  20616  leordtval  21017  xpstopnlem1  21612  divcn  22671  oprpiece1res1  22750  oprpiece1res2  22751  cxpcn  24486  numclwwlk6  27248  cnnvm  27537  mdetpmtr2  29890  madjusmdetlem1  29893  cnre2csqima  29957  mndpluscn  29972  raddcn  29975  icorempt2  33199  matunitlindflem1  33405  mendplusgfval  37755  hoidmv1le  40808  hspdifhsp  40830  vonn0ioo  40901  vonn0icc  40902  dflinc2  42199