Theorem xpeq2 5645

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  {copab 5160   × cxp 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-opab 5161  df-xp 5630

This theorem is referenced by:  xpeq12  5649  xpeq2i  5651  xpeq2d  5654  xpnz  6117  xpdisj2  6120  dmxpss  6129  rnxpid  6131  xpcan  6134  unixp  6240  dfpo2  6254  fconst5  7152  naddcllem  8604  pmvalg  8774  xpcomeng  8997  unxpdom  9159  marypha1  9337  djueq12  9816  dfac5lem3  10035  dfac5lem4  10036  dfac5lem4OLD  10038  hsmexlem8  10334  axdc4uz  13907  hashxp  14357  mamufval  22336  txuni2  23509  txbas  23511  txopn  23546  txrest  23575  txdis  23576  txdis1cn  23579  txtube  23584  txcmplem2  23586  tx1stc  23594  qustgplem  24065  tsmsxplem1  24097  isgrpo  30572  vciOLD  30636  isvclem  30652  issh  31283  hhssablo  31338  hhssnvt  31340  hhsssh  31344  2ndimaxp  32724  txomap  33991  tpr2rico  34069  elsx  34351  mbfmcst  34416  br2base  34426  dya2iocnrect  34438  sxbrsigalem5  34445  0rrv  34608  elima4  35970  finxpeq1  37591  isbnd3  37985  hdmap1fval  42056  csbresgVD  45135  mofeu  49093  functermc  49753