Theorem xpeq2 5684

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146  {copab 5175   × cxp 5661

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-opab 5176  df-xp 5669

This theorem is used by:  xpeq12  5688  xpeq2i  5690  xpeq2d  5693  xpnz  6158  xpdisj2  6161  dmxpss  6171  rnxpid  6173  xpcan  6176  unixp  6287  dfpo2  6301  fconst5  7211  naddcllem  8668  pmvalg  8840  xpcomeng  9064  unxpdom  9226  marypha1  9401  djueq12  9906  dfac5lem3  10125  dfac5lem4  10126  hsmexlem8  10423  axdc4uz  14038  hashxp  14489  mamufval  22599  txuni2  23773  txbas  23775  txopn  23810  txrest  23839  txdis  23840  txdis1cn  23843  txtube  23848  txcmplem2  23850  tx1stc  23858  qustgplem  24329  tsmsxplem1  24361  isgrpo  30920  vciOLD  30984  isvclem  31000  issh  31631  hhssablo  31686  hhssnvt  31688  hhsssh  31692  2ndimaxp  33062  txomap  34288  tpr2rico  34366  elsx  34649  mbfmcst  34714  br2base  34724  dya2iocnrect  34736  sxbrsigalem5  34743  0rrv  34906  elima4  36305  finxpeq1  38089  isbnd3  38493  hdmap1fval  42628  csbresgVD  45661  mofeu  49683  functermc  50343