Theorem xpeq2 5540

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111  {copab 5092   × cxp 5517

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-opab 5093  df-xp 5525

This theorem is referenced by:  xpeq12  5544  xpeq2i  5546  xpeq2d  5549  xpnz  5983  xpdisj2  5986  dmxpss  5995  rnxpid  5997  xpcan  6000  unixp  6101  fconst5  6945  pmvalg  8400  xpcomeng  8592  unxpdom  8709  marypha1  8882  djueq12  9317  dfac5lem3  9536  dfac5lem4  9537  hsmexlem8  9835  axdc4uz  13347  hashxp  13791  mamufval  20992  txuni2  22170  txbas  22172  txopn  22207  txrest  22236  txdis  22237  txdis1cn  22240  txtube  22245  txcmplem2  22247  tx1stc  22255  qustgplem  22726  tsmsxplem1  22758  isgrpo  28280  vciOLD  28344  isvclem  28360  issh  28991  hhssablo  29046  hhssnvt  29048  hhsssh  29052  2ndimaxp  30409  txomap  31187  tpr2rico  31265  elsx  31563  mbfmcst  31627  br2base  31637  dya2iocnrect  31649  sxbrsigalem5  31656  0rrv  31819  dfpo2  33104  elima4  33132  finxpeq1  34803  isbnd3  35222  hdmap1fval  39092  csbresgVD  41601