Theorem xpeq1 5645

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {copab 5164   × cxp 5629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-opab 5165  df-xp 5637

This theorem is referenced by:  xpeq12  5656  xpeq1i  5657  xpeq1d  5660  opthprc  5695  dmxpid  5883  reseq2  5934  xpnz  6120  xpdisj1  6122  xpcan2  6138  xpima  6143  unixp  6243  unixpid  6245  naddcllem  8617  pmvalg  8787  xpsneng  9003  xpcomeng  9010  xpdom2g  9014  fodomr  9069  unxpdom  9176  xpfiOLD  9246  fodomfir  9255  marypha1lem  9360  iundom2g  10469  hashxplem  14374  dmtrclfv  14960  ramcl  16976  efgval  19623  frgpval  19664  frlmval  21633  txuni2  23428  txbas  23430  txopn  23465  txrest  23494  txdis  23495  txdis1cn  23498  tx1stc  23513  tmdgsum  23958  qustgplem  23984  incistruhgr  28982  isgrpo  30399  hhssablo  31165  hhssnvt  31167  hhsssh  31171  gsumpart  32970  txomap  33797  tpr2rico  33875  elsx  34157  br2base  34233  dya2iocnrect  34245  sxbrsigalem5  34252  sibf0  34298  cvmlift2lem13  35275