Theorem xpeq1 5128

Description: Equality theorem for Cartesian 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 2690	. . . 4 |- ( A = B -> ( x e. A <-> x e. B ) )
2	1	anbi1d 741	. . 3 |- ( A = B -> ( ( x e. A /\ y e. C ) <-> ( x e. B /\ y e. C ) ) )
3	2	opabbidv 4716	. 2 |- ( A = B -> { <. x , y >. | ( x e. A /\ y e. C ) } = { <. x , y >. | ( x e. B /\ y e. C ) } )
4		df-xp 5120	. 2 |- ( A X. C ) = { <. x , y >. | ( x e. A /\ y e. C ) }
5		df-xp 5120	. 2 |- ( B X. C ) = { <. x , y >. | ( x e. B /\ y e. C ) }
6	3, 4, 5	3eqtr4g 2681	1 |- ( A = B -> ( A X. C ) = ( B X. C ) )

Syntax hints:   -> wi 4   /\ wa 384   = wceq 1483   e. wcel 1990   {copab 4712   X. cxp 5112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-opab 4713  df-xp 5120

This theorem is referenced by:  xpeq12  5134  xpeq1i  5135  xpeq1d  5138  opthprc  5167  dmxpid  5345  reseq2  5391  xpnz  5553  xpdisj1  5555  xpcan2  5571  xpima  5576  unixp  5668  unixpid  5670  pmvalg  7868  xpsneng  8045  xpcomeng  8052  xpdom2g  8056  fodomr  8111  unxpdom  8167  xpfi  8231  marypha1lem  8339  cdaval  8992  iundom2g  9362  hashxplem  13220  dmtrclfv  13759  ramcl  15733  efgval  18130  frgpval  18171  frlmval  20092  txuni2  21368  txbas  21370  txopn  21405  txrest  21434  txdis  21435  txdis1cn  21438  tx1stc  21453  tmdgsum  21899  qustgplem  21924  incistruhgr  25974  isgrpo  27351  hhssablo  28120  hhssnvt  28122  hhsssh  28126  txomap  29901  tpr2rico  29958  elsx  30257  br2base  30331  dya2iocnrect  30343  sxbrsigalem5  30350  sibf0  30396  cvmlift2lem13  31297