Theorem xpeq1 3206

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

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

This theorem is referenced by:  opthprc 3227  xpindi 3276  dmxpid 3339  xpid11 3341  reseq2 3375  xpnz 3472  xpdisj1 3474  rnxpss 3480  xp11 3482  rescnvcnv 3499  resdmres 3503  unixp 3523  fssxp 3643  fconst 3664  curry1 4104  pmvalg 4337  xpsneng 4442  xpcomeng 4446  xpdom1g 4450  fodomr 4489  aceq5lem3 4747  aceq5lem4 4748  unidomg 4819  unxpdom 4855  sucxpdom 4857  cdavalt 4931  cdaassen 4942  climconst3 7096  serzclim0 7109  infxpidmlem2 7554  infxpidmlem3 7555  infxpidmlem4 7556  ismet 7795  dfms2 7796  ismsg 7797  msflem 7800  metreslem 7819  isgrp 8038  isring 8137  ringi 8138  0ofval 8443  hhssablt 9128  hhssnvt 9130  hhsssh 9134  occllem5 9172  hh0o 9824  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