Theorem xpeq2 5640

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 2817	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵))
2	1	anbi2d 630	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐴) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐵)))
3	2	opabbidv 5158	. 2 ⊢ (𝐴 = 𝐵 → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐴)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐵)})
4		df-xp 5625	. 2 ⊢ (𝐶 × 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐴)}
5		df-xp 5625	. 2 ⊢ (𝐶 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐵)}
6	3, 4, 5	3eqtr4g 2789	1 ⊢ (𝐴 = 𝐵 → (𝐶 × 𝐴) = (𝐶 × 𝐵))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {copab 5154   × cxp 5617

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-opab 5155  df-xp 5625

This theorem is referenced by:  xpeq12  5644  xpeq2i  5646  xpeq2d  5649  xpnz  6108  xpdisj2  6111  dmxpss  6120  rnxpid  6122  xpcan  6125  unixp  6230  dfpo2  6244  fconst5  7142  naddcllem  8594  pmvalg  8764  xpcomeng  8986  unxpdom  9148  marypha1  9324  djueq12  9800  dfac5lem3  10019  dfac5lem4  10020  dfac5lem4OLD  10022  hsmexlem8  10318  axdc4uz  13891  hashxp  14341  mamufval  22277  txuni2  23450  txbas  23452  txopn  23487  txrest  23516  txdis  23517  txdis1cn  23520  txtube  23525  txcmplem2  23527  tx1stc  23535  qustgplem  24006  tsmsxplem1  24038  isgrpo  30441  vciOLD  30505  isvclem  30521  issh  31152  hhssablo  31207  hhssnvt  31209  hhsssh  31213  2ndimaxp  32589  txomap  33801  tpr2rico  33879  elsx  34161  mbfmcst  34227  br2base  34237  dya2iocnrect  34249  sxbrsigalem5  34256  0rrv  34419  elima4  35749  finxpeq1  37360  isbnd3  37764  hdmap1fval  41775  csbresgVD  44868  mofeu  48832  functermc  49493