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

Theorem xpeq1 5264
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 2839 . . . 4 (𝐴 = 𝐵 → (𝑥𝐴𝑥𝐵))
21anbi1d 615 . . 3 (𝐴 = 𝐵 → ((𝑥𝐴𝑦𝐶) ↔ (𝑥𝐵𝑦𝐶)))
32opabbidv 4851 . 2 (𝐴 = 𝐵 → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)})
4 df-xp 5256 . 2 (𝐴 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)}
5 df-xp 5256 . 2 (𝐵 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)}
63, 4, 53eqtr4g 2830 1 (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1631  wcel 2145  {copab 4847   × cxp 5248
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-opab 4848  df-xp 5256
This theorem is referenced by:  xpeq12  5274  xpeq1i  5275  xpeq1d  5278  opthprc  5306  dmxpid  5482  reseq2  5528  xpnz  5693  xpdisj1  5695  xpcan2  5711  xpima  5716  unixp  5811  unixpid  5813  pmvalg  8023  xpsneng  8204  xpcomeng  8211  xpdom2g  8215  fodomr  8270  unxpdom  8326  xpfi  8390  marypha1lem  8498  cdaval  9197  iundom2g  9567  hashxplem  13421  dmtrclfv  13966  ramcl  15939  efgval  18336  frgpval  18377  frlmval  20308  txuni2  21588  txbas  21590  txopn  21625  txrest  21654  txdis  21655  txdis1cn  21658  tx1stc  21673  tmdgsum  22118  qustgplem  22143  incistruhgr  26194  isgrpo  27690  hhssablo  28459  hhssnvt  28461  hhsssh  28465  txomap  30240  tpr2rico  30297  elsx  30596  br2base  30670  dya2iocnrect  30682  sxbrsigalem5  30689  sibf0  30735  cvmlift2lem13  31634
  Copyright terms: Public domain W3C validator