Theorem xpeq1 5673

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567   ∈ wcel 2149  {copab 5174   × cxp 5657

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-opab 5175  df-xp 5665

This theorem is referenced by:  xpeq12  5684  xpeq1i  5685  xpeq1d  5688  opthprc  5723  dmxpid  5918  reseq2  5971  xpnz  6154  xpdisj1  6156  xpcan2  6173  xpima  6178  unixp  6281  unixpid  6283  naddcllem  8658  pmvalg  8830  xpsneng  9046  xpcomeng  9053  xpdom2g  9057  fodomr  9112  unxpdom  9215  fodomfir  9283  marypha1lem  9389  iundom2g  10520  hashxplem  14466  dmtrclfv  15051  ramcl  17085  efgval  19783  frgpval  19824  frlmval  21863  txuni2  23687  txbas  23689  txopn  23724  txrest  23753  txdis  23754  txdis1cn  23757  tx1stc  23772  tmdgsum  24217  qustgplem  24243  incistruhgr  29366  isgrpo  30786  hhssablo  31552  hhssnvt  31554  hhsssh  31558  gsumpart  33320  txomap  34165  tpr2rico  34243  elsx  34525  br2base  34600  dya2iocnrect  34612  sxbrsigalem5  34619  sibf0  34665  cvmlift2lem13  35702