Theorem xpeq2 3201

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 1535	. . . 4 |- (A = B -> (y e. A <-> y e. B))
2	1	anbi2d 616	. . 3 |- (A = B -> ((x e. C /\ y e. A) <-> (x e. C /\ y e. B)))
3	2	opabbidv 2670	. 2 |- (A = B -> {<.x, y>. | (x e. C /\ y e. A)} = {<.x, y>. | (x e. C /\ y e. B)})
4		df-xp 3184	. 2 |- (C X. A) = {<.x, y>. | (x e. C /\ y e. A)}
5		df-xp 3184	. 2 |- (C X. B) = {<.x, y>. | (x e. C /\ y e. B)}
6	3, 4, 5	3eqtr4g 1531	1 |- (A = B -> (C X. A) = (C X. B))

Syntax hints:   -> wi 3   /\ wa 223   = wceq 956   e. wcel 958  {copab 2666   X. cxp 3168

This theorem is referenced by:  xpindir 3271  xpid11 3335  xpnz 3466  xpdisj2 3469  dmxpss 3473  xp11 3476  rescnvcnv 3493  unixp 3517  fconstg 3659  fconst5 3848  curry1 4098  pmvalg 4331  xpsneng 4436  xpcomeng 4440  xpdom2 4442  xpdom1g 4444  aceq5lem3 4737  aceq5lem4 4738  unidomg 4809  unxpdom 4844  sucxpdom 4846  xp1en 4927  xp2cda 4928  xpcdaen 4931  expvalt 6570  infxpidmlem2 7553  infxpidmlem3 7554  infxpidmlem4 7555  infxpdom 7571  ismet 7798  dfms2 7799  ismsg 7800  msflem 7803  metreslem 7822  lmfval 7925  caufval 7926  isgrp 8041  isring 8141  ringi 8142  vci 8167  isvclem 8196  vcoprnelem 8197  0ofval 8447  hhssablt 9133  hhssnvt 9135  hhsssh 9139  df0op2 9678  ho01 9754  hh0o 9829  nmop0h 9916  ghomgrplem 10389

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-opab 2667  df-xp 3184

Copyright terms: Public domain