Theorem opeq12 3807

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1364  ⟨cop 3622

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3158  df-sn 3625  df-pr 3626  df-op 3628

This theorem is referenced by:  opeq12i  3810  opeq12d  3813  cbvopab  4101  opth  4267  copsex2t  4275  copsex2g  4276  relop  4813  funopg  5289  fsn  5731  fnressn  5745  cbvoprab12  5993  eqopi  6227  f1o2ndf1  6283  tposoprab  6335  brecop  6681  th3q  6696  ecovcom  6698  ecovicom  6699  ecovass  6700  ecoviass  6701  ecovdi  6702  ecovidi  6703  xpf1o  6902  1qec  7450  enq0sym  7494  addnq0mo  7509  mulnq0mo  7510  addnnnq0  7511  mulnnnq0  7512  distrnq0  7521  mulcomnq0  7522  addassnq0  7524  addsrmo  7805  mulsrmo  7806  addsrpr  7807  mulsrpr  7808  axcnre  7943  fsumcnv  11583  fprodcnv  11771  eucalgval2  12194