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

Theorem xpeq1 5699
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 2830 . . . 4 (𝐴 = 𝐵 → (𝑥𝐴𝑥𝐵))
21anbi1d 631 . . 3 (𝐴 = 𝐵 → ((𝑥𝐴𝑦𝐶) ↔ (𝑥𝐵𝑦𝐶)))
32opabbidv 5209 . 2 (𝐴 = 𝐵 → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)})
4 df-xp 5691 . 2 (𝐴 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)}
5 df-xp 5691 . 2 (𝐵 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)}
63, 4, 53eqtr4g 2802 1 (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1540  wcel 2108  {copab 5205   × cxp 5683
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-opab 5206  df-xp 5691
This theorem is referenced by:  xpeq12  5710  xpeq1i  5711  xpeq1d  5714  opthprc  5749  dmxpid  5941  reseq2  5992  xpnz  6179  xpdisj1  6181  xpcan2  6197  xpima  6202  unixp  6302  unixpid  6304  naddcllem  8714  pmvalg  8877  xpsneng  9096  xpcomeng  9104  xpdom2g  9108  fodomr  9168  unxpdom  9289  xpfiOLD  9359  fodomfir  9368  marypha1lem  9473  iundom2g  10580  hashxplem  14472  dmtrclfv  15057  ramcl  17067  efgval  19735  frgpval  19776  frlmval  21768  txuni2  23573  txbas  23575  txopn  23610  txrest  23639  txdis  23640  txdis1cn  23643  tx1stc  23658  tmdgsum  24103  qustgplem  24129  incistruhgr  29096  isgrpo  30516  hhssablo  31282  hhssnvt  31284  hhsssh  31288  gsumpart  33060  txomap  33833  tpr2rico  33911  elsx  34195  br2base  34271  dya2iocnrect  34283  sxbrsigalem5  34290  sibf0  34336  cvmlift2lem13  35320
  Copyright terms: Public domain W3C validator