Theorem xpeq1 5632

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119  {copab 5134   × cxp 5616

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-opab 5135  df-xp 5624

This theorem is referenced by:  xpeq12  5643  xpeq1i  5644  xpeq1d  5647  opthprc  5682  dmxpid  5872  reseq2  5926  xpnz  6110  xpdisj1  6112  xpcan2  6128  xpima  6133  unixp  6233  unixpid  6235  naddcllem  8602  pmvalg  8774  xpsneng  8990  xpcomeng  8997  xpdom2g  9001  fodomr  9056  unxpdom  9159  fodomfir  9228  marypha1lem  9336  iundom2g  10453  hashxplem  14386  dmtrclfv  14971  ramcl  16991  efgval  19683  frgpval  19724  frlmval  21723  txuni2  23548  txbas  23550  txopn  23585  txrest  23614  txdis  23615  txdis1cn  23618  tx1stc  23633  tmdgsum  24078  qustgplem  24104  incistruhgr  29166  isgrpo  30586  hhssablo  31352  hhssnvt  31354  hhsssh  31358  gsumpart  33144  txomap  34018  tpr2rico  34096  elsx  34378  br2base  34453  dya2iocnrect  34465  sxbrsigalem5  34472  sibf0  34518  cvmlift2lem13  35543