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

Theorem xpeq1 4636
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 2241 . . . 4 (𝐴 = 𝐵 → (𝑥𝐴𝑥𝐵))
21anbi1d 465 . . 3 (𝐴 = 𝐵 → ((𝑥𝐴𝑦𝐶) ↔ (𝑥𝐵𝑦𝐶)))
32opabbidv 4066 . 2 (𝐴 = 𝐵 → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)})
4 df-xp 4628 . 2 (𝐴 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)}
5 df-xp 4628 . 2 (𝐵 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)}
63, 4, 53eqtr4g 2235 1 (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104   = wceq 1353  wcel 2148  {copab 4060   × cxp 4620
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-opab 4062  df-xp 4628
This theorem is referenced by:  xpeq12  4641  xpeq1i  4642  xpeq1d  4645  opthprc  4673  reseq2  4897  xpeq0r  5046  xpdisj1  5048  xpima1  5070  pmvalg  6652  xpsneng  6815  xpcomeng  6821  xpdom2g  6825  xpfi  6922  exmidomni  7133  exmidfodomrlemim  7193  hashxp  10777  txuni2  13389  txbas  13391  txopn  13398  txrest  13409  txdis  13410  txdis1cn  13411  xmettxlem  13642  xmettx  13643
  Copyright terms: Public domain W3C validator