Theorem xpeq1 5665

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

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

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-opab 5168  df-xp 5657

This theorem is used by:  xpeq12  5676  xpeq1i  5677  xpeq1d  5680  opthprc  5715  dmxpid  5912  reseq2  5965  xpnz  6150  xpdisj1  6152  xpcan2  6169  xpima  6174  unixp  6284  unixpid  6286  naddcllem  8678  pmvalg  8850  xpsneng  9074  xpcomeng  9081  xpdom2g  9085  fodomr  9140  unxpdom  9243  fodomfir  9312  marypha1lem  9418  iundom2g  10617  hashxplem  14571  dmtrclfv  15164  ramcl  17200  efgval  19924  frgpval  19965  frlmval  22047  txuni2  23877  txbas  23879  txopn  23914  txrest  23943  txdis  23944  txdis1cn  23947  tx1stc  23962  tmdgsum  24407  qustgplem  24433  incistruhgr  29650  isgrpo  31092  hhssablo  31858  hhssnvt  31860  hhsssh  31864  gsumpart  33617  txomap  34459  tpr2rico  34537  elsx  34820  br2base  34894  dya2iocnrect  34906  sxbrsigalem5  34913  sibf0  34959  cvmlift2lem13  36059