Theorem xpeq1 5669

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  {copab 5167   × cxp 5653

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-opab 5168  df-xp 5661

This theorem is used by:  xpeq12  5680  xpeq1i  5681  xpeq1d  5684  opthprc  5719  dmxpid  5914  reseq2  5967  xpnz  6151  xpdisj1  6153  xpcan2  6170  xpima  6175  unixp  6280  unixpid  6282  naddcllem  8664  pmvalg  8836  xpsneng  9060  xpcomeng  9067  xpdom2g  9071  fodomr  9126  unxpdom  9229  fodomfir  9297  marypha1lem  9403  iundom2g  10548  hashxplem  14498  dmtrclfv  15091  ramcl  17121  efgval  19844  frgpval  19885  frlmval  21961  txuni2  23791  txbas  23793  txopn  23828  txrest  23857  txdis  23858  txdis1cn  23861  tx1stc  23876  tmdgsum  24321  qustgplem  24347  incistruhgr  29536  isgrpo  30978  hhssablo  31744  hhssnvt  31746  hhsssh  31750  gsumpart  33503  txomap  34344  tpr2rico  34422  elsx  34705  br2base  34780  dya2iocnrect  34792  sxbrsigalem5  34799  sibf0  34845  cvmlift2lem13  35894