Theorem opeq12 3795

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

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

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 2171

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-v 2754  df-un 3148  df-sn 3613  df-pr 3614  df-op 3616

This theorem is referenced by:  opeq12i  3798  opeq12d  3801  cbvopab  4089  opth  4255  copsex2t  4263  copsex2g  4264  relop  4795  funopg  5269  fsn  5708  fnressn  5722  cbvoprab12  5969  eqopi  6196  f1o2ndf1  6252  tposoprab  6304  brecop  6650  th3q  6665  ecovcom  6667  ecovicom  6668  ecovass  6669  ecoviass  6670  ecovdi  6671  ecovidi  6672  xpf1o  6871  1qec  7416  enq0sym  7460  addnq0mo  7475  mulnq0mo  7476  addnnnq0  7477  mulnnnq0  7478  distrnq0  7487  mulcomnq0  7488  addassnq0  7490  addsrmo  7771  mulsrmo  7772  addsrpr  7773  mulsrpr  7774  axcnre  7909  fsumcnv  11476  fprodcnv  11664  eucalgval2  12084