Theorem xpeq2 2441

Description: Equality theorem for cross product.

Assertion

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

Proof of Theorem xpeq2

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

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

This theorem is referenced by:  xpexg 2489  xpindir 2498  resabs1 2592  xpdisj2 2654  fconstg 2775  xpsneng 3340  aceq5lem3 3560  aceq5lem4 3561  unxpdom 3650  sucxpdom 3652  xp1en 3722  xp2cda 3723  xpcdaen 3726  expvalt 4677  infxpidmlem2 4934  infxpidmlem3 4935  infxpidmlem4 4936  ho0 5612

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