Theorem xpeq2 5662

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {copab 5172   × cxp 5639

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-opab 5173  df-xp 5647

This theorem is referenced by:  xpeq12  5666  xpeq2i  5668  xpeq2d  5671  xpnz  6135  xpdisj2  6138  dmxpss  6147  rnxpid  6149  xpcan  6152  unixp  6258  dfpo2  6272  fconst5  7183  naddcllem  8643  pmvalg  8813  xpcomeng  9038  unxpdom  9207  marypha1  9392  djueq12  9864  dfac5lem3  10085  dfac5lem4  10086  dfac5lem4OLD  10088  hsmexlem8  10384  axdc4uz  13956  hashxp  14406  mamufval  22286  txuni2  23459  txbas  23461  txopn  23496  txrest  23525  txdis  23526  txdis1cn  23529  txtube  23534  txcmplem2  23536  tx1stc  23544  qustgplem  24015  tsmsxplem1  24047  isgrpo  30433  vciOLD  30497  isvclem  30513  issh  31144  hhssablo  31199  hhssnvt  31201  hhsssh  31205  2ndimaxp  32577  txomap  33831  tpr2rico  33909  elsx  34191  mbfmcst  34257  br2base  34267  dya2iocnrect  34279  sxbrsigalem5  34286  0rrv  34449  elima4  35770  finxpeq1  37381  isbnd3  37785  hdmap1fval  41797  csbresgVD  44891  mofeu  48840  functermc  49501