Theorem opeq12 3864

Description: Equality theorem for ordered pairs. (Contributed by NM, 28-May-1995.)

Assertion

Ref	Expression
opeq12	⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩)

Proof of Theorem opeq12

Step	Hyp	Ref	Expression
1		opeq1 3862	. 2 ⊢ (𝐴 = 𝐶 → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐵⟩)
2		opeq2 3863	. 2 ⊢ (𝐵 = 𝐷 → ⟨𝐶, 𝐵⟩ = ⟨𝐶, 𝐷⟩)
3	1, 2	sylan9eq 2284	1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩)

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1397  ⟨cop 3672

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678

This theorem is referenced by:  opeq12i  3867  opeq12d  3870  cbvopab  4160  opth  4329  copsex2t  4337  copsex2g  4338  relop  4880  funopg  5360  fsn  5819  fnressn  5839  cbvoprab12  6094  eqopi  6334  f1o2ndf1  6392  tposoprab  6445  brecop  6793  th3q  6808  ecovcom  6810  ecovicom  6811  ecovass  6812  ecoviass  6813  ecovdi  6814  ecovidi  6815  xpf1o  7029  1qec  7607  enq0sym  7651  addnq0mo  7666  mulnq0mo  7667  addnnnq0  7668  mulnnnq0  7669  distrnq0  7678  mulcomnq0  7679  addassnq0  7681  addsrmo  7962  mulsrmo  7963  addsrpr  7964  mulsrpr  7965  axcnre  8100  fsumcnv  11997  fprodcnv  12185  eucalgval2  12624