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

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1539   ∈ wcel 2104  {copab 5211   × cxp 5675

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  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  7210  naddcllem  8679  pmvalg  8835  xpcomeng  9068  unxpdom  9257  marypha1  9433  djueq12  9903  dfac5lem3  10124  dfac5lem4  10125  hsmexlem8  10423  axdc4uz  13955  hashxp  14400  mamufval  22109  txuni2  23291  txbas  23293  txopn  23328  txrest  23357  txdis  23358  txdis1cn  23361  txtube  23366  txcmplem2  23368  tx1stc  23376  qustgplem  23847  tsmsxplem1  23879  isgrpo  30015  vciOLD  30079  isvclem  30095  issh  30726  hhssablo  30781  hhssnvt  30783  hhsssh  30787  2ndimaxp  32137  txomap  33110  tpr2rico  33188  elsx  33488  mbfmcst  33554  br2base  33564  dya2iocnrect  33576  sxbrsigalem5  33583  0rrv  33746  elima4  35049  finxpeq1  36572  isbnd3  36957  hdmap1fval  40972  csbresgVD  43960  mofeu  47603