Theorem xpeq2 5659

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {copab 5169   × cxp 5636

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-opab 5170  df-xp 5644

This theorem is referenced by:  xpeq12  5663  xpeq2i  5665  xpeq2d  5668  xpnz  6132  xpdisj2  6135  dmxpss  6144  rnxpid  6146  xpcan  6149  unixp  6255  dfpo2  6269  fconst5  7180  naddcllem  8640  pmvalg  8810  xpcomeng  9033  unxpdom  9200  marypha1  9385  djueq12  9857  dfac5lem3  10078  dfac5lem4  10079  dfac5lem4OLD  10081  hsmexlem8  10377  axdc4uz  13949  hashxp  14399  mamufval  22279  txuni2  23452  txbas  23454  txopn  23489  txrest  23518  txdis  23519  txdis1cn  23522  txtube  23527  txcmplem2  23529  tx1stc  23537  qustgplem  24008  tsmsxplem1  24040  isgrpo  30426  vciOLD  30490  isvclem  30506  issh  31137  hhssablo  31192  hhssnvt  31194  hhsssh  31198  2ndimaxp  32570  txomap  33824  tpr2rico  33902  elsx  34184  mbfmcst  34250  br2base  34260  dya2iocnrect  34272  sxbrsigalem5  34279  0rrv  34442  elima4  35763  finxpeq1  37374  isbnd3  37778  hdmap1fval  41790  csbresgVD  44884  mofeu  48836  functermc  49497