Theorem xpeq2 5610

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2106  {copab 5136   × cxp 5587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-opab 5137  df-xp 5595

This theorem is referenced by:  xpeq12  5614  xpeq2i  5616  xpeq2d  5619  xpnz  6062  xpdisj2  6065  dmxpss  6074  rnxpid  6076  xpcan  6079  unixp  6185  dfpo2  6199  fconst5  7081  pmvalg  8626  xpcomeng  8851  unxpdom  9030  marypha1  9193  djueq12  9662  dfac5lem3  9881  dfac5lem4  9882  hsmexlem8  10180  axdc4uz  13704  hashxp  14149  mamufval  21534  txuni2  22716  txbas  22718  txopn  22753  txrest  22782  txdis  22783  txdis1cn  22786  txtube  22791  txcmplem2  22793  tx1stc  22801  qustgplem  23272  tsmsxplem1  23304  isgrpo  28859  vciOLD  28923  isvclem  28939  issh  29570  hhssablo  29625  hhssnvt  29627  hhsssh  29631  2ndimaxp  30984  txomap  31784  tpr2rico  31862  elsx  32162  mbfmcst  32226  br2base  32236  dya2iocnrect  32248  sxbrsigalem5  32255  0rrv  32418  elima4  33750  naddcllem  33831  finxpeq1  35557  isbnd3  35942  hdmap1fval  39810  csbresgVD  42515  mofeu  46175