Theorem opeq12 3767

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 3765	. 2 ⊢ (𝐴 = 𝐶 → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐵⟩)
2		opeq2 3766	. 2 ⊢ (𝐵 = 𝐷 → ⟨𝐶, 𝐵⟩ = ⟨𝐶, 𝐷⟩)
3	1, 2	sylan9eq 2223	1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩)

Syntax hints:   → wi 4   ∧ wa 103   = wceq 1348  ⟨cop 3586

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-un 3125  df-sn 3589  df-pr 3590  df-op 3592

This theorem is referenced by:  opeq12i  3770  opeq12d  3773  cbvopab  4060  opth  4222  copsex2t  4230  copsex2g  4231  relop  4761  funopg  5232  fsn  5668  fnressn  5682  cbvoprab12  5927  eqopi  6151  f1o2ndf1  6207  tposoprab  6259  brecop  6603  th3q  6618  ecovcom  6620  ecovicom  6621  ecovass  6622  ecoviass  6623  ecovdi  6624  ecovidi  6625  xpf1o  6822  1qec  7350  enq0sym  7394  addnq0mo  7409  mulnq0mo  7410  addnnnq0  7411  mulnnnq0  7412  distrnq0  7421  mulcomnq0  7422  addassnq0  7424  addsrmo  7705  mulsrmo  7706  addsrpr  7707  mulsrpr  7708  axcnre  7843  fsumcnv  11400  fprodcnv  11588  eucalgval2  12007