Theorem xpeq2 5643

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  {copab 5158   × cxp 5620

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-opab 5159  df-xp 5628

This theorem is referenced by:  xpeq12  5647  xpeq2i  5649  xpeq2d  5652  xpnz  6115  xpdisj2  6118  dmxpss  6127  rnxpid  6129  xpcan  6132  unixp  6238  dfpo2  6252  fconst5  7150  naddcllem  8602  pmvalg  8772  xpcomeng  8995  unxpdom  9157  marypha1  9335  djueq12  9814  dfac5lem3  10033  dfac5lem4  10034  dfac5lem4OLD  10036  hsmexlem8  10332  axdc4uz  13905  hashxp  14355  mamufval  22334  txuni2  23507  txbas  23509  txopn  23544  txrest  23573  txdis  23574  txdis1cn  23577  txtube  23582  txcmplem2  23584  tx1stc  23592  qustgplem  24063  tsmsxplem1  24095  isgrpo  30521  vciOLD  30585  isvclem  30601  issh  31232  hhssablo  31287  hhssnvt  31289  hhsssh  31293  2ndimaxp  32673  txomap  33940  tpr2rico  34018  elsx  34300  mbfmcst  34365  br2base  34375  dya2iocnrect  34387  sxbrsigalem5  34394  0rrv  34557  elima4  35919  finxpeq1  37530  isbnd3  37924  hdmap1fval  41995  csbresgVD  45077  mofeu  49035  functermc  49695