Theorem xpeq2 5706

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  {copab 5205   × cxp 5683

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-opab 5206  df-xp 5691

This theorem is referenced by:  xpeq12  5710  xpeq2i  5712  xpeq2d  5715  xpnz  6179  xpdisj2  6182  dmxpss  6191  rnxpid  6193  xpcan  6196  unixp  6302  dfpo2  6316  fconst5  7226  naddcllem  8714  pmvalg  8877  xpcomeng  9104  unxpdom  9289  marypha1  9474  djueq12  9944  dfac5lem3  10165  dfac5lem4  10166  dfac5lem4OLD  10168  hsmexlem8  10464  axdc4uz  14025  hashxp  14473  mamufval  22396  txuni2  23573  txbas  23575  txopn  23610  txrest  23639  txdis  23640  txdis1cn  23643  txtube  23648  txcmplem2  23650  tx1stc  23658  qustgplem  24129  tsmsxplem1  24161  isgrpo  30516  vciOLD  30580  isvclem  30596  issh  31227  hhssablo  31282  hhssnvt  31284  hhsssh  31288  2ndimaxp  32656  txomap  33833  tpr2rico  33911  elsx  34195  mbfmcst  34261  br2base  34271  dya2iocnrect  34283  sxbrsigalem5  34290  0rrv  34453  elima4  35776  finxpeq1  37387  isbnd3  37791  hdmap1fval  41798  csbresgVD  44915  mofeu  48757  functermc  49140