Theorem xpeq2 5646

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {copab 5148   × cxp 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-opab 5149  df-xp 5631

This theorem is referenced by:  xpeq12  5650  xpeq2i  5652  xpeq2d  5655  xpnz  6118  xpdisj2  6121  dmxpss  6130  rnxpid  6132  xpcan  6135  unixp  6241  dfpo2  6255  fconst5  7155  naddcllem  8606  pmvalg  8778  xpcomeng  9001  unxpdom  9163  marypha1  9341  djueq12  9822  dfac5lem3  10041  dfac5lem4  10042  dfac5lem4OLD  10044  hsmexlem8  10340  axdc4uz  13940  hashxp  14390  mamufval  22370  txuni2  23543  txbas  23545  txopn  23580  txrest  23609  txdis  23610  txdis1cn  23613  txtube  23618  txcmplem2  23620  tx1stc  23628  qustgplem  24099  tsmsxplem1  24131  isgrpo  30586  vciOLD  30650  isvclem  30666  issh  31297  hhssablo  31352  hhssnvt  31354  hhsssh  31358  2ndimaxp  32737  txomap  33997  tpr2rico  34075  elsx  34357  mbfmcst  34422  br2base  34432  dya2iocnrect  34444  sxbrsigalem5  34451  0rrv  34614  elima4  35977  finxpeq1  37719  isbnd3  38122  hdmap1fval  42259  csbresgVD  45342  mofeu  49338  functermc  49998