FOM: Alternatives to ZFC in actual use

[Kanovei]

Is there any known statement A such that 

1) A is a meaningful mathematical statement 
   (e.g., NOT of the form Con ZFC)
2) A is formalizable in set theoretic language 
   (e.g. NOT on existence of some "universe")
3) A is NOT provable in ZFC 
4) A is provable in ZFC + "universes" or "topoi" or the like. 

?

V.Kanovei