{
  "citations" : [ {
    "textCitation" : "[See xpfi on Metamath](http://us.metamath.org/mpegif/xpfi.html)"
  } ],
  "names" : [ "xpfi" ],
  "language" : "METAMATH_SET_MM",
  "lookupTerms" : [ "#T_cA", "#T_wcel", "#T_cfn", "#T_wa", "#T_cB", "#T_wcel", "#T_cfn", "#T_wi", "#T_cA", "#T_cxp", "#T_cB", "#T_wcel", "#T_cfn" ],
  "metaLanguage" : "METAMATH",
  "remarks" : " The Cartesian product of two finite sets is finite.  (Contributed by <NAME>, 2-Sep-2009.)  (Revised by <NAME>, 12-Mar-2015.) ",
  "statement" : "xpfi $p |- ( ( A e. Fin /\\ B e. Fin ) -> ( A X. B ) e. Fin ) $."
}