Theorem xpeq2 5682

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143  {copab 5173   × cxp 5659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-opab 5174  df-xp 5667

This theorem is referenced by:  xpeq12  5686  xpeq2i  5688  xpeq2d  5691  xpnz  6156  xpdisj2  6159  dmxpss  6169  rnxpid  6171  xpcan  6174  unixp  6283  dfpo2  6297  fconst5  7204  naddcllem  8658  pmvalg  8830  xpcomeng  9053  unxpdom  9215  marypha1  9390  djueq12  9886  dfac5lem3  10105  dfac5lem4  10106  hsmexlem8  10403  axdc4uz  14016  hashxp  14467  mamufval  22549  txuni2  23722  txbas  23724  txopn  23759  txrest  23788  txdis  23789  txdis1cn  23792  txtube  23797  txcmplem2  23799  tx1stc  23807  qustgplem  24278  tsmsxplem1  24310  isgrpo  30849  vciOLD  30913  isvclem  30929  issh  31560  hhssablo  31615  hhssnvt  31617  hhsssh  31621  2ndimaxp  32991  txomap  34224  tpr2rico  34302  elsx  34584  mbfmcst  34649  br2base  34659  dya2iocnrect  34671  sxbrsigalem5  34678  0rrv  34841  elima4  36268  finxpeq1  38032  isbnd3  38435  hdmap1fval  42570  csbresgVD  45603  mofeu  49626  functermc  50286