Theorem xpeq2 3196

Description: Equality theorem for cross product.

Assertion

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

Proof of Theorem xpeq2

Step	Hyp	Ref	Expression
1		eleq2 1532	. . . 4 |- (A = B -> (y e. A <-> y e. B))
2	1	anbi2d 615	. . 3 |- (A = B -> ((x e. C /\ y e. A) <-> (x e. C /\ y e. B)))
3	2	opabbidv 2665	. 2 |- (A = B -> {<.x, y>. | (x e. C /\ y e. A)} = {<.x, y>. | (x e. C /\ y e. B)})
4		df-xp 3179	. 2 |- (C X. A) = {<.x, y>. | (x e. C /\ y e. A)}
5		df-xp 3179	. 2 |- (C X. B) = {<.x, y>. | (x e. C /\ y e. B)}
6	3, 4, 5	3eqtr4g 1528	1 |- (A = B -> (C X. A) = (C X. B))

Syntax hints:   -> wi 3   /\ wa 223   = wceq 954   e. wcel 956  {copab 2661   X. cxp 3163

This theorem is referenced by:  xpindir 3266  xpid11 3330  xpnz 3458  xpdisj2 3461  dmxpss 3465  xp11 3468  rescnvcnv 3485  unixp 3509  fconstg 3650  fconst5 3839  curry1 4088  pmvalg 4321  xpsneng 4422  xpcomeng 4426  xpdom2 4428  xpdom1g 4430  aceq5lem3 4717  aceq5lem4 4718  unidomg 4789  unxpdom 4824  sucxpdom 4826  xp1en 4907  xp2cda 4908  xpcdaen 4911  expvalt 6510  infxpidmlem2 7504  infxpidmlem3 7505  infxpidmlem4 7506  infxpdom 7522  ismet 7748  dfms2 7749  ismsg 7750  msflem 7753  metreslem 7774  lmfval 7877  caufval 7878  isgrp 7991  isring 8093  ringi 8094  vci 8119  isvclem 8148  vcoprnelem 8149  0ofval 8392  hhssablt 9072  hhssnvt 9074  hhsssh 9078  df0op2 9618  ho01 9694  hh0o 9769  nmop0h 9854  ghomgrplem 10323

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-opab 2662  df-xp 3179

Copyright terms: Public domain