Theorem xpeq1 5652

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {copab 5169   × cxp 5636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-opab 5170  df-xp 5644

This theorem is referenced by:  xpeq12  5663  xpeq1i  5664  xpeq1d  5667  opthprc  5702  dmxpid  5894  reseq2  5945  xpnz  6132  xpdisj1  6134  xpcan2  6150  xpima  6155  unixp  6255  unixpid  6257  naddcllem  8640  pmvalg  8810  xpsneng  9026  xpcomeng  9033  xpdom2g  9037  fodomr  9092  unxpdom  9200  xpfiOLD  9270  fodomfir  9279  marypha1lem  9384  iundom2g  10493  hashxplem  14398  dmtrclfv  14984  ramcl  17000  efgval  19647  frgpval  19688  frlmval  21657  txuni2  23452  txbas  23454  txopn  23489  txrest  23518  txdis  23519  txdis1cn  23522  tx1stc  23537  tmdgsum  23982  qustgplem  24008  incistruhgr  29006  isgrpo  30426  hhssablo  31192  hhssnvt  31194  hhsssh  31198  gsumpart  32997  txomap  33824  tpr2rico  33902  elsx  34184  br2base  34260  dya2iocnrect  34272  sxbrsigalem5  34279  sibf0  34325  cvmlift2lem13  35302