Theorem xpeq2 5668

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.

Step	Hyp	Ref	Expression
1		eleq2 2851	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵))
2	1	anbi2d 639	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐴) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐵)))
3	2	opabbidv 5166	. 2 ⊢ (𝐴 = 𝐵 → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐴)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐵)})
4		df-xp 5653	. 2 ⊢ (𝐶 × 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐴)}
5		df-xp 5653	. 2 ⊢ (𝐶 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐵)}
6	3, 4, 5	3eqtr4g 2822	1 ⊢ (𝐴 = 𝐵 → (𝐶 × 𝐴) = (𝐶 × 𝐵))

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1560   ∈ wcel 2142  {copab 5162   × cxp 5645

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-opab 5163  df-xp 5653

This theorem is referenced by:  xpeq12  5672  xpeq2i  5674  xpeq2d  5677  xpnz  6144  xpdisj2  6147  dmxpss  6157  rnxpid  6159  xpcan  6162  unixp  6269  dfpo2  6283  fconst5  7190  naddcllem  8646  pmvalg  8818  xpcomeng  9041  unxpdom  9203  marypha1  9380  djueq12  9862  dfac5lem3  10081  dfac5lem4  10082  dfac5lem4OLD  10084  hsmexlem8  10381  axdc4uz  13997  hashxp  14447  mamufval  22449  txuni2  23622  txbas  23624  txopn  23659  txrest  23688  txdis  23689  txdis1cn  23692  txtube  23697  txcmplem2  23699  tx1stc  23707  qustgplem  24178  tsmsxplem1  24210  isgrpo  30697  vciOLD  30761  isvclem  30777  issh  31408  hhssablo  31463  hhssnvt  31465  hhsssh  31469  2ndimaxp  32845  txomap  34128  tpr2rico  34206  elsx  34488  mbfmcst  34553  br2base  34563  dya2iocnrect  34575  sxbrsigalem5  34582  0rrv  34745  elima4  36123  finxpeq1  37877  isbnd3  38280  hdmap1fval  42417  csbresgVD  45467  mofeu  49466  functermc  50126