Theorem xpeq2 5709

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1536   ∈ wcel 2105  {copab 5209   × cxp 5686

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-opab 5210  df-xp 5694

This theorem is referenced by:  xpeq12  5713  xpeq2i  5715  xpeq2d  5718  xpnz  6180  xpdisj2  6183  dmxpss  6192  rnxpid  6194  xpcan  6197  unixp  6303  dfpo2  6317  fconst5  7225  naddcllem  8712  pmvalg  8875  xpcomeng  9102  unxpdom  9286  marypha1  9471  djueq12  9941  dfac5lem3  10162  dfac5lem4  10163  dfac5lem4OLD  10165  hsmexlem8  10461  axdc4uz  14021  hashxp  14469  mamufval  22411  txuni2  23588  txbas  23590  txopn  23625  txrest  23654  txdis  23655  txdis1cn  23658  txtube  23663  txcmplem2  23665  tx1stc  23673  qustgplem  24144  tsmsxplem1  24176  isgrpo  30525  vciOLD  30589  isvclem  30605  issh  31236  hhssablo  31291  hhssnvt  31293  hhsssh  31297  2ndimaxp  32662  txomap  33794  tpr2rico  33872  elsx  34174  mbfmcst  34240  br2base  34250  dya2iocnrect  34262  sxbrsigalem5  34269  0rrv  34432  elima4  35756  finxpeq1  37368  isbnd3  37770  hdmap1fval  41778  csbresgVD  44892  mofeu  48677