Theorem xpeq1 5699

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-opab 5206  df-xp 5691

This theorem is referenced by:  xpeq12  5710  xpeq1i  5711  xpeq1d  5714  opthprc  5749  dmxpid  5941  reseq2  5992  xpnz  6179  xpdisj1  6181  xpcan2  6197  xpima  6202  unixp  6302  unixpid  6304  naddcllem  8714  pmvalg  8877  xpsneng  9096  xpcomeng  9104  xpdom2g  9108  fodomr  9168  unxpdom  9289  xpfiOLD  9359  fodomfir  9368  marypha1lem  9473  iundom2g  10580  hashxplem  14472  dmtrclfv  15057  ramcl  17067  efgval  19735  frgpval  19776  frlmval  21768  txuni2  23573  txbas  23575  txopn  23610  txrest  23639  txdis  23640  txdis1cn  23643  tx1stc  23658  tmdgsum  24103  qustgplem  24129  incistruhgr  29096  isgrpo  30516  hhssablo  31282  hhssnvt  31284  hhsssh  31288  gsumpart  33060  txomap  33833  tpr2rico  33911  elsx  34195  br2base  34271  dya2iocnrect  34283  sxbrsigalem5  34290  sibf0  34336  cvmlift2lem13  35320