Theorem xpeq2 5635

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2111  {copab 5151   × cxp 5612

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-opab 5152  df-xp 5620

This theorem is referenced by:  xpeq12  5639  xpeq2i  5641  xpeq2d  5644  xpnz  6106  xpdisj2  6109  dmxpss  6118  rnxpid  6120  xpcan  6123  unixp  6229  dfpo2  6243  fconst5  7140  naddcllem  8591  pmvalg  8761  xpcomeng  8982  unxpdom  9143  marypha1  9318  djueq12  9797  dfac5lem3  10016  dfac5lem4  10017  dfac5lem4OLD  10019  hsmexlem8  10315  axdc4uz  13891  hashxp  14341  mamufval  22307  txuni2  23480  txbas  23482  txopn  23517  txrest  23546  txdis  23547  txdis1cn  23550  txtube  23555  txcmplem2  23557  tx1stc  23565  qustgplem  24036  tsmsxplem1  24068  isgrpo  30477  vciOLD  30541  isvclem  30557  issh  31188  hhssablo  31243  hhssnvt  31245  hhsssh  31249  2ndimaxp  32628  txomap  33847  tpr2rico  33925  elsx  34207  mbfmcst  34272  br2base  34282  dya2iocnrect  34294  sxbrsigalem5  34301  0rrv  34464  elima4  35820  finxpeq1  37428  isbnd3  37832  hdmap1fval  41843  csbresgVD  44935  mofeu  48887  functermc  49548