Theorem xpeq2 5672

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  {copab 5167   × cxp 5649

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-opab 5168  df-xp 5657

This theorem is used by:  xpeq12  5676  xpeq2i  5678  xpeq2d  5681  xpnz  6150  xpdisj2  6153  dmxpss  6163  rnxpid  6165  xpcan  6168  unixp  6284  dfpo2  6298  fconst5  7210  naddcllem  8678  pmvalg  8850  xpcomeng  9081  unxpdom  9243  marypha1  9419  djueq12  9978  dfac5lem3  10197  dfac5lem4  10198  hsmexlem8  10495  axdc4uz  14120  hashxp  14572  mamufval  22700  txuni2  23877  txbas  23879  txopn  23914  txrest  23943  txdis  23944  txdis1cn  23947  txtube  23952  txcmplem2  23954  tx1stc  23962  qustgplem  24433  tsmsxplem1  24465  isgrpo  31092  vciOLD  31156  isvclem  31172  issh  31803  hhssablo  31858  hhssnvt  31860  hhsssh  31864  2ndimaxp  33233  txomap  34459  tpr2rico  34537  elsx  34820  mbfmcst  34884  br2base  34894  dya2iocnrect  34906  sxbrsigalem5  34913  0rrv  35076  elima4  36520  finxpeq1  38289  isbnd3  38698  hdmap1fval  42833  csbresgVD  45862  mofeu  49927  functermc  50585