Theorem xpeq2 5685

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146  {copab 5176   × cxp 5662

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-opab 5177  df-xp 5670

This theorem is used by:  xpeq12  5689  xpeq2i  5691  xpeq2d  5694  xpnz  6159  xpdisj2  6162  dmxpss  6172  rnxpid  6174  xpcan  6177  unixp  6287  dfpo2  6301  fconst5  7208  naddcllem  8664  pmvalg  8836  xpcomeng  9059  unxpdom  9221  marypha1  9396  djueq12  9901  dfac5lem3  10120  dfac5lem4  10121  hsmexlem8  10418  axdc4uz  14031  hashxp  14482  mamufval  22564  txuni2  23737  txbas  23739  txopn  23774  txrest  23803  txdis  23804  txdis1cn  23807  txtube  23812  txcmplem2  23814  tx1stc  23822  qustgplem  24293  tsmsxplem1  24325  isgrpo  30864  vciOLD  30928  isvclem  30944  issh  31575  hhssablo  31630  hhssnvt  31632  hhsssh  31636  2ndimaxp  33006  txomap  34237  tpr2rico  34315  elsx  34597  mbfmcst  34662  br2base  34672  dya2iocnrect  34684  sxbrsigalem5  34691  0rrv  34854  elima4  36280  finxpeq1  38064  isbnd3  38467  hdmap1fval  42602  csbresgVD  45635  mofeu  49658  functermc  50318