Theorem opeq12 4590

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

Syntax hints:   → wi 4   ∧ wa 384   = wceq 1637  ⟨cop 4370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-rab 3101  df-v 3389  df-dif 3766  df-un 3768  df-in 3770  df-ss 3777  df-nul 4111  df-if 4274  df-sn 4365  df-pr 4367  df-op 4371

This theorem is referenced by:  opeq12i  4593  opeq12d  4596  cbvopab  4908  opth  5128  copsex2t  5140  copsex2g  5141  relop  5468  funopg  6129  fvn0ssdmfun  6566  fsn  6619  fnressn  6643  fmptsng  6653  fmptsnd  6654  tpres  6685  cbvoprab12  6953  eqopi  7428  f1o2ndf1  7513  tposoprab  7617  omeu  7896  brecop  8069  ecovcom  8083  ecovass  8084  ecovdi  8085  xpf1o  8355  addsrmo  10173  mulsrmo  10174  addsrpr  10175  mulsrpr  10176  addcnsr  10235  axcnre  10264  seqeq1  13021  opfi1uzind  13494  fsumcnv  14721  fprodcnv  14928  eucalgval2  15507  xpstopnlem1  21820  qustgplem  22131  finsumvtxdg2size  26668  brabgaf  29739  qqhval2  30345  brsegle  32530  finxpreclem3  33540  cnfinltrel  33551  eqrelf  34332  dvnprodlem1  40635  funop1  41867  uspgrsprf1  42317