Theorem xpeq1 5157

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

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1523   ∈ wcel 2030  {copab 4745   × cxp 5141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-opab 4746  df-xp 5149

This theorem is referenced by:  xpeq12  5168  xpeq1i  5169  xpeq1d  5172  opthprc  5201  dmxpid  5377  reseq2  5423  xpnz  5588  xpdisj1  5590  xpcan2  5606  xpima  5611  unixp  5706  unixpid  5708  pmvalg  7910  xpsneng  8086  xpcomeng  8093  xpdom2g  8097  fodomr  8152  unxpdom  8208  xpfi  8272  marypha1lem  8380  cdaval  9030  iundom2g  9400  hashxplem  13258  dmtrclfv  13803  ramcl  15780  efgval  18176  frgpval  18217  frlmval  20140  txuni2  21416  txbas  21418  txopn  21453  txrest  21482  txdis  21483  txdis1cn  21486  tx1stc  21501  tmdgsum  21946  qustgplem  21971  incistruhgr  26019  isgrpo  27479  hhssablo  28248  hhssnvt  28250  hhsssh  28254  txomap  30029  tpr2rico  30086  elsx  30385  br2base  30459  dya2iocnrect  30471  sxbrsigalem5  30478  sibf0  30524  cvmlift2lem13  31423