<filename>_data/proposition/P_op2ndb.json
{
  "citations" : [ {
    "textCitation" : "[See op2ndb on Metamath](http://us.metamath.org/mpegif/op2ndb.html)"
  } ],
  "names" : [ "op2ndb" ],
  "language" : "METAMATH_SET_MM",
  "lookupTerms" : [ "#T_cA", "#T_wcel", "#T_cvv", "#T_cB", "#T_wcel", "#T_cvv", "#T_cint", "#T_cint", "#T_cint", "#T_ccnv", "#T_csn--1", "#T_cop--1", "#T_cA", "#T_cop--2", "#T_cB", "#T_cop--3", "#T_csn--2", "#T_wceq", "#T_cB" ],
  "metaLanguage" : "METAMATH",
  "remarks" : " Extract the second member of an ordered pair.  Theorem 5.12(ii) of [Monk1] p. 52.  (See ~ op1stb to extract the first member, ~ op2nda for an alternate version, and ~ op2nd for the preferred version.) (Contributed by NM, 25-Nov-2003.) \n\n---\n\n Extract the second member of an ordered pair.  Theorem 5.12(ii) of [Monk1] p. 52.  (See ~ op1stb to extract the first member and ~ op2nda for an alternate version.)  (Contributed by NM, 25-Nov-2003.) ",
  "statement" : "cnvsn.1 $e |- A e. _V $.\ncnvsn.2 $e |- B e. _V $.\nop2ndb $p |- |^| |^| |^| `' { <. A , B >. } = B $."
}