MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xpeq1 Structured version   Visualization version   GIF version

Theorem xpeq1 5604
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.
StepHypRef Expression
1 eleq2 2829 . . . 4 (𝐴 = 𝐵 → (𝑥𝐴𝑥𝐵))
21anbi1d 630 . . 3 (𝐴 = 𝐵 → ((𝑥𝐴𝑦𝐶) ↔ (𝑥𝐵𝑦𝐶)))
32opabbidv 5145 . 2 (𝐴 = 𝐵 → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)})
4 df-xp 5596 . 2 (𝐴 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)}
5 df-xp 5596 . 2 (𝐵 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)}
63, 4, 53eqtr4g 2805 1 (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1542  wcel 2110  {copab 5141   × cxp 5588
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-opab 5142  df-xp 5596
This theorem is referenced by:  xpeq12  5615  xpeq1i  5616  xpeq1d  5619  opthprc  5652  dmxpid  5838  reseq2  5885  xpnz  6061  xpdisj1  6063  xpcan2  6079  xpima  6084  unixp  6184  unixpid  6186  pmvalg  8609  xpsneng  8826  xpcomeng  8833  xpdom2g  8837  fodomr  8897  unxpdom  9008  xpfi  9063  marypha1lem  9170  iundom2g  10297  hashxplem  14146  dmtrclfv  14727  ramcl  16728  efgval  19321  frgpval  19362  frlmval  20953  txuni2  22714  txbas  22716  txopn  22751  txrest  22780  txdis  22781  txdis1cn  22784  tx1stc  22799  tmdgsum  23244  qustgplem  23270  incistruhgr  27447  isgrpo  28855  hhssablo  29621  hhssnvt  29623  hhsssh  29627  gsumpart  31311  txomap  31780  tpr2rico  31858  elsx  32158  br2base  32232  dya2iocnrect  32244  sxbrsigalem5  32251  sibf0  32297  cvmlift2lem13  33273  naddcllem  33827
  Copyright terms: Public domain W3C validator