Theory Set_Ext

(* Title: Examples/SML_Relativization/Foundations/Set_Ext.thy
   Author: Mihails Milehins
   Copyright 2021 (C) Mihails Milehins
*)
section‹Extension of the theory text‹Set›
theory Set_Ext
  imports Main
begin

lemma set_comp_pair: "{f t r |t r. P t r} = {x. t r. P t r  x = (f t r)}"
  by auto

lemma image_iff': "(xA. f x  B) = (f ` A  B)" by auto

text‹\newpage›

end