Theorem xpeq2 5661

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-opab 5172  df-xp 5646

This theorem is referenced by:  xpeq12  5665  xpeq2i  5667  xpeq2d  5670  xpnz  6134  xpdisj2  6137  dmxpss  6146  rnxpid  6148  xpcan  6151  unixp  6257  dfpo2  6271  fconst5  7182  naddcllem  8642  pmvalg  8812  xpcomeng  9037  unxpdom  9206  marypha1  9391  djueq12  9863  dfac5lem3  10084  dfac5lem4  10085  dfac5lem4OLD  10087  hsmexlem8  10383  axdc4uz  13955  hashxp  14405  mamufval  22285  txuni2  23458  txbas  23460  txopn  23495  txrest  23524  txdis  23525  txdis1cn  23528  txtube  23533  txcmplem2  23535  tx1stc  23543  qustgplem  24014  tsmsxplem1  24046  isgrpo  30432  vciOLD  30496  isvclem  30512  issh  31143  hhssablo  31198  hhssnvt  31200  hhsssh  31204  2ndimaxp  32576  txomap  33830  tpr2rico  33908  elsx  34190  mbfmcst  34256  br2base  34266  dya2iocnrect  34278  sxbrsigalem5  34285  0rrv  34448  elima4  35758  finxpeq1  37369  isbnd3  37773  hdmap1fval  41785  csbresgVD  44877  mofeu  48826  functermc  49487