Theorem xpeq1 5655

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-opab 5173  df-xp 5647

This theorem is referenced by:  xpeq12  5666  xpeq1i  5667  xpeq1d  5670  opthprc  5705  dmxpid  5897  reseq2  5948  xpnz  6135  xpdisj1  6137  xpcan2  6153  xpima  6158  unixp  6258  unixpid  6260  naddcllem  8643  pmvalg  8813  xpsneng  9030  xpcomeng  9038  xpdom2g  9042  fodomr  9098  unxpdom  9207  xpfiOLD  9277  fodomfir  9286  marypha1lem  9391  iundom2g  10500  hashxplem  14405  dmtrclfv  14991  ramcl  17007  efgval  19654  frgpval  19695  frlmval  21664  txuni2  23459  txbas  23461  txopn  23496  txrest  23525  txdis  23526  txdis1cn  23529  tx1stc  23544  tmdgsum  23989  qustgplem  24015  incistruhgr  29013  isgrpo  30433  hhssablo  31199  hhssnvt  31201  hhsssh  31205  gsumpart  33004  txomap  33831  tpr2rico  33909  elsx  34191  br2base  34267  dya2iocnrect  34279  sxbrsigalem5  34286  sibf0  34332  cvmlift2lem13  35309