Theorem opeq12 3862

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

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

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 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676

This theorem is referenced by:  opeq12i  3865  opeq12d  3868  cbvopab  4158  opth  4327  copsex2t  4335  copsex2g  4336  relop  4878  funopg  5358  fsn  5815  fnressn  5835  cbvoprab12  6090  eqopi  6330  f1o2ndf1  6388  tposoprab  6441  brecop  6789  th3q  6804  ecovcom  6806  ecovicom  6807  ecovass  6808  ecoviass  6809  ecovdi  6810  ecovidi  6811  xpf1o  7025  1qec  7598  enq0sym  7642  addnq0mo  7657  mulnq0mo  7658  addnnnq0  7659  mulnnnq0  7660  distrnq0  7669  mulcomnq0  7670  addassnq0  7672  addsrmo  7953  mulsrmo  7954  addsrpr  7955  mulsrpr  7956  axcnre  8091  fsumcnv  11988  fprodcnv  12176  eucalgval2  12615