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

Theorem xpeq2 5376
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 2848 . . . 4 (𝐴 = 𝐵 → (𝑦𝐴𝑦𝐵))
21anbi2d 622 . . 3 (𝐴 = 𝐵 → ((𝑥𝐶𝑦𝐴) ↔ (𝑥𝐶𝑦𝐵)))
32opabbidv 4952 . 2 (𝐴 = 𝐵 → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐶𝑦𝐴)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐶𝑦𝐵)})
4 df-xp 5361 . 2 (𝐶 × 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐶𝑦𝐴)}
5 df-xp 5361 . 2 (𝐶 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐶𝑦𝐵)}
63, 4, 53eqtr4g 2839 1 (𝐴 = 𝐵 → (𝐶 × 𝐴) = (𝐶 × 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386   = wceq 1601  wcel 2107  {copab 4948   × cxp 5353
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-12 2163  ax-ext 2754
This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-opab 4949  df-xp 5361
This theorem is referenced by:  xpeq12  5380  xpeq2i  5382  xpeq2d  5385  xpnz  5807  xpdisj2  5810  dmxpss  5819  rnxpid  5821  xpcan  5824  unixp  5922  fconst5  6743  pmvalg  8151  xpcomeng  8340  unxpdom  8455  marypha1  8628  djueq12  9064  dfac5lem3  9281  dfac5lem4  9282  hsmexlem8  9581  axdc4uz  13102  hashxp  13535  mamufval  20595  txuni2  21777  txbas  21779  txopn  21814  txrest  21843  txdis  21844  txdis1cn  21847  txtube  21852  txcmplem2  21854  tx1stc  21862  qustgplem  22332  tsmsxplem1  22364  isgrpo  27924  vciOLD  27988  isvclem  28004  issh  28637  hhssablo  28692  hhssnvt  28694  hhsssh  28698  txomap  30499  tpr2rico  30556  elsx  30855  mbfmcst  30919  br2base  30929  dya2iocnrect  30941  sxbrsigalem5  30948  0rrv  31112  dfpo2  32239  elima4  32267  finxpeq1  33818  isbnd3  34207  hdmap1fval  37950  csbresgVD  40064
  Copyright terms: Public domain W3C validator