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

Theorem xpeq2 5563
 Description: Equality theorem for Cartesian product. (Contributed by NM, 5-Jul-1994.)
Assertion
Ref Expression
xpeq2 (𝐴 = 𝐵 → (𝐶 × 𝐴) = (𝐶 × 𝐵))

Proof of Theorem xpeq2
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eleq2 2904 . . . 4 (𝐴 = 𝐵 → (𝑦𝐴𝑦𝐵))
21anbi2d 631 . . 3 (𝐴 = 𝐵 → ((𝑥𝐶𝑦𝐴) ↔ (𝑥𝐶𝑦𝐵)))
32opabbidv 5118 . 2 (𝐴 = 𝐵 → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐶𝑦𝐴)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐶𝑦𝐵)})
4 df-xp 5548 . 2 (𝐶 × 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐶𝑦𝐴)}
5 df-xp 5548 . 2 (𝐶 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐶𝑦𝐵)}
63, 4, 53eqtr4g 2884 1 (𝐴 = 𝐵 → (𝐶 × 𝐴) = (𝐶 × 𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2115  {copab 5114   × cxp 5540 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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-12 2179  ax-ext 2796 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-opab 5115  df-xp 5548 This theorem is referenced by:  xpeq12  5567  xpeq2i  5569  xpeq2d  5572  xpnz  6003  xpdisj2  6006  dmxpss  6015  rnxpid  6017  xpcan  6020  unixp  6120  fconst5  6959  pmvalg  8413  xpcomeng  8605  unxpdom  8722  marypha1  8895  djueq12  9330  dfac5lem3  9549  dfac5lem4  9550  hsmexlem8  9844  axdc4uz  13356  hashxp  13800  mamufval  20996  txuni2  22173  txbas  22175  txopn  22210  txrest  22239  txdis  22240  txdis1cn  22243  txtube  22248  txcmplem2  22250  tx1stc  22258  qustgplem  22729  tsmsxplem1  22761  isgrpo  28283  vciOLD  28347  isvclem  28363  issh  28994  hhssablo  29049  hhssnvt  29051  hhsssh  29055  txomap  31158  tpr2rico  31212  elsx  31510  mbfmcst  31574  br2base  31584  dya2iocnrect  31596  sxbrsigalem5  31603  0rrv  31766  dfpo2  33048  elima4  33076  finxpeq1  34748  isbnd3  35167  hdmap1fval  39037  csbresgVD  41521
 Copyright terms: Public domain W3C validator