Theorem opeq12 3646

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

Syntax hints:   → wi 4   ∧ wa 103   = wceq 1296  ⟨cop 3469

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-3an 929  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-v 2635  df-un 3017  df-sn 3472  df-pr 3473  df-op 3475

This theorem is referenced by:  opeq12i  3649  opeq12d  3652  cbvopab  3931  opth  4088  copsex2t  4096  copsex2g  4097  relop  4617  funopg  5082  fsn  5508  fnressn  5522  cbvoprab12  5760  eqopi  5980  f1o2ndf1  6031  tposoprab  6083  brecop  6422  th3q  6437  ecovcom  6439  ecovicom  6440  ecovass  6441  ecoviass  6442  ecovdi  6443  ecovidi  6444  xpf1o  6640  1qec  7044  enq0sym  7088  addnq0mo  7103  mulnq0mo  7104  addnnnq0  7105  mulnnnq0  7106  distrnq0  7115  mulcomnq0  7116  addassnq0  7118  addsrmo  7386  mulsrmo  7387  addsrpr  7388  mulsrpr  7389  axcnre  7513  fsumcnv  10995  eucalgval2  11477