Theorem xpeq2 5679

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147  {copab 5173   × cxp 5656

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-opab 5174  df-xp 5664

This theorem is used by:  xpeq12  5683  xpeq2i  5685  xpeq2d  5688  xpnz  6168  xpdisj2  6171  dmxpss  6181  rnxpid  6183  xpcan  6186  unixp  6309  dfpo2  6325  fconst5  7243  naddcllem  8723  pmvalg  8895  xpcomeng  9126  unxpdom  9288  marypha1  9463  djueq12  10022  dfac5lem3  10243  dfac5lem4  10244  hsmexlem8  10541  axdc4uz  14167  hashxp  14620  mamufval  22762  txuni2  23939  txbas  23941  txopn  23976  txrest  24005  txdis  24006  txdis1cn  24009  txtube  24014  txcmplem2  24016  tx1stc  24024  qustgplem  24495  tsmsxplem1  24527  isgrpo  31156  vciOLD  31220  isvclem  31236  issh  31867  hhssablo  31922  hhssnvt  31924  hhsssh  31928  2ndimaxp  33338  txomap  34577  tpr2rico  34655  elsx  34938  mbfmcst  35002  br2base  35012  dya2iocnrect  35024  sxbrsigalem5  35031  0rrv  35194  elima4  36755  finxpeq1  38577  isbnd3  38984  hdmap1fval  43119  csbresgVD  46137  mofeu  50290  functermc  50974