Theorem xpeq2 5652

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

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

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 5165  df-xp 5637

This theorem is referenced by:  xpeq12  5656  xpeq2i  5658  xpeq2d  5661  xpnz  6120  xpdisj2  6123  dmxpss  6132  rnxpid  6134  xpcan  6137  unixp  6243  dfpo2  6257  fconst5  7162  naddcllem  8617  pmvalg  8787  xpcomeng  9010  unxpdom  9176  marypha1  9361  djueq12  9833  dfac5lem3  10054  dfac5lem4  10055  dfac5lem4OLD  10057  hsmexlem8  10353  axdc4uz  13925  hashxp  14375  mamufval  22255  txuni2  23428  txbas  23430  txopn  23465  txrest  23494  txdis  23495  txdis1cn  23498  txtube  23503  txcmplem2  23505  tx1stc  23513  qustgplem  23984  tsmsxplem1  24016  isgrpo  30399  vciOLD  30463  isvclem  30479  issh  31110  hhssablo  31165  hhssnvt  31167  hhsssh  31171  2ndimaxp  32543  txomap  33797  tpr2rico  33875  elsx  34157  mbfmcst  34223  br2base  34233  dya2iocnrect  34245  sxbrsigalem5  34252  0rrv  34415  elima4  35736  finxpeq1  37347  isbnd3  37751  hdmap1fval  41763  csbresgVD  44857  mofeu  48809  functermc  49470