Theorem xpeq1 5645

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {copab 5147   × cxp 5629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-opab 5148  df-xp 5637

This theorem is referenced by:  xpeq12  5656  xpeq1i  5657  xpeq1d  5660  opthprc  5695  dmxpid  5885  reseq2  5939  xpnz  6123  xpdisj1  6125  xpcan2  6141  xpima  6146  unixp  6246  unixpid  6248  naddcllem  8612  pmvalg  8784  xpsneng  9000  xpcomeng  9007  xpdom2g  9011  fodomr  9066  unxpdom  9169  fodomfir  9238  marypha1lem  9346  iundom2g  10462  hashxplem  14395  dmtrclfv  14980  ramcl  17000  efgval  19692  frgpval  19733  frlmval  21728  txuni2  23530  txbas  23532  txopn  23567  txrest  23596  txdis  23597  txdis1cn  23600  tx1stc  23615  tmdgsum  24060  qustgplem  24086  incistruhgr  29148  isgrpo  30568  hhssablo  31334  hhssnvt  31336  hhsssh  31340  gsumpart  33124  txomap  33978  tpr2rico  34056  elsx  34338  br2base  34413  dya2iocnrect  34425  sxbrsigalem5  34432  sibf0  34478  cvmlift2lem13  35497