Theorem xpeq1 5052

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

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475   ∈ wcel 1977  {copab 4642   × cxp 5036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-opab 4644  df-xp 5044

This theorem is referenced by:  xpeq12  5058  xpeq1i  5059  xpeq1d  5062  opthprc  5089  dmxpid  5266  reseq2  5312  xpnz  5472  xpdisj1  5474  xpcan2  5490  xpima  5495  unixp  5585  unixpid  5587  pmvalg  7755  xpsneng  7930  xpcomeng  7937  xpdom2g  7941  fodomr  7996  unxpdom  8052  xpfi  8116  marypha1lem  8222  cdaval  8875  iundom2g  9241  hashxplem  13080  dmtrclfv  13607  ramcl  15571  efgval  17953  frgpval  17994  frlmval  19911  txuni2  21178  txbas  21180  txopn  21215  txrest  21244  txdis  21245  txdis1cn  21248  tx1stc  21263  tmdgsum  21709  qustgplem  21734  incistruhgr  25746  isgrpo  26735  hhssablo  27504  hhssnvt  27506  hhsssh  27510  txomap  29229  tpr2rico  29286  elsx  29584  br2base  29658  dya2iocnrect  29670  sxbrsigalem5  29677  sibf0  29723  cvmlift2lem13  30551