src/ZF/upair.thy
changeset 63901 4ce989e962e0
parent 61798 27f3c10b0b50
child 65449 c82e63b11b8b
     1.1 --- a/src/ZF/upair.thy	Fri Sep 16 18:09:13 2016 +0200
     1.2 +++ b/src/ZF/upair.thy	Fri Sep 16 21:28:09 2016 +0200
     1.3 @@ -156,11 +156,11 @@
     1.4  apply (fast dest: subst)
     1.5  done
     1.6  
     1.7 -(* Only use this if you already know EX!x. P(x) *)
     1.8 -lemma the_equality2: "[| EX! x. P(x);  P(a) |] ==> (THE x. P(x)) = a"
     1.9 +(* Only use this if you already know \<exists>!x. P(x) *)
    1.10 +lemma the_equality2: "[| \<exists>!x. P(x);  P(a) |] ==> (THE x. P(x)) = a"
    1.11  by blast
    1.12  
    1.13 -lemma theI: "EX! x. P(x) ==> P(THE x. P(x))"
    1.14 +lemma theI: "\<exists>!x. P(x) ==> P(THE x. P(x))"
    1.15  apply (erule ex1E)
    1.16  apply (subst the_equality)
    1.17  apply (blast+)
    1.18 @@ -170,14 +170,14 @@
    1.19    @{term "THE x.P(x)"}  rewrites to @{term "THE x.Q(x)"} *)
    1.20  
    1.21  (*If it's "undefined", it's zero!*)
    1.22 -lemma the_0: "~ (EX! x. P(x)) ==> (THE x. P(x))=0"
    1.23 +lemma the_0: "~ (\<exists>!x. P(x)) ==> (THE x. P(x))=0"
    1.24  apply (unfold the_def)
    1.25  apply (blast elim!: ReplaceE)
    1.26  done
    1.27  
    1.28  (*Easier to apply than theI: conclusion has only one occurrence of P*)
    1.29  lemma theI2:
    1.30 -    assumes p1: "~ Q(0) ==> EX! x. P(x)"
    1.31 +    assumes p1: "~ Q(0) ==> \<exists>!x. P(x)"
    1.32          and p2: "!!x. P(x) ==> Q(x)"
    1.33      shows "Q(THE x. P(x))"
    1.34  apply (rule classical)