Theorem xpeq1 2440

Description: Equality theorem for cross product.

Assertion

Ref	Expression
xpeq1	⊢ (A = B → (A × C) = (B × C))

Proof of Theorem xpeq1

Step	Hyp	Ref	Expression
1		eleq2 1150	. . . 4 ⊢ (A = B → (x ∈ A ↔ x ∈ B))
2	1	anbi1d 469	. . 3 ⊢ (A = B → ((x ∈ A ∧ y ∈ C) ↔ (x ∈ B ∧ y ∈ C)))
3	2	biopabdv 2102	. 2 ⊢ (A = B → {⟨x, y⟩∣(x ∈ A ∧ y ∈ C)} = {⟨x, y⟩∣(x ∈ B ∧ y ∈ C)})
4		df-xp 2424	. 2 ⊢ (A × C) = {⟨x, y⟩∣(x ∈ A ∧ y ∈ C)}
5		df-xp 2424	. 2 ⊢ (B × C) = {⟨x, y⟩∣(x ∈ B ∧ y ∈ C)}
6	3, 4, 5	3eqtr4g 1147	1 ⊢ (A = B → (A × C) = (B × C))

Syntax hints:   → wi 2   ∧ wa 196   = wceq 1091   ∈ wcel 1092  {copab 2055   × cxp 2408

This theorem is referenced by:  opthprc 2457  xpexg 2489  xpindi 2497  dmxpid 2553  reseq2 2576  resabs1 2592  xpdisj1 2653  fssxp 2761  fconst 2774  xpsneng 3340  aceq5lem3 3560  aceq5lem4 3561  fodomb 3615  unxpdom 3650  sucxpdom 3652  cdavalt 3716  cdaassen 3725  infxpidmlem2 4934  infxpidmlem3 4935  infxpidmlem4 4936

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-opab 2098  df-xp 2424

metamath.org