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

Theorem xpeq2 5284
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 2826 . . . 4 (𝐴 = 𝐵 → (𝑦𝐴𝑦𝐵))
21anbi2d 742 . . 3 (𝐴 = 𝐵 → ((𝑥𝐶𝑦𝐴) ↔ (𝑥𝐶𝑦𝐵)))
32opabbidv 4866 . 2 (𝐴 = 𝐵 → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐶𝑦𝐴)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐶𝑦𝐵)})
4 df-xp 5270 . 2 (𝐶 × 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐶𝑦𝐴)}
5 df-xp 5270 . 2 (𝐶 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐶𝑦𝐵)}
63, 4, 53eqtr4g 2817 1 (𝐴 = 𝐵 → (𝐶 × 𝐴) = (𝐶 × 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1630  wcel 2137  {copab 4862   × cxp 5262
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-clab 2745  df-cleq 2751  df-clel 2754  df-opab 4863  df-xp 5270
This theorem is referenced by:  xpeq12  5289  xpeq2i  5291  xpeq2d  5294  xpnz  5709  xpdisj2  5712  dmxpss  5721  rnxpid  5723  xpcan  5726  unixp  5827  fconst5  6633  pmvalg  8032  xpcomeng  8215  unxpdom  8330  marypha1  8503  djueq12  8938  dfac5lem3  9136  dfac5lem4  9137  hsmexlem8  9436  axdc4uz  12975  hashxp  13411  mamufval  20391  txuni2  21568  txbas  21570  txopn  21605  txrest  21634  txdis  21635  txdis1cn  21638  txtube  21643  txcmplem2  21645  tx1stc  21653  qustgplem  22123  tsmsxplem1  22155  isgrpo  27658  vciOLD  27723  isvclem  27739  issh  28372  hhssablo  28427  hhssnvt  28429  hhsssh  28433  txomap  30208  tpr2rico  30265  elsx  30564  mbfmcst  30628  br2base  30638  dya2iocnrect  30650  sxbrsigalem5  30657  0rrv  30820  dfpo2  31950  elima4  31982  finxpeq1  33532  isbnd3  33894  hdmap1fval  37586  csbresgVD  39628
  Copyright terms: Public domain W3C validator