Theorem xpeq2 5652

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

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

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 5165  df-xp 5637

This theorem is referenced by:  xpeq12  5656  xpeq2i  5658  xpeq2d  5661  xpnz  6120  xpdisj2  6123  dmxpss  6132  rnxpid  6134  xpcan  6137  unixp  6243  dfpo2  6257  fconst5  7162  naddcllem  8617  pmvalg  8787  xpcomeng  9010  unxpdom  9176  marypha1  9361  djueq12  9833  dfac5lem3  10054  dfac5lem4  10055  dfac5lem4OLD  10057  hsmexlem8  10353  axdc4uz  13925  hashxp  14375  mamufval  22312  txuni2  23485  txbas  23487  txopn  23522  txrest  23551  txdis  23552  txdis1cn  23555  txtube  23560  txcmplem2  23562  tx1stc  23570  qustgplem  24041  tsmsxplem1  24073  isgrpo  30476  vciOLD  30540  isvclem  30556  issh  31187  hhssablo  31242  hhssnvt  31244  hhsssh  31248  2ndimaxp  32620  txomap  33817  tpr2rico  33895  elsx  34177  mbfmcst  34243  br2base  34253  dya2iocnrect  34265  sxbrsigalem5  34272  0rrv  34435  elima4  35756  finxpeq1  37367  isbnd3  37771  hdmap1fval  41783  csbresgVD  44877  mofeu  48829  functermc  49490