Theorem xpeq2 4678

Description: Equality theorem for cross product. (Contributed by NM, 5-Jul-1994.)

Assertion

Ref	Expression
xpeq2	|- ( A = B -> ( C X. A ) = ( C X. B ) )

Proof of Theorem xpeq2

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq2 2260	. . . 4 |- ( A = B -> ( y e. A <-> y e. B ) )
2	1	anbi2d 464	. . 3 |- ( A = B -> ( ( x e. C /\ y e. A ) <-> ( x e. C /\ y e. B ) ) )
3	2	opabbidv 4099	. 2 |- ( A = B -> { <. x , y >. | ( x e. C /\ y e. A ) } = { <. x , y >. | ( x e. C /\ y e. B ) } )
4		df-xp 4669	. 2 |- ( C X. A ) = { <. x , y >. | ( x e. C /\ y e. A ) }
5		df-xp 4669	. 2 |- ( C X. B ) = { <. x , y >. | ( x e. C /\ y e. B ) }
6	3, 4, 5	3eqtr4g 2254	1 |- ( A = B -> ( C X. A ) = ( C X. B ) )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1364   e. wcel 2167   {copab 4093   X. cxp 4661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-opab 4095  df-xp 4669

This theorem is referenced by:  xpeq12  4682  xpeq2i  4684  xpeq2d  4687  xpeq0r  5092  xpdisj2  5095  pmvalg  6718  xpcomeng  6887  djueq12  7105  txuni2  14492  txbas  14494  txopn  14501  txrest  14512  txdis  14513  txdis1cn  14514  xmettxlem  14745  xmettx  14746