Theorem xpeq2 5672

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144  {copab 5166   × cxp 5649

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-opab 5167  df-xp 5657

This theorem is used by:  xpeq12  5676  xpeq2i  5678  xpeq2d  5681  xpnz  6152  xpdisj2  6155  dmxpss  6165  rnxpid  6167  xpcan  6170  unixp  6288  dfpo2  6302  fconst5  7216  naddcllem  8692  pmvalg  8864  xpcomeng  9095  unxpdom  9257  marypha1  9433  djueq12  9992  dfac5lem3  10211  dfac5lem4  10212  hsmexlem8  10509  axdc4uz  14134  hashxp  14586  mamufval  22716  txuni2  23893  txbas  23895  txopn  23930  txrest  23959  txdis  23960  txdis1cn  23963  txtube  23968  txcmplem2  23970  tx1stc  23978  qustgplem  24449  tsmsxplem1  24481  isgrpo  31108  vciOLD  31172  isvclem  31188  issh  31819  hhssablo  31874  hhssnvt  31876  hhsssh  31880  2ndimaxp  33291  txomap  34516  tpr2rico  34594  elsx  34877  mbfmcst  34941  br2base  34951  dya2iocnrect  34963  sxbrsigalem5  34970  0rrv  35133  elima4  36636  finxpeq1  38418  isbnd3  38827  hdmap1fval  42962  csbresgVD  45985  mofeu  50067  functermc  50751