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

Theorem xpeq2 5163
 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 2719 . . . 4 (𝐴 = 𝐵 → (𝑦𝐴𝑦𝐵))
21anbi2d 740 . . 3 (𝐴 = 𝐵 → ((𝑥𝐶𝑦𝐴) ↔ (𝑥𝐶𝑦𝐵)))
32opabbidv 4749 . 2 (𝐴 = 𝐵 → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐶𝑦𝐴)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐶𝑦𝐵)})
4 df-xp 5149 . 2 (𝐶 × 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐶𝑦𝐴)}
5 df-xp 5149 . 2 (𝐶 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐶𝑦𝐵)}
63, 4, 53eqtr4g 2710 1 (𝐴 = 𝐵 → (𝐶 × 𝐴) = (𝐶 × 𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   = wceq 1523   ∈ wcel 2030  {copab 4745   × cxp 5141 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-opab 4746  df-xp 5149 This theorem is referenced by:  xpeq12  5168  xpeq2i  5170  xpeq2d  5173  xpnz  5588  xpdisj2  5591  dmxpss  5600  rnxpid  5602  xpcan  5605  unixp  5706  fconst5  6512  pmvalg  7910  xpcomeng  8093  unxpdom  8208  marypha1  8381  dfac5lem3  8986  dfac5lem4  8987  hsmexlem8  9284  axdc4uz  12823  hashxp  13259  mamufval  20239  txuni2  21416  txbas  21418  txopn  21453  txrest  21482  txdis  21483  txdis1cn  21486  txtube  21491  txcmplem2  21493  tx1stc  21501  qustgplem  21971  tsmsxplem1  22003  isgrpo  27479  vciOLD  27544  isvclem  27560  issh  28193  hhssablo  28248  hhssnvt  28250  hhsssh  28254  txomap  30029  tpr2rico  30086  elsx  30385  mbfmcst  30449  br2base  30459  dya2iocnrect  30471  sxbrsigalem5  30478  0rrv  30641  dfpo2  31771  elima4  31803  finxpeq1  33353  isbnd3  33713  hdmap1fval  37403  csbresgVD  39445
 Copyright terms: Public domain W3C validator