Theorem opeq12 3858

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1395  ⟨cop 3669

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675

This theorem is referenced by:  opeq12i  3861  opeq12d  3864  cbvopab  4154  opth  4322  copsex2t  4330  copsex2g  4331  relop  4871  funopg  5351  fsn  5806  fnressn  5824  cbvoprab12  6077  eqopi  6316  f1o2ndf1  6372  tposoprab  6424  brecop  6770  th3q  6785  ecovcom  6787  ecovicom  6788  ecovass  6789  ecoviass  6790  ecovdi  6791  ecovidi  6792  xpf1o  7001  1qec  7571  enq0sym  7615  addnq0mo  7630  mulnq0mo  7631  addnnnq0  7632  mulnnnq0  7633  distrnq0  7642  mulcomnq0  7643  addassnq0  7645  addsrmo  7926  mulsrmo  7927  addsrpr  7928  mulsrpr  7929  axcnre  8064  fsumcnv  11943  fprodcnv  12131  eucalgval2  12570