Theorem xpeq1 5646

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 2826	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	anbi1d 632	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))
3	2	opabbidv 5166	. 2 ⊢ (𝐴 = 𝐵 → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)})
4		df-xp 5638	. 2 ⊢ (𝐴 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)}
5		df-xp 5638	. 2 ⊢ (𝐵 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)}
6	3, 4, 5	3eqtr4g 2797	1 ⊢ (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {copab 5162   × cxp 5630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-opab 5163  df-xp 5638

This theorem is referenced by:  xpeq12  5657  xpeq1i  5658  xpeq1d  5661  opthprc  5696  dmxpid  5887  reseq2  5941  xpnz  6125  xpdisj1  6127  xpcan2  6143  xpima  6148  unixp  6248  unixpid  6250  naddcllem  8614  pmvalg  8786  xpsneng  9002  xpcomeng  9009  xpdom2g  9013  fodomr  9068  unxpdom  9171  fodomfir  9240  marypha1lem  9348  iundom2g  10462  hashxplem  14368  dmtrclfv  14953  ramcl  16969  efgval  19658  frgpval  19699  frlmval  21715  txuni2  23521  txbas  23523  txopn  23558  txrest  23587  txdis  23588  txdis1cn  23591  tx1stc  23606  tmdgsum  24051  qustgplem  24077  incistruhgr  29164  isgrpo  30585  hhssablo  31351  hhssnvt  31353  hhsssh  31357  gsumpart  33157  txomap  34012  tpr2rico  34090  elsx  34372  br2base  34447  dya2iocnrect  34459  sxbrsigalem5  34466  sibf0  34512  cvmlift2lem13  35531