Theorem xpeq1 5665

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1563   ∈ wcel 2145  {copab 5166   × cxp 5649

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-opab 5167  df-xp 5657

This theorem is referenced by:  xpeq12  5676  xpeq1i  5677  xpeq1d  5680  opthprc  5715  dmxpid  5910  reseq2  5963  xpnz  6147  xpdisj1  6149  xpcan2  6166  xpima  6171  unixp  6272  unixpid  6274  naddcllem  8650  pmvalg  8822  xpsneng  9038  xpcomeng  9045  xpdom2g  9049  fodomr  9104  unxpdom  9207  fodomfir  9275  marypha1lem  9381  iundom2g  10512  hashxplem  14458  dmtrclfv  15043  ramcl  17077  efgval  19775  frgpval  19816  frlmval  21855  txuni2  23679  txbas  23681  txopn  23716  txrest  23745  txdis  23746  txdis1cn  23749  tx1stc  23764  tmdgsum  24209  qustgplem  24235  incistruhgr  29334  isgrpo  30754  hhssablo  31520  hhssnvt  31522  hhsssh  31526  gsumpart  33291  txomap  34136  tpr2rico  34214  elsx  34496  br2base  34571  dya2iocnrect  34583  sxbrsigalem5  34590  sibf0  34636  cvmlift2lem13  35673