Theorem xpeq1 3195

Description: Equality theorem for cross product.

Assertion

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

Proof of Theorem xpeq1

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

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

This theorem is referenced by:  opthprc 3216  xpindi 3265  dmxpid 3328  xpid11 3330  reseq2 3361  xpnz 3458  xpdisj1 3460  rnxpss 3466  xp11 3468  rescnvcnv 3485  resdmres 3489  unixp 3509  fssxp 3628  fconst 3649  curry1 4088  pmvalg 4321  xpsneng 4422  xpcomeng 4426  xpdom1g 4430  fodomr 4469  aceq5lem3 4717  aceq5lem4 4718  unidomg 4789  unxpdom 4824  sucxpdom 4826  cdavalt 4899  cdaassen 4910  climconst3 7041  serzclim0 7054  infxpidmlem2 7504  infxpidmlem3 7505  infxpidmlem4 7506  ismet 7748  dfms2 7749  ismsg 7750  msflem 7753  metreslem 7774  isgrp 7991  isring 8093  ringi 8094  0ofval 8392  hhssablt 9072  hhssnvt 9074  hhsssh 9078  occllem5 9116  hh0o 9769  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