Theorem xpeq2 5697

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107  {copab 5210   × cxp 5674

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-opab 5211  df-xp 5682

This theorem is referenced by:  xpeq12  5701  xpeq2i  5703  xpeq2d  5706  xpnz  6156  xpdisj2  6159  dmxpss  6168  rnxpid  6170  xpcan  6173  unixp  6279  dfpo2  6293  fconst5  7204  naddcllem  8672  pmvalg  8828  xpcomeng  9061  unxpdom  9250  marypha1  9426  djueq12  9896  dfac5lem3  10117  dfac5lem4  10118  hsmexlem8  10416  axdc4uz  13946  hashxp  14391  mamufval  21879  txuni2  23061  txbas  23063  txopn  23098  txrest  23127  txdis  23128  txdis1cn  23131  txtube  23136  txcmplem2  23138  tx1stc  23146  qustgplem  23617  tsmsxplem1  23649  isgrpo  29738  vciOLD  29802  isvclem  29818  issh  30449  hhssablo  30504  hhssnvt  30506  hhsssh  30510  2ndimaxp  31860  txomap  32803  tpr2rico  32881  elsx  33181  mbfmcst  33247  br2base  33257  dya2iocnrect  33269  sxbrsigalem5  33276  0rrv  33439  elima4  34736  finxpeq1  36256  isbnd3  36641  hdmap1fval  40656  csbresgVD  43642  mofeu  47468