Theorem xpeq1 5564

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1533   ∈ wcel 2110  {copab 5121   × cxp 5548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-12 2172  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-opab 5122  df-xp 5556

This theorem is referenced by:  xpeq12  5575  xpeq1i  5576  xpeq1d  5579  opthprc  5611  dmxpid  5795  reseq2  5843  xpnz  6011  xpdisj1  6013  xpcan2  6029  xpima  6034  unixp  6128  unixpid  6130  pmvalg  8411  xpsneng  8596  xpcomeng  8603  xpdom2g  8607  fodomr  8662  unxpdom  8719  xpfi  8783  marypha1lem  8891  iundom2g  9956  hashxplem  13788  dmtrclfv  14372  ramcl  16359  efgval  18837  frgpval  18878  frlmval  20886  txuni2  22167  txbas  22169  txopn  22204  txrest  22233  txdis  22234  txdis1cn  22237  tx1stc  22252  tmdgsum  22697  qustgplem  22723  incistruhgr  26858  isgrpo  28268  hhssablo  29034  hhssnvt  29036  hhsssh  29040  txomap  31093  tpr2rico  31150  elsx  31448  br2base  31522  dya2iocnrect  31534  sxbrsigalem5  31541  sibf0  31587  cvmlift2lem13  32557