Theorem xpeq2 5652

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 2825	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵))
2	1	anbi2d 631	. . 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  xpeq2i  5658  xpeq2d  5661  xpnz  6123  xpdisj2  6126  dmxpss  6135  rnxpid  6137  xpcan  6140  unixp  6246  dfpo2  6260  fconst5  7161  naddcllem  8612  pmvalg  8784  xpcomeng  9007  unxpdom  9169  marypha1  9347  djueq12  9828  dfac5lem3  10047  dfac5lem4  10048  dfac5lem4OLD  10050  hsmexlem8  10346  axdc4uz  13946  hashxp  14396  mamufval  22357  txuni2  23530  txbas  23532  txopn  23567  txrest  23596  txdis  23597  txdis1cn  23600  txtube  23605  txcmplem2  23607  tx1stc  23615  qustgplem  24086  tsmsxplem1  24118  isgrpo  30568  vciOLD  30632  isvclem  30648  issh  31279  hhssablo  31334  hhssnvt  31336  hhsssh  31340  2ndimaxp  32719  txomap  33978  tpr2rico  34056  elsx  34338  mbfmcst  34403  br2base  34413  dya2iocnrect  34425  sxbrsigalem5  34432  0rrv  34595  elima4  35958  finxpeq1  37702  isbnd3  38105  hdmap1fval  42242  csbresgVD  45321  mofeu  49323  functermc  49983