Theorem xpeq2 5721

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2108  {copab 5228   × cxp 5698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-opab 5229  df-xp 5706

This theorem is referenced by:  xpeq12  5725  xpeq2i  5727  xpeq2d  5730  xpnz  6190  xpdisj2  6193  dmxpss  6202  rnxpid  6204  xpcan  6207  unixp  6313  dfpo2  6327  fconst5  7243  naddcllem  8732  pmvalg  8895  xpcomeng  9130  unxpdom  9316  marypha1  9503  djueq12  9973  dfac5lem3  10194  dfac5lem4  10195  dfac5lem4OLD  10197  hsmexlem8  10493  axdc4uz  14035  hashxp  14483  mamufval  22417  txuni2  23594  txbas  23596  txopn  23631  txrest  23660  txdis  23661  txdis1cn  23664  txtube  23669  txcmplem2  23671  tx1stc  23679  qustgplem  24150  tsmsxplem1  24182  isgrpo  30529  vciOLD  30593  isvclem  30609  issh  31240  hhssablo  31295  hhssnvt  31297  hhsssh  31301  2ndimaxp  32665  txomap  33780  tpr2rico  33858  elsx  34158  mbfmcst  34224  br2base  34234  dya2iocnrect  34246  sxbrsigalem5  34253  0rrv  34416  elima4  35739  finxpeq1  37352  isbnd3  37744  hdmap1fval  41753  csbresgVD  44866  mofeu  48561