Theorem xpeq1 5672

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147  {copab 5173   × cxp 5656

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-opab 5174  df-xp 5664

This theorem is used by:  xpeq12  5683  xpeq1i  5684  xpeq1d  5687  opthprc  5722  dmxpid  5924  reseq2  5981  xpnz  6168  xpdisj1  6170  xpcan2  6187  xpima  6192  unixp  6309  unixpid  6311  naddcllem  8723  pmvalg  8895  xpsneng  9119  xpcomeng  9126  xpdom2g  9130  fodomr  9185  unxpdom  9288  fodomfir  9357  marypha1lem  9462  iundom2g  10663  hashxplem  14619  dmtrclfv  15214  ramcl  17251  efgval  19982  frgpval  20023  frlmval  22109  txuni2  23939  txbas  23941  txopn  23976  txrest  24005  txdis  24006  txdis1cn  24009  tx1stc  24024  tmdgsum  24469  qustgplem  24495  incistruhgr  29714  isgrpo  31156  hhssablo  31922  hhssnvt  31924  hhsssh  31928  gsumpart  33723  txomap  34577  tpr2rico  34655  elsx  34938  br2base  35012  dya2iocnrect  35024  sxbrsigalem5  35031  sibf0  35077  cvmlift2lem13  36288