Theorem xpeq2 5675

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 5185	. 2 ⊢ (𝐴 = 𝐵 → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐴)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐵)})
4		df-xp 5660	. 2 ⊢ (𝐶 × 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐴)}
5		df-xp 5660	. 2 ⊢ (𝐶 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐵)}
6	3, 4, 5	3eqtr4g 2795	1 ⊢ (𝐴 = 𝐵 → (𝐶 × 𝐴) = (𝐶 × 𝐵))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  {copab 5181   × cxp 5652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-opab 5182  df-xp 5660

This theorem is referenced by:  xpeq12  5679  xpeq2i  5681  xpeq2d  5684  xpnz  6148  xpdisj2  6151  dmxpss  6160  rnxpid  6162  xpcan  6165  unixp  6271  dfpo2  6285  fconst5  7198  naddcllem  8688  pmvalg  8851  xpcomeng  9078  unxpdom  9261  marypha1  9446  djueq12  9918  dfac5lem3  10139  dfac5lem4  10140  dfac5lem4OLD  10142  hsmexlem8  10438  axdc4uz  14002  hashxp  14452  mamufval  22330  txuni2  23503  txbas  23505  txopn  23540  txrest  23569  txdis  23570  txdis1cn  23573  txtube  23578  txcmplem2  23580  tx1stc  23588  qustgplem  24059  tsmsxplem1  24091  isgrpo  30478  vciOLD  30542  isvclem  30558  issh  31189  hhssablo  31244  hhssnvt  31246  hhsssh  31250  2ndimaxp  32624  txomap  33865  tpr2rico  33943  elsx  34225  mbfmcst  34291  br2base  34301  dya2iocnrect  34313  sxbrsigalem5  34320  0rrv  34483  elima4  35793  finxpeq1  37404  isbnd3  37808  hdmap1fval  41815  csbresgVD  44919  mofeu  48826  functermc  49393