Theorem opeq12 3702

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

Syntax hints:   → wi 4   ∧ wa 103   = wceq 1331  ⟨cop 3525

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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-v 2683  df-un 3070  df-sn 3528  df-pr 3529  df-op 3531

This theorem is referenced by:  opeq12i  3705  opeq12d  3708  cbvopab  3994  opth  4154  copsex2t  4162  copsex2g  4163  relop  4684  funopg  5152  fsn  5585  fnressn  5599  cbvoprab12  5838  eqopi  6063  f1o2ndf1  6118  tposoprab  6170  brecop  6512  th3q  6527  ecovcom  6529  ecovicom  6530  ecovass  6531  ecoviass  6532  ecovdi  6533  ecovidi  6534  xpf1o  6731  1qec  7189  enq0sym  7233  addnq0mo  7248  mulnq0mo  7249  addnnnq0  7250  mulnnnq0  7251  distrnq0  7260  mulcomnq0  7261  addassnq0  7263  addsrmo  7544  mulsrmo  7545  addsrpr  7546  mulsrpr  7547  axcnre  7682  fsumcnv  11199  eucalgval2  11723