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)
```