Theorem xpeq1 4511

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

Assertion

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

Proof of Theorem xpeq1

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

Step	Hyp	Ref	Expression
1		eleq2 2176	. . . 4 |- ( A = B -> ( x e. A <-> x e. B ) )
2	1	anbi1d 458	. . 3 |- ( A = B -> ( ( x e. A /\ y e. C ) <-> ( x e. B /\ y e. C ) ) )
3	2	opabbidv 3952	. 2 |- ( A = B -> { <. x , y >. | ( x e. A /\ y e. C ) } = { <. x , y >. | ( x e. B /\ y e. C ) } )
4		df-xp 4503	. 2 |- ( A X. C ) = { <. x , y >. | ( x e. A /\ y e. C ) }
5		df-xp 4503	. 2 |- ( B X. C ) = { <. x , y >. | ( x e. B /\ y e. C ) }
6	3, 4, 5	3eqtr4g 2170	1 |- ( A = B -> ( A X. C ) = ( B X. C ) )

Syntax hints:   -> wi 4   /\ wa 103   = wceq 1312   e. wcel 1461   {copab 3946   X. cxp 4495

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-11 1465  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-opab 3948  df-xp 4503

This theorem is referenced by:  xpeq12  4516  xpeq1i  4517  xpeq1d  4520  opthprc  4548  reseq2  4770  xpeq0r  4917  xpdisj1  4919  xpima1  4941  pmvalg  6505  xpsneng  6667  xpcomeng  6673  xpdom2g  6677  xpfi  6769  exmidomni  6962  exmidfodomrlemim  7002  hashxp  10459  txuni2  12261  txbas  12263  txopn  12270  txrest  12281  txdis  12282  txdis1cn  12283  xmettxlem  12492  xmettx  12493