Theorem xpeq2 5653

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {copab 5162   × cxp 5630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-opab 5163  df-xp 5638

This theorem is referenced by:  xpeq12  5657  xpeq2i  5659  xpeq2d  5662  xpnz  6125  xpdisj2  6128  dmxpss  6137  rnxpid  6139  xpcan  6142  unixp  6248  dfpo2  6262  fconst5  7162  naddcllem  8614  pmvalg  8786  xpcomeng  9009  unxpdom  9171  marypha1  9349  djueq12  9828  dfac5lem3  10047  dfac5lem4  10048  dfac5lem4OLD  10050  hsmexlem8  10346  axdc4uz  13919  hashxp  14369  mamufval  22348  txuni2  23521  txbas  23523  txopn  23558  txrest  23587  txdis  23588  txdis1cn  23591  txtube  23596  txcmplem2  23598  tx1stc  23606  qustgplem  24077  tsmsxplem1  24109  isgrpo  30585  vciOLD  30649  isvclem  30665  issh  31296  hhssablo  31351  hhssnvt  31353  hhsssh  31357  2ndimaxp  32736  txomap  34012  tpr2rico  34090  elsx  34372  mbfmcst  34437  br2base  34447  dya2iocnrect  34459  sxbrsigalem5  34466  0rrv  34629  elima4  35992  finxpeq1  37641  isbnd3  38035  hdmap1fval  42172  csbresgVD  45250  mofeu  49207  functermc  49867