Theorem xpeq1 5635

Description: Equality theorem for Cartesian product. (Contributed by NM, 4-Jul-1994.)

Assertion

Ref	Expression
xpeq1	⊢ (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶))

Proof of Theorem xpeq1

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq2 2822	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	anbi1d 631	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))
3	2	opabbidv 5161	. 2 ⊢ (𝐴 = 𝐵 → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)})
4		df-xp 5627	. 2 ⊢ (𝐴 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)}
5		df-xp 5627	. 2 ⊢ (𝐵 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)}
6	3, 4, 5	3eqtr4g 2793	1 ⊢ (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  {copab 5157   × cxp 5619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-opab 5158  df-xp 5627

This theorem is referenced by:  xpeq12  5646  xpeq1i  5647  xpeq1d  5650  opthprc  5685  dmxpid  5876  reseq2  5930  xpnz  6114  xpdisj1  6116  xpcan2  6132  xpima  6137  unixp  6237  unixpid  6239  naddcllem  8600  pmvalg  8770  xpsneng  8986  xpcomeng  8993  xpdom2g  8997  fodomr  9052  unxpdom  9154  fodomfir  9223  marypha1lem  9328  iundom2g  10442  hashxplem  14347  dmtrclfv  14932  ramcl  16948  efgval  19637  frgpval  19678  frlmval  21694  txuni2  23500  txbas  23502  txopn  23537  txrest  23566  txdis  23567  txdis1cn  23570  tx1stc  23585  tmdgsum  24030  qustgplem  24056  incistruhgr  29078  isgrpo  30498  hhssablo  31264  hhssnvt  31266  hhsssh  31270  gsumpart  33074  txomap  33919  tpr2rico  33997  elsx  34279  br2base  34354  dya2iocnrect  34366  sxbrsigalem5  34373  sibf0  34419  cvmlift2lem13  35431