Theorem xpeq2 5639

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119  {copab 5134   × cxp 5616

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-opab 5135  df-xp 5624

This theorem is referenced by:  xpeq12  5643  xpeq2i  5645  xpeq2d  5648  xpnz  6110  xpdisj2  6113  dmxpss  6122  rnxpid  6124  xpcan  6127  unixp  6233  dfpo2  6247  fconst5  7150  naddcllem  8602  pmvalg  8774  xpcomeng  8997  unxpdom  9159  marypha1  9337  djueq12  9819  dfac5lem3  10038  dfac5lem4  10039  dfac5lem4OLD  10041  hsmexlem8  10337  axdc4uz  13937  hashxp  14387  mamufval  22375  txuni2  23548  txbas  23550  txopn  23585  txrest  23614  txdis  23615  txdis1cn  23618  txtube  23623  txcmplem2  23625  tx1stc  23633  qustgplem  24104  tsmsxplem1  24136  isgrpo  30586  vciOLD  30650  isvclem  30666  issh  31297  hhssablo  31352  hhssnvt  31354  hhsssh  31358  2ndimaxp  32738  txomap  34018  tpr2rico  34096  elsx  34378  mbfmcst  34443  br2base  34453  dya2iocnrect  34465  sxbrsigalem5  34472  0rrv  34635  elima4  36004  finxpeq1  37748  isbnd3  38151  hdmap1fval  42288  csbresgVD  45338  mofeu  49338  functermc  49998