Theorem xpeq1 5533

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111  {copab 5092   × cxp 5517

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-opab 5093  df-xp 5525

This theorem is referenced by:  xpeq12  5544  xpeq1i  5545  xpeq1d  5548  opthprc  5580  dmxpid  5764  reseq2  5813  xpnz  5983  xpdisj1  5985  xpcan2  6001  xpima  6006  unixp  6101  unixpid  6103  pmvalg  8400  xpsneng  8585  xpcomeng  8592  xpdom2g  8596  fodomr  8652  unxpdom  8709  xpfi  8773  marypha1lem  8881  iundom2g  9951  hashxplem  13790  dmtrclfv  14369  ramcl  16355  efgval  18835  frgpval  18876  frlmval  20437  txuni2  22170  txbas  22172  txopn  22207  txrest  22236  txdis  22237  txdis1cn  22240  tx1stc  22255  tmdgsum  22700  qustgplem  22726  incistruhgr  26872  isgrpo  28280  hhssablo  29046  hhssnvt  29048  hhsssh  29052  gsumpart  30740  txomap  31187  tpr2rico  31265  elsx  31563  br2base  31637  dya2iocnrect  31649  sxbrsigalem5  31656  sibf0  31702  cvmlift2lem13  32675