Theorem xpeq2 5683

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567   ∈ wcel 2149  {copab 5177   × cxp 5660

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-opab 5178  df-xp 5668

This theorem is referenced by:  xpeq12  5687  xpeq2i  5689  xpeq2d  5692  xpnz  6157  xpdisj2  6160  dmxpss  6170  rnxpid  6172  xpcan  6175  unixp  6284  dfpo2  6298  fconst5  7205  naddcllem  8661  pmvalg  8833  xpcomeng  9056  unxpdom  9218  marypha1  9393  djueq12  9889  dfac5lem3  10108  dfac5lem4  10109  hsmexlem8  10407  axdc4uz  14019  hashxp  14470  mamufval  22517  txuni2  23690  txbas  23692  txopn  23727  txrest  23756  txdis  23757  txdis1cn  23760  txtube  23765  txcmplem2  23767  tx1stc  23775  qustgplem  24246  tsmsxplem1  24278  isgrpo  30789  vciOLD  30853  isvclem  30869  issh  31500  hhssablo  31555  hhssnvt  31557  hhsssh  31561  2ndimaxp  32931  txomap  34168  tpr2rico  34246  elsx  34528  mbfmcst  34593  br2base  34603  dya2iocnrect  34615  sxbrsigalem5  34622  0rrv  34785  elima4  36166  finxpeq1  37919  isbnd3  38322  hdmap1fval  42459  csbresgVD  45494  mofeu  49510  functermc  50170