Theorem xpeq2 5676

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  {copab 5167   × cxp 5653

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 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-opab 5168  df-xp 5661

This theorem is used by:  xpeq12  5680  xpeq2i  5682  xpeq2d  5685  xpnz  6151  xpdisj2  6154  dmxpss  6164  rnxpid  6166  xpcan  6169  unixp  6280  dfpo2  6294  fconst5  7205  naddcllem  8664  pmvalg  8836  xpcomeng  9067  unxpdom  9229  marypha1  9404  djueq12  9909  dfac5lem3  10128  dfac5lem4  10129  hsmexlem8  10426  axdc4uz  14048  hashxp  14499  mamufval  22614  txuni2  23791  txbas  23793  txopn  23828  txrest  23857  txdis  23858  txdis1cn  23861  txtube  23866  txcmplem2  23868  tx1stc  23876  qustgplem  24347  tsmsxplem1  24379  isgrpo  30978  vciOLD  31042  isvclem  31058  issh  31689  hhssablo  31744  hhssnvt  31746  hhsssh  31750  2ndimaxp  33119  txomap  34344  tpr2rico  34422  elsx  34705  mbfmcst  34770  br2base  34780  dya2iocnrect  34792  sxbrsigalem5  34799  0rrv  34962  elima4  36355  finxpeq1  38140  isbnd3  38534  hdmap1fval  42669  csbresgVD  45717  mofeu  49776  functermc  50434