Theorem xpeq2 5053

Description: Equality theorem for Cartesian product. (Contributed by NM, 5-Jul-1994.)

Assertion

Ref	Expression
xpeq2	⊢ (𝐴 = 𝐵 → (𝐶 × 𝐴) = (𝐶 × 𝐵))

Proof of Theorem xpeq2

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq2 2677	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵))
2	1	anbi2d 736	. . 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  xpeq2i  5060  xpeq2d  5063  xpnz  5472  xpdisj2  5475  dmxpss  5484  rnxpid  5486  xpcan  5489  unixp  5585  fconst5  6376  pmvalg  7755  xpcomeng  7937  unxpdom  8052  marypha1  8223  dfac5lem3  8831  dfac5lem4  8832  hsmexlem8  9129  axdc4uz  12645  hashxp  13081  mamufval  20010  txuni2  21178  txbas  21180  txopn  21215  txrest  21244  txdis  21245  txdis1cn  21248  txtube  21253  txcmplem2  21255  tx1stc  21263  qustgplem  21734  tsmsxplem1  21766  isgrpo  26735  vciOLD  26800  isvclem  26816  issh  27449  hhssablo  27504  hhssnvt  27506  hhsssh  27510  txomap  29229  tpr2rico  29286  elsx  29584  mbfmcst  29648  br2base  29658  dya2iocnrect  29670  sxbrsigalem5  29677  0rrv  29840  dfpo2  30898  elima4  30924  finxpeq1  32399  isbnd3  32753  hdmap1fval  36104  csbresgVD  38153