Theorem xpeq1 5371

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

Syntax hints:   → wi 4   ∧ wa 386   = wceq 1601   ∈ wcel 2107  {copab 4950   × cxp 5355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-opab 4951  df-xp 5363

This theorem is referenced by:  xpeq12  5382  xpeq1i  5383  xpeq1d  5386  opthprc  5415  dmxpid  5592  reseq2  5639  xpnz  5809  xpdisj1  5811  xpcan2  5827  xpima  5832  unixp  5924  unixpid  5926  pmvalg  8153  xpsneng  8335  xpcomeng  8342  xpdom2g  8346  fodomr  8401  unxpdom  8457  xpfi  8521  marypha1lem  8629  cdaval  9329  iundom2g  9699  hashxplem  13538  dmtrclfv  14170  ramcl  16141  efgval  18518  frgpval  18561  frlmval  20495  txuni2  21781  txbas  21783  txopn  21818  txrest  21847  txdis  21848  txdis1cn  21851  tx1stc  21866  tmdgsum  22311  qustgplem  22336  incistruhgr  26431  isgrpo  27928  hhssablo  28696  hhssnvt  28698  hhsssh  28702  txomap  30503  tpr2rico  30560  elsx  30859  br2base  30933  dya2iocnrect  30945  sxbrsigalem5  30952  sibf0  30998  cvmlift2lem13  31900