Theorem xpeq1 5691

Description: Equality theorem for Cartesian product. (Contributed by NM, 4-Jul-1994.)

Assertion

Ref	Expression
xpeq1	⊢ (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶))

Proof of Theorem xpeq1

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq2 2823	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	anbi1d 631	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))
3	2	opabbidv 5215	. 2 ⊢ (𝐴 = 𝐵 → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)})
4		df-xp 5683	. 2 ⊢ (𝐴 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)}
5		df-xp 5683	. 2 ⊢ (𝐵 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)}
6	3, 4, 5	3eqtr4g 2798	1 ⊢ (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶))

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107  {copab 5211   × cxp 5675

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-opab 5212  df-xp 5683

This theorem is referenced by:  xpeq12  5702  xpeq1i  5703  xpeq1d  5706  opthprc  5741  dmxpid  5930  reseq2  5977  xpnz  6159  xpdisj1  6161  xpcan2  6177  xpima  6182  unixp  6282  unixpid  6284  naddcllem  8675  pmvalg  8831  xpsneng  9056  xpcomeng  9064  xpdom2g  9068  fodomr  9128  unxpdom  9253  xpfiOLD  9318  marypha1lem  9428  iundom2g  10535  hashxplem  14393  dmtrclfv  14965  ramcl  16962  efgval  19585  frgpval  19626  frlmval  21303  txuni2  23069  txbas  23071  txopn  23106  txrest  23135  txdis  23136  txdis1cn  23139  tx1stc  23154  tmdgsum  23599  qustgplem  23625  incistruhgr  28339  isgrpo  29750  hhssablo  30516  hhssnvt  30518  hhsssh  30522  gsumpart  32207  txomap  32814  tpr2rico  32892  elsx  33192  br2base  33268  dya2iocnrect  33280  sxbrsigalem5  33287  sibf0  33333  cvmlift2lem13  34306