Theorem xpeq2 5578

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537   ∈ wcel 2114  {copab 5130   × cxp 5555

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-opab 5131  df-xp 5563

This theorem is referenced by:  xpeq12  5582  xpeq2i  5584  xpeq2d  5587  xpnz  6018  xpdisj2  6021  dmxpss  6030  rnxpid  6032  xpcan  6035  unixp  6135  fconst5  6970  pmvalg  8419  xpcomeng  8611  unxpdom  8727  marypha1  8900  djueq12  9335  dfac5lem3  9553  dfac5lem4  9554  hsmexlem8  9848  axdc4uz  13355  hashxp  13798  mamufval  20998  txuni2  22175  txbas  22177  txopn  22212  txrest  22241  txdis  22242  txdis1cn  22245  txtube  22250  txcmplem2  22252  tx1stc  22260  qustgplem  22731  tsmsxplem1  22763  isgrpo  28276  vciOLD  28340  isvclem  28356  issh  28987  hhssablo  29042  hhssnvt  29044  hhsssh  29048  txomap  31100  tpr2rico  31157  elsx  31455  mbfmcst  31519  br2base  31529  dya2iocnrect  31541  sxbrsigalem5  31548  0rrv  31711  dfpo2  32993  elima4  33021  finxpeq1  34669  isbnd3  35064  hdmap1fval  38934  csbresgVD  41236