src/ZF/Epsilon.thy
changeset 63901 4ce989e962e0
parent 60770 240563fbf41d
child 68490 eb53f944c8cd
     1.1 --- a/src/ZF/Epsilon.thy	Fri Sep 16 18:09:13 2016 +0200
     1.2 +++ b/src/ZF/Epsilon.thy	Fri Sep 16 21:28:09 2016 +0200
     1.3 @@ -305,7 +305,7 @@
     1.4  (*Not clear how to remove the P(a) condition, since the "then" part
     1.5    must refer to "a"*)
     1.6  lemma the_equality_if:
     1.7 -     "P(a) ==> (THE x. P(x)) = (if (EX!x. P(x)) then a else 0)"
     1.8 +     "P(a) ==> (THE x. P(x)) = (if (\<exists>!x. P(x)) then a else 0)"
     1.9  by (simp add: the_0 the_equality2)
    1.10  
    1.11  (*The first premise not only fixs i but ensures @{term"f\<noteq>0"}.