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

Theorem xpeq1 5546
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 2902 . . . 4 (𝐴 = 𝐵 → (𝑥𝐴𝑥𝐵))
21anbi1d 632 . . 3 (𝐴 = 𝐵 → ((𝑥𝐴𝑦𝐶) ↔ (𝑥𝐵𝑦𝐶)))
32opabbidv 5108 . 2 (𝐴 = 𝐵 → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)})
4 df-xp 5538 . 2 (𝐴 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)}
5 df-xp 5538 . 2 (𝐵 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)}
63, 4, 53eqtr4g 2882 1 (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1538  wcel 2114  {copab 5104   × cxp 5530
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-12 2178  ax-ext 2794
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-opab 5105  df-xp 5538
This theorem is referenced by:  xpeq12  5557  xpeq1i  5558  xpeq1d  5561  opthprc  5593  dmxpid  5777  reseq2  5826  xpnz  5994  xpdisj1  5996  xpcan2  6012  xpima  6017  unixp  6111  unixpid  6113  pmvalg  8404  xpsneng  8589  xpcomeng  8596  xpdom2g  8600  fodomr  8656  unxpdom  8713  xpfi  8777  marypha1lem  8885  iundom2g  9951  hashxplem  13790  dmtrclfv  14369  ramcl  16354  efgval  18834  frgpval  18875  frlmval  20435  txuni2  22168  txbas  22170  txopn  22205  txrest  22234  txdis  22235  txdis1cn  22238  tx1stc  22253  tmdgsum  22698  qustgplem  22724  incistruhgr  26870  isgrpo  28278  hhssablo  29044  hhssnvt  29046  hhsssh  29050  txomap  31156  tpr2rico  31229  elsx  31527  br2base  31601  dya2iocnrect  31613  sxbrsigalem5  31620  sibf0  31666  cvmlift2lem13  32636
  Copyright terms: Public domain W3C validator