Theorem xpeq2 3207

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 1538	. . . 4 ⊢ (A = B → (y ∈ A ↔ y ∈ B))
2	1	anbi2d 618	. . 3 ⊢ (A = B → ((x ∈ C ⋀ y ∈ A) ↔ (x ∈ C ⋀ y ∈ B)))
3	2	opabbidv 2675	. 2 ⊢ (A = B → {⟨x, y⟩∣(x ∈ C ⋀ y ∈ A)} = {⟨x, y⟩∣(x ∈ C ⋀ y ∈ B)})
4		df-xp 3190	. 2 ⊢ (C × A) = {⟨x, y⟩∣(x ∈ C ⋀ y ∈ A)}
5		df-xp 3190	. 2 ⊢ (C × B) = {⟨x, y⟩∣(x ∈ C ⋀ y ∈ B)}
6	3, 4, 5	3eqtr4g 1534	1 ⊢ (A = B → (C × A) = (C × B))

Syntax hints:   → wi 3   ⋀ wa 223   = wceq 958   ∈ wcel 960  {copab 2671   × cxp 3174

This theorem is referenced by:  xpindir 3277  xpid11 3341  xpnz 3472  xpdisj2 3475  dmxpss 3479  xp11 3482  rescnvcnv 3499  unixp 3523  fconstg 3665  fconst5 3854  curry1 4104  pmvalg 4337  xpsneng 4442  xpcomeng 4446  xpdom2 4448  xpdom1g 4450  aceq5lem3 4747  aceq5lem4 4748  unidomg 4819  unxpdom 4855  sucxpdom 4857  xp1en 4939  xp2cda 4940  xpcdaen 4943  expvalt 6571  infxpidmlem2 7554  infxpidmlem3 7555  infxpidmlem4 7556  infxpdom 7572  ismet 7795  dfms2 7796  ismsg 7797  msflem 7800  metreslem 7819  lmfval 7922  caufval 7923  isgrp 8038  isring 8137  ringi 8138  vci 8163  isvclem 8192  vcoprnelem 8193  0ofval 8443  hhssablt 9128  hhssnvt 9130  hhsssh 9134  df0op2 9673  ho01 9749  hh0o 9824  nmop0h 9911  ghomgrplem 10384

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 2672  df-xp 3190

Copyright terms: Public domain