Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  xpeq1 GIF version

Theorem xpeq1 4562
 Description: Equality theorem for cross 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 2204 . . . 4 (𝐴 = 𝐵 → (𝑥𝐴𝑥𝐵))
21anbi1d 461 . . 3 (𝐴 = 𝐵 → ((𝑥𝐴𝑦𝐶) ↔ (𝑥𝐵𝑦𝐶)))
32opabbidv 4003 . 2 (𝐴 = 𝐵 → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)})
4 df-xp 4554 . 2 (𝐴 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)}
5 df-xp 4554 . 2 (𝐵 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)}
63, 4, 53eqtr4g 2198 1 (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   = wceq 1332   ∈ wcel 1481  {copab 3997   × cxp 4546 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-11 1485  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122 This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-opab 3999  df-xp 4554 This theorem is referenced by:  xpeq12  4567  xpeq1i  4568  xpeq1d  4571  opthprc  4599  reseq2  4823  xpeq0r  4970  xpdisj1  4972  xpima1  4994  pmvalg  6562  xpsneng  6725  xpcomeng  6731  xpdom2g  6735  xpfi  6828  exmidomni  7024  exmidfodomrlemim  7077  hashxp  10624  txuni2  12484  txbas  12486  txopn  12493  txrest  12504  txdis  12505  txdis1cn  12506  xmettxlem  12737  xmettx  12738
 Copyright terms: Public domain W3C validator