Theorem xpeq1 3207

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 1538	. . . 4 |- (A = B -> (x e. A <-> x e. B))
2	1	anbi1d 619	. . 3 |- (A = B -> ((x e. A /\ y e. C) <-> (x e. B /\ y e. C)))
3	2	opabbidv 2676	. 2 |- (A = B -> {<.x, y>. | (x e. A /\ y e. C)} = {<.x, y>. | (x e. B /\ y e. C)})
4		df-xp 3191	. 2 |- (A X. C) = {<.x, y>. | (x e. A /\ y e. C)}
5		df-xp 3191	. 2 |- (B X. C) = {<.x, y>. | (x e. B /\ y e. C)}
6	3, 4, 5	3eqtr4g 1534	1 |- (A = B -> (A X. C) = (B X. C))

Syntax hints:   -> wi 3   /\ wa 223   = wceq 958   e. wcel 960  {copab 2672   X. cxp 3175

This theorem is referenced by:  opthprc 3228  xpindi 3277  dmxpid 3340  xpid11 3342  reseq2 3376  xpnz 3473  xpdisj1 3475  rnxpss 3481  xp11 3483  rescnvcnv 3500  resdmres 3504  unixp 3524  fssxp 3644  fconst 3665  curry1 4105  pmvalg 4338  xpsneng 4443  xpcomeng 4447  xpdom1g 4451  fodomr 4490  aceq5lem3 4754  aceq5lem4 4755  unidomg 4826  unxpdom 4862  sucxpdom 4864  cdavalt 4938  cdaassen 4949  climconst3 7103  serzclim0 7116  infxpidmlem2 7561  infxpidmlem3 7562  infxpidmlem4 7563  ismet 7802  dfms2 7803  ismsg 7804  msflem 7807  metreslem 7826  isgrp 8045  isring 8144  ringi 8145  0ofval 8450  hhssablt 9135  hhssnvt 9137  hhsssh 9141  occllem5 9179  hh0o 9831  ghomgrplem 10392

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-opab 2673  df-xp 3191

Copyright terms: Public domain