Theorem xpeq2 5376

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

Syntax hints:   → wi 4   ∧ wa 386   = wceq 1601   ∈ wcel 2107  {copab 4948   × cxp 5353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-opab 4949  df-xp 5361

This theorem is referenced by:  xpeq12  5380  xpeq2i  5382  xpeq2d  5385  xpnz  5807  xpdisj2  5810  dmxpss  5819  rnxpid  5821  xpcan  5824  unixp  5922  fconst5  6743  pmvalg  8151  xpcomeng  8340  unxpdom  8455  marypha1  8628  djueq12  9064  dfac5lem3  9281  dfac5lem4  9282  hsmexlem8  9581  axdc4uz  13102  hashxp  13535  mamufval  20595  txuni2  21777  txbas  21779  txopn  21814  txrest  21843  txdis  21844  txdis1cn  21847  txtube  21852  txcmplem2  21854  tx1stc  21862  qustgplem  22332  tsmsxplem1  22364  isgrpo  27924  vciOLD  27988  isvclem  28004  issh  28637  hhssablo  28692  hhssnvt  28694  hhsssh  28698  txomap  30499  tpr2rico  30556  elsx  30855  mbfmcst  30919  br2base  30929  dya2iocnrect  30941  sxbrsigalem5  30948  0rrv  31112  dfpo2  32239  elima4  32267  finxpeq1  33818  isbnd3  34207  hdmap1fval  37950  csbresgVD  40064