src/ZF/equalities.ML
changeset 839 1aa6b351ca34
parent 787 1affbb1c5f1f
child 1035 279a4fd3c5ce
equal deleted inserted replaced
838:120edb26ee93 839:1aa6b351ca34
   483 
   483 
   484 goal ZF.thy "!!x A. x:A ==> (INT x:A. Pow(B(x))) = Pow(INT x:A. B(x))";
   484 goal ZF.thy "!!x A. x:A ==> (INT x:A. Pow(B(x))) = Pow(INT x:A. B(x))";
   485 by (fast_tac eq_cs 1);
   485 by (fast_tac eq_cs 1);
   486 qed "INT_Pow_subset";
   486 qed "INT_Pow_subset";
   487 
   487 
       
   488 (** RepFun **)
       
   489 
       
   490 goal ZF.thy "{f(x).x:A}=0 <-> A=0";
       
   491 by (fast_tac (eq_cs addSEs [equalityE]) 1);
       
   492 qed "RepFun_eq_0_iff";
       
   493 
       
   494 goal ZF.thy "{f(x).x:0} = 0";
       
   495 by (fast_tac eq_cs 1);
       
   496 qed "RepFun_0";