Theorem xpeq1 5638

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  {copab 5160   × cxp 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-opab 5161  df-xp 5630

This theorem is referenced by:  xpeq12  5649  xpeq1i  5650  xpeq1d  5653  opthprc  5688  dmxpid  5879  reseq2  5933  xpnz  6117  xpdisj1  6119  xpcan2  6135  xpima  6140  unixp  6240  unixpid  6242  naddcllem  8604  pmvalg  8774  xpsneng  8990  xpcomeng  8997  xpdom2g  9001  fodomr  9056  unxpdom  9159  fodomfir  9228  marypha1lem  9336  iundom2g  10450  hashxplem  14356  dmtrclfv  14941  ramcl  16957  efgval  19646  frgpval  19687  frlmval  21703  txuni2  23509  txbas  23511  txopn  23546  txrest  23575  txdis  23576  txdis1cn  23579  tx1stc  23594  tmdgsum  24039  qustgplem  24065  incistruhgr  29152  isgrpo  30572  hhssablo  31338  hhssnvt  31340  hhsssh  31344  gsumpart  33146  txomap  33991  tpr2rico  34069  elsx  34351  br2base  34426  dya2iocnrect  34438  sxbrsigalem5  34445  sibf0  34491  cvmlift2lem13  35509