Theorem xpeq2 5571

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1533   ∈ wcel 2110  {copab 5121   × cxp 5548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-12 2172  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-opab 5122  df-xp 5556

This theorem is referenced by:  xpeq12  5575  xpeq2i  5577  xpeq2d  5580  xpnz  6011  xpdisj2  6014  dmxpss  6023  rnxpid  6025  xpcan  6028  unixp  6128  fconst5  6963  pmvalg  8411  xpcomeng  8603  unxpdom  8719  marypha1  8892  djueq12  9327  dfac5lem3  9545  dfac5lem4  9546  hsmexlem8  9840  axdc4uz  13346  hashxp  13789  mamufval  20990  txuni2  22167  txbas  22169  txopn  22204  txrest  22233  txdis  22234  txdis1cn  22237  txtube  22242  txcmplem2  22244  tx1stc  22252  qustgplem  22723  tsmsxplem1  22755  isgrpo  28268  vciOLD  28332  isvclem  28348  issh  28979  hhssablo  29034  hhssnvt  29036  hhsssh  29040  txomap  31093  tpr2rico  31150  elsx  31448  mbfmcst  31512  br2base  31522  dya2iocnrect  31534  sxbrsigalem5  31541  0rrv  31704  dfpo2  32986  elima4  33014  finxpeq1  34661  isbnd3  35056  hdmap1fval  38926  csbresgVD  41222