ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  opeq12 GIF version

Theorem opeq12 3551
Description: Equality theorem for ordered pairs. (Contributed by NM, 28-May-1995.)
Assertion
Ref Expression
opeq12 ((𝐴 = 𝐶𝐵 = 𝐷) → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩)

Proof of Theorem opeq12
StepHypRef Expression
1 opeq1 3549 . 2 (𝐴 = 𝐶 → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐵⟩)
2 opeq2 3550 . 2 (𝐵 = 𝐷 → ⟨𝐶, 𝐵⟩ = ⟨𝐶, 𝐷⟩)
31, 2sylan9eq 2092 1 ((𝐴 = 𝐶𝐵 = 𝐷) → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97   = wceq 1243  cop 3378
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-v 2559  df-un 2922  df-sn 3381  df-pr 3382  df-op 3384
This theorem is referenced by:  opeq12i  3554  opeq12d  3557  cbvopab  3828  opth  3974  copsex2t  3982  copsex2g  3983  relop  4486  funopg  4934  fsn  5335  fnressn  5349  cbvoprab12  5578  eqopi  5798  f1o2ndf1  5849  tposoprab  5895  brecop  6196  th3q  6211  ecovcom  6213  ecovicom  6214  ecovass  6215  ecoviass  6216  ecovdi  6217  ecovidi  6218  1qec  6486  enq0sym  6530  addnq0mo  6545  mulnq0mo  6546  addnnnq0  6547  mulnnnq0  6548  distrnq0  6557  mulcomnq0  6558  addassnq0  6560  addsrmo  6828  mulsrmo  6829  addsrpr  6830  mulsrpr  6831  axcnre  6955
  Copyright terms: Public domain W3C validator