Theorem xpeq1 5664

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144  {copab 5166   × cxp 5648

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-opab 5167  df-xp 5656

This theorem is used by:  xpeq12  5675  xpeq1i  5676  xpeq1d  5679  opthprc  5714  dmxpid  5912  reseq2  5965  xpnz  6151  xpdisj1  6153  xpcan2  6170  xpima  6175  unixp  6287  unixpid  6289  naddcllem  8690  pmvalg  8862  xpsneng  9086  xpcomeng  9093  xpdom2g  9097  fodomr  9152  unxpdom  9255  fodomfir  9324  marypha1lem  9430  iundom2g  10629  hashxplem  14583  dmtrclfv  15178  ramcl  17214  efgval  19938  frgpval  19979  frlmval  22061  txuni2  23891  txbas  23893  txopn  23928  txrest  23957  txdis  23958  txdis1cn  23961  tx1stc  23976  tmdgsum  24421  qustgplem  24447  incistruhgr  29664  isgrpo  31106  hhssablo  31872  hhssnvt  31874  hhsssh  31878  gsumpart  33672  txomap  34514  tpr2rico  34592  elsx  34875  br2base  34949  dya2iocnrect  34961  sxbrsigalem5  34968  sibf0  35014  cvmlift2lem13  36168