Theorem xpeq1 5714

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2108  {copab 5228   × cxp 5698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-opab 5229  df-xp 5706

This theorem is referenced by:  xpeq12  5725  xpeq1i  5726  xpeq1d  5729  opthprc  5764  dmxpid  5955  reseq2  6004  xpnz  6190  xpdisj1  6192  xpcan2  6208  xpima  6213  unixp  6313  unixpid  6315  naddcllem  8732  pmvalg  8895  xpsneng  9122  xpcomeng  9130  xpdom2g  9134  fodomr  9194  unxpdom  9316  xpfiOLD  9387  fodomfir  9396  marypha1lem  9502  iundom2g  10609  hashxplem  14482  dmtrclfv  15067  ramcl  17076  efgval  19759  frgpval  19800  frlmval  21791  txuni2  23594  txbas  23596  txopn  23631  txrest  23660  txdis  23661  txdis1cn  23664  tx1stc  23679  tmdgsum  24124  qustgplem  24150  incistruhgr  29114  isgrpo  30529  hhssablo  31295  hhssnvt  31297  hhsssh  31301  gsumpart  33038  txomap  33780  tpr2rico  33858  elsx  34158  br2base  34234  dya2iocnrect  34246  sxbrsigalem5  34253  sibf0  34299  cvmlift2lem13  35283