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

Theorem xpeq1 5371
 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 2848 . . . 4 (𝐴 = 𝐵 → (𝑥𝐴𝑥𝐵))
21anbi1d 623 . . 3 (𝐴 = 𝐵 → ((𝑥𝐴𝑦𝐶) ↔ (𝑥𝐵𝑦𝐶)))
32opabbidv 4954 . 2 (𝐴 = 𝐵 → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)})
4 df-xp 5363 . 2 (𝐴 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)}
5 df-xp 5363 . 2 (𝐵 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)}
63, 4, 53eqtr4g 2839 1 (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 386   = wceq 1601   ∈ wcel 2107  {copab 4950   × cxp 5355 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 4951  df-xp 5363 This theorem is referenced by:  xpeq12  5382  xpeq1i  5383  xpeq1d  5386  opthprc  5415  dmxpid  5592  reseq2  5639  xpnz  5809  xpdisj1  5811  xpcan2  5827  xpima  5832  unixp  5924  unixpid  5926  pmvalg  8153  xpsneng  8335  xpcomeng  8342  xpdom2g  8346  fodomr  8401  unxpdom  8457  xpfi  8521  marypha1lem  8629  cdaval  9329  iundom2g  9699  hashxplem  13538  dmtrclfv  14170  ramcl  16141  efgval  18518  frgpval  18561  frlmval  20495  txuni2  21781  txbas  21783  txopn  21818  txrest  21847  txdis  21848  txdis1cn  21851  tx1stc  21866  tmdgsum  22311  qustgplem  22336  incistruhgr  26431  isgrpo  27928  hhssablo  28696  hhssnvt  28698  hhsssh  28702  txomap  30503  tpr2rico  30560  elsx  30859  br2base  30933  dya2iocnrect  30945  sxbrsigalem5  30952  sibf0  30998  cvmlift2lem13  31900
 Copyright terms: Public domain W3C validator