Theorem xpeq2 5695

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

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1534   ∈ wcel 2099  {copab 5207   × cxp 5672

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-opab 5208  df-xp 5680

This theorem is referenced by:  xpeq12  5699  xpeq2i  5701  xpeq2d  5704  xpnz  6162  xpdisj2  6165  dmxpss  6174  rnxpid  6176  xpcan  6179  unixp  6285  dfpo2  6299  fconst5  7215  naddcllem  8698  pmvalg  8858  xpcomeng  9094  unxpdom  9280  marypha1  9470  djueq12  9940  dfac5lem3  10161  dfac5lem4  10162  hsmexlem8  10458  axdc4uz  13998  hashxp  14446  mamufval  22380  txuni2  23557  txbas  23559  txopn  23594  txrest  23623  txdis  23624  txdis1cn  23627  txtube  23632  txcmplem2  23634  tx1stc  23642  qustgplem  24113  tsmsxplem1  24145  isgrpo  30427  vciOLD  30491  isvclem  30507  issh  31138  hhssablo  31193  hhssnvt  31195  hhsssh  31199  2ndimaxp  32564  txomap  33662  tpr2rico  33740  elsx  34040  mbfmcst  34106  br2base  34116  dya2iocnrect  34128  sxbrsigalem5  34135  0rrv  34298  elima4  35612  finxpeq1  37106  isbnd3  37498  hdmap1fval  41508  csbresgVD  44608  mofeu  48251