Theorem xpeq2 5698

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

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

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 5212  df-xp 5683

This theorem is referenced by:  xpeq12  5702  xpeq2i  5704  xpeq2d  5707  xpnz  6159  xpdisj2  6162  dmxpss  6171  rnxpid  6173  xpcan  6176  unixp  6282  dfpo2  6296  fconst5  7207  naddcllem  8675  pmvalg  8831  xpcomeng  9064  unxpdom  9253  marypha1  9429  djueq12  9899  dfac5lem3  10120  dfac5lem4  10121  hsmexlem8  10419  axdc4uz  13949  hashxp  14394  mamufval  21887  txuni2  23069  txbas  23071  txopn  23106  txrest  23135  txdis  23136  txdis1cn  23139  txtube  23144  txcmplem2  23146  tx1stc  23154  qustgplem  23625  tsmsxplem1  23657  isgrpo  29750  vciOLD  29814  isvclem  29830  issh  30461  hhssablo  30516  hhssnvt  30518  hhsssh  30522  2ndimaxp  31872  txomap  32814  tpr2rico  32892  elsx  33192  mbfmcst  33258  br2base  33268  dya2iocnrect  33280  sxbrsigalem5  33287  0rrv  33450  elima4  34747  finxpeq1  36267  isbnd3  36652  hdmap1fval  40667  csbresgVD  43656  mofeu  47514