Theorem xpeq1 5594

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2108  {copab 5132   × cxp 5578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-opab 5133  df-xp 5586

This theorem is referenced by:  xpeq12  5605  xpeq1i  5606  xpeq1d  5609  opthprc  5642  dmxpid  5828  reseq2  5875  xpnz  6051  xpdisj1  6053  xpcan2  6069  xpima  6074  unixp  6174  unixpid  6176  pmvalg  8584  xpsneng  8797  xpcomeng  8804  xpdom2g  8808  fodomr  8864  unxpdom  8959  xpfi  9015  marypha1lem  9122  iundom2g  10227  hashxplem  14076  dmtrclfv  14657  ramcl  16658  efgval  19238  frgpval  19279  frlmval  20865  txuni2  22624  txbas  22626  txopn  22661  txrest  22690  txdis  22691  txdis1cn  22694  tx1stc  22709  tmdgsum  23154  qustgplem  23180  incistruhgr  27352  isgrpo  28760  hhssablo  29526  hhssnvt  29528  hhsssh  29532  gsumpart  31217  txomap  31686  tpr2rico  31764  elsx  32062  br2base  32136  dya2iocnrect  32148  sxbrsigalem5  32155  sibf0  32201  cvmlift2lem13  33177  naddcllem  33758