Theorem opeq12 3780

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1353  ⟨cop 3595

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-un 3133  df-sn 3598  df-pr 3599  df-op 3601

This theorem is referenced by:  opeq12i  3783  opeq12d  3786  cbvopab  4074  opth  4237  copsex2t  4245  copsex2g  4246  relop  4777  funopg  5250  fsn  5688  fnressn  5702  cbvoprab12  5948  eqopi  6172  f1o2ndf1  6228  tposoprab  6280  brecop  6624  th3q  6639  ecovcom  6641  ecovicom  6642  ecovass  6643  ecoviass  6644  ecovdi  6645  ecovidi  6646  xpf1o  6843  1qec  7386  enq0sym  7430  addnq0mo  7445  mulnq0mo  7446  addnnnq0  7447  mulnnnq0  7448  distrnq0  7457  mulcomnq0  7458  addassnq0  7460  addsrmo  7741  mulsrmo  7742  addsrpr  7743  mulsrpr  7744  axcnre  7879  fsumcnv  11444  fprodcnv  11632  eucalgval2  12052