Theorem xpeq2 5601

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2108  {copab 5132   × cxp 5578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-opab 5133  df-xp 5586

This theorem is referenced by:  xpeq12  5605  xpeq2i  5607  xpeq2d  5610  xpnz  6051  xpdisj2  6054  dmxpss  6063  rnxpid  6065  xpcan  6068  unixp  6174  dfpo2  6188  fconst5  7063  pmvalg  8584  xpcomeng  8804  unxpdom  8959  marypha1  9123  djueq12  9593  dfac5lem3  9812  dfac5lem4  9813  hsmexlem8  10111  axdc4uz  13632  hashxp  14077  mamufval  21444  txuni2  22624  txbas  22626  txopn  22661  txrest  22690  txdis  22691  txdis1cn  22694  txtube  22699  txcmplem2  22701  tx1stc  22709  qustgplem  23180  tsmsxplem1  23212  isgrpo  28760  vciOLD  28824  isvclem  28840  issh  29471  hhssablo  29526  hhssnvt  29528  hhsssh  29532  2ndimaxp  30885  txomap  31686  tpr2rico  31764  elsx  32062  mbfmcst  32126  br2base  32136  dya2iocnrect  32148  sxbrsigalem5  32155  0rrv  32318  elima4  33656  naddcllem  33758  finxpeq1  35484  isbnd3  35869  hdmap1fval  39737  csbresgVD  42404  mofeu  46063