Theorem xpeq1 5668

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  {copab 5181   × cxp 5652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-opab 5182  df-xp 5660

This theorem is referenced by:  xpeq12  5679  xpeq1i  5680  xpeq1d  5683  opthprc  5718  dmxpid  5910  reseq2  5961  xpnz  6148  xpdisj1  6150  xpcan2  6166  xpima  6171  unixp  6271  unixpid  6273  naddcllem  8686  pmvalg  8849  xpsneng  9068  xpcomeng  9076  xpdom2g  9080  fodomr  9140  unxpdom  9259  xpfiOLD  9329  fodomfir  9338  marypha1lem  9443  iundom2g  10552  hashxplem  14449  dmtrclfv  15035  ramcl  17047  efgval  19696  frgpval  19737  frlmval  21706  txuni2  23501  txbas  23503  txopn  23538  txrest  23567  txdis  23568  txdis1cn  23571  tx1stc  23586  tmdgsum  24031  qustgplem  24057  incistruhgr  29004  isgrpo  30424  hhssablo  31190  hhssnvt  31192  hhsssh  31196  gsumpart  32997  txomap  33811  tpr2rico  33889  elsx  34171  br2base  34247  dya2iocnrect  34259  sxbrsigalem5  34266  sibf0  34312  cvmlift2lem13  35283