Home | Intuitionistic Logic Explorer Theorem List (p. 39 of 94) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | brun 3801 | The union of two binary relations. (Contributed by NM, 21-Dec-2008.) |
⊢ (A(𝑅 ∪ 𝑆)B ↔ (A𝑅B ∨ A𝑆B)) | ||
Theorem | brin 3802 | The intersection of two relations. (Contributed by FL, 7-Oct-2008.) |
⊢ (A(𝑅 ∩ 𝑆)B ↔ (A𝑅B ∧ A𝑆B)) | ||
Theorem | brdif 3803 | The difference of two binary relations. (Contributed by Scott Fenton, 11-Apr-2011.) |
⊢ (A(𝑅 ∖ 𝑆)B ↔ (A𝑅B ∧ ¬ A𝑆B)) | ||
Theorem | sbcbrg 3804 | Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ (A ∈ 𝐷 → ([A / x]B𝑅𝐶 ↔ ⦋A / x⦌B⦋A / x⦌𝑅⦋A / x⦌𝐶)) | ||
Theorem | sbcbr12g 3805* | Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.) |
⊢ (A ∈ 𝐷 → ([A / x]B𝑅𝐶 ↔ ⦋A / x⦌B𝑅⦋A / x⦌𝐶)) | ||
Theorem | sbcbr1g 3806* | Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.) |
⊢ (A ∈ 𝐷 → ([A / x]B𝑅𝐶 ↔ ⦋A / x⦌B𝑅𝐶)) | ||
Theorem | sbcbr2g 3807* | Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.) |
⊢ (A ∈ 𝐷 → ([A / x]B𝑅𝐶 ↔ B𝑅⦋A / x⦌𝐶)) | ||
Syntax | copab 3808 | Extend class notation to include ordered-pair class abstraction (class builder). |
class {⟨x, y⟩ ∣ φ} | ||
Syntax | cmpt 3809 | Extend the definition of a class to include maps-to notation for defining a function via a rule. |
class (x ∈ A ↦ B) | ||
Definition | df-opab 3810* | Define the class abstraction of a collection of ordered pairs. Definition 3.3 of [Monk1] p. 34. Usually x and y are distinct, although the definition doesn't strictly require it. The brace notation is called "class abstraction" by Quine; it is also (more commonly) called a "class builder" in the literature. (Contributed by NM, 4-Jul-1994.) |
⊢ {⟨x, y⟩ ∣ φ} = {z ∣ ∃x∃y(z = ⟨x, y⟩ ∧ φ)} | ||
Definition | df-mpt 3811* | Define maps-to notation for defining a function via a rule. Read as "the function defined by the map from x (in A) to B(x)." The class expression B is the value of the function at x and normally contains the variable x. Similar to the definition of mapping in [ChoquetDD] p. 2. (Contributed by NM, 17-Feb-2008.) |
⊢ (x ∈ A ↦ B) = {⟨x, y⟩ ∣ (x ∈ A ∧ y = B)} | ||
Theorem | opabss 3812* | The collection of ordered pairs in a class is a subclass of it. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ {⟨x, y⟩ ∣ x𝑅y} ⊆ 𝑅 | ||
Theorem | opabbid 3813 | Equivalent wff's yield equal ordered-pair class abstractions (deduction rule). (Contributed by NM, 21-Feb-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ Ⅎxφ & ⊢ Ⅎyφ & ⊢ (φ → (ψ ↔ χ)) ⇒ ⊢ (φ → {⟨x, y⟩ ∣ ψ} = {⟨x, y⟩ ∣ χ}) | ||
Theorem | opabbidv 3814* | Equivalent wff's yield equal ordered-pair class abstractions (deduction rule). (Contributed by NM, 15-May-1995.) |
⊢ (φ → (ψ ↔ χ)) ⇒ ⊢ (φ → {⟨x, y⟩ ∣ ψ} = {⟨x, y⟩ ∣ χ}) | ||
Theorem | opabbii 3815 | Equivalent wff's yield equal class abstractions. (Contributed by NM, 15-May-1995.) |
⊢ (φ ↔ ψ) ⇒ ⊢ {⟨x, y⟩ ∣ φ} = {⟨x, y⟩ ∣ ψ} | ||
Theorem | nfopab 3816* | Bound-variable hypothesis builder for class abstraction. (Contributed by NM, 1-Sep-1999.) (Unnecessary distinct variable restrictions were removed by Andrew Salmon, 11-Jul-2011.) |
⊢ Ⅎzφ ⇒ ⊢ Ⅎz{⟨x, y⟩ ∣ φ} | ||
Theorem | nfopab1 3817 | The first abstraction variable in an ordered-pair class abstraction (class builder) is effectively not free. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 14-Oct-2016.) |
⊢ Ⅎx{⟨x, y⟩ ∣ φ} | ||
Theorem | nfopab2 3818 | The second abstraction variable in an ordered-pair class abstraction (class builder) is effectively not free. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 14-Oct-2016.) |
⊢ Ⅎy{⟨x, y⟩ ∣ φ} | ||
Theorem | cbvopab 3819* | Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 14-Sep-2003.) |
⊢ Ⅎzφ & ⊢ Ⅎwφ & ⊢ Ⅎxψ & ⊢ Ⅎyψ & ⊢ ((x = z ∧ y = w) → (φ ↔ ψ)) ⇒ ⊢ {⟨x, y⟩ ∣ φ} = {⟨z, w⟩ ∣ ψ} | ||
Theorem | cbvopabv 3820* | Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 15-Oct-1996.) |
⊢ ((x = z ∧ y = w) → (φ ↔ ψ)) ⇒ ⊢ {⟨x, y⟩ ∣ φ} = {⟨z, w⟩ ∣ ψ} | ||
Theorem | cbvopab1 3821* | Change first bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 6-Oct-2004.) (Revised by Mario Carneiro, 14-Oct-2016.) |
⊢ Ⅎzφ & ⊢ Ⅎxψ & ⊢ (x = z → (φ ↔ ψ)) ⇒ ⊢ {⟨x, y⟩ ∣ φ} = {⟨z, y⟩ ∣ ψ} | ||
Theorem | cbvopab2 3822* | Change second bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 22-Aug-2013.) |
⊢ Ⅎzφ & ⊢ Ⅎyψ & ⊢ (y = z → (φ ↔ ψ)) ⇒ ⊢ {⟨x, y⟩ ∣ φ} = {⟨x, z⟩ ∣ ψ} | ||
Theorem | cbvopab1s 3823* | Change first bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 31-Jul-2003.) |
⊢ {⟨x, y⟩ ∣ φ} = {⟨z, y⟩ ∣ [z / x]φ} | ||
Theorem | cbvopab1v 3824* | Rule used to change the first bound variable in an ordered pair abstraction, using implicit substitution. (Contributed by NM, 31-Jul-2003.) (Proof shortened by Eric Schmidt, 4-Apr-2007.) |
⊢ (x = z → (φ ↔ ψ)) ⇒ ⊢ {⟨x, y⟩ ∣ φ} = {⟨z, y⟩ ∣ ψ} | ||
Theorem | cbvopab2v 3825* | Rule used to change the second bound variable in an ordered pair abstraction, using implicit substitution. (Contributed by NM, 2-Sep-1999.) |
⊢ (y = z → (φ ↔ ψ)) ⇒ ⊢ {⟨x, y⟩ ∣ φ} = {⟨x, z⟩ ∣ ψ} | ||
Theorem | csbopabg 3826* | Move substitution into a class abstraction. (Contributed by NM, 6-Aug-2007.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) |
⊢ (A ∈ 𝑉 → ⦋A / x⦌{⟨y, z⟩ ∣ φ} = {⟨y, z⟩ ∣ [A / x]φ}) | ||
Theorem | unopab 3827 | Union of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002.) |
⊢ ({⟨x, y⟩ ∣ φ} ∪ {⟨x, y⟩ ∣ ψ}) = {⟨x, y⟩ ∣ (φ ∨ ψ)} | ||
Theorem | mpteq12f 3828 | An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
⊢ ((∀x A = 𝐶 ∧ ∀x ∈ A B = 𝐷) → (x ∈ A ↦ B) = (x ∈ 𝐶 ↦ 𝐷)) | ||
Theorem | mpteq12dva 3829* | An equality inference for the maps to notation. (Contributed by Mario Carneiro, 26-Jan-2017.) |
⊢ (φ → A = 𝐶) & ⊢ ((φ ∧ x ∈ A) → B = 𝐷) ⇒ ⊢ (φ → (x ∈ A ↦ B) = (x ∈ 𝐶 ↦ 𝐷)) | ||
Theorem | mpteq12dv 3830* | An equality inference for the maps to notation. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 16-Dec-2013.) |
⊢ (φ → A = 𝐶) & ⊢ (φ → B = 𝐷) ⇒ ⊢ (φ → (x ∈ A ↦ B) = (x ∈ 𝐶 ↦ 𝐷)) | ||
Theorem | mpteq12 3831* | An equality theorem for the maps to notation. (Contributed by NM, 16-Dec-2013.) |
⊢ ((A = 𝐶 ∧ ∀x ∈ A B = 𝐷) → (x ∈ A ↦ B) = (x ∈ 𝐶 ↦ 𝐷)) | ||
Theorem | mpteq1 3832* | An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
⊢ (A = B → (x ∈ A ↦ 𝐶) = (x ∈ B ↦ 𝐶)) | ||
Theorem | mpteq1d 3833* | An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 11-Jun-2016.) |
⊢ (φ → A = B) ⇒ ⊢ (φ → (x ∈ A ↦ 𝐶) = (x ∈ B ↦ 𝐶)) | ||
Theorem | mpteq2ia 3834 | An equality inference for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
⊢ (x ∈ A → B = 𝐶) ⇒ ⊢ (x ∈ A ↦ B) = (x ∈ A ↦ 𝐶) | ||
Theorem | mpteq2i 3835 | An equality inference for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
⊢ B = 𝐶 ⇒ ⊢ (x ∈ A ↦ B) = (x ∈ A ↦ 𝐶) | ||
Theorem | mpteq12i 3836 | An equality inference for the maps to notation. (Contributed by Scott Fenton, 27-Oct-2010.) (Revised by Mario Carneiro, 16-Dec-2013.) |
⊢ A = 𝐶 & ⊢ B = 𝐷 ⇒ ⊢ (x ∈ A ↦ B) = (x ∈ 𝐶 ↦ 𝐷) | ||
Theorem | mpteq2da 3837 | Slightly more general equality inference for the maps to notation. (Contributed by FL, 14-Sep-2013.) (Revised by Mario Carneiro, 16-Dec-2013.) |
⊢ Ⅎxφ & ⊢ ((φ ∧ x ∈ A) → B = 𝐶) ⇒ ⊢ (φ → (x ∈ A ↦ B) = (x ∈ A ↦ 𝐶)) | ||
Theorem | mpteq2dva 3838* | Slightly more general equality inference for the maps to notation. (Contributed by Scott Fenton, 25-Apr-2012.) |
⊢ ((φ ∧ x ∈ A) → B = 𝐶) ⇒ ⊢ (φ → (x ∈ A ↦ B) = (x ∈ A ↦ 𝐶)) | ||
Theorem | mpteq2dv 3839* | An equality inference for the maps to notation. (Contributed by Mario Carneiro, 23-Aug-2014.) |
⊢ (φ → B = 𝐶) ⇒ ⊢ (φ → (x ∈ A ↦ B) = (x ∈ A ↦ 𝐶)) | ||
Theorem | nfmpt 3840* | Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.) |
⊢ ℲxA & ⊢ ℲxB ⇒ ⊢ Ⅎx(y ∈ A ↦ B) | ||
Theorem | nfmpt1 3841 | Bound-variable hypothesis builder for the maps-to notation. (Contributed by FL, 17-Feb-2008.) |
⊢ Ⅎx(x ∈ A ↦ B) | ||
Theorem | cbvmpt 3842* | Rule to change the bound variable in a maps-to function, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. (Contributed by NM, 11-Sep-2011.) |
⊢ ℲyB & ⊢ Ⅎx𝐶 & ⊢ (x = y → B = 𝐶) ⇒ ⊢ (x ∈ A ↦ B) = (y ∈ A ↦ 𝐶) | ||
Theorem | cbvmptv 3843* | Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by Mario Carneiro, 19-Feb-2013.) |
⊢ (x = y → B = 𝐶) ⇒ ⊢ (x ∈ A ↦ B) = (y ∈ A ↦ 𝐶) | ||
Theorem | mptv 3844* | Function with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013.) |
⊢ (x ∈ V ↦ B) = {⟨x, y⟩ ∣ y = B} | ||
Syntax | wtr 3845 | Extend wff notation to include transitive classes. Notation from [TakeutiZaring] p. 35. |
wff Tr A | ||
Definition | df-tr 3846 | Define the transitive class predicate. Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 3847 (which is suggestive of the word "transitive"), dftr3 3849, dftr4 3850, and dftr5 3848. The term "complete" is used instead of "transitive" in Definition 3 of [Suppes] p. 130. (Contributed by NM, 29-Aug-1993.) |
⊢ (Tr A ↔ ∪ A ⊆ A) | ||
Theorem | dftr2 3847* | An alternate way of defining a transitive class. Exercise 7 of [TakeutiZaring] p. 40. (Contributed by NM, 24-Apr-1994.) |
⊢ (Tr A ↔ ∀x∀y((x ∈ y ∧ y ∈ A) → x ∈ A)) | ||
Theorem | dftr5 3848* | An alternate way of defining a transitive class. (Contributed by NM, 20-Mar-2004.) |
⊢ (Tr A ↔ ∀x ∈ A ∀y ∈ x y ∈ A) | ||
Theorem | dftr3 3849* | An alternate way of defining a transitive class. Definition 7.1 of [TakeutiZaring] p. 35. (Contributed by NM, 29-Aug-1993.) |
⊢ (Tr A ↔ ∀x ∈ A x ⊆ A) | ||
Theorem | dftr4 3850 | An alternate way of defining a transitive class. Definition of [Enderton] p. 71. (Contributed by NM, 29-Aug-1993.) |
⊢ (Tr A ↔ A ⊆ 𝒫 A) | ||
Theorem | treq 3851 | Equality theorem for the transitive class predicate. (Contributed by NM, 17-Sep-1993.) |
⊢ (A = B → (Tr A ↔ Tr B)) | ||
Theorem | trel 3852 | In a transitive class, the membership relation is transitive. (Contributed by NM, 19-Apr-1994.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ (Tr A → ((B ∈ 𝐶 ∧ 𝐶 ∈ A) → B ∈ A)) | ||
Theorem | trel3 3853 | In a transitive class, the membership relation is transitive. (Contributed by NM, 19-Apr-1994.) |
⊢ (Tr A → ((B ∈ 𝐶 ∧ 𝐶 ∈ 𝐷 ∧ 𝐷 ∈ A) → B ∈ A)) | ||
Theorem | trss 3854 | An element of a transitive class is a subset of the class. (Contributed by NM, 7-Aug-1994.) |
⊢ (Tr A → (B ∈ A → B ⊆ A)) | ||
Theorem | trin 3855 | The intersection of transitive classes is transitive. (Contributed by NM, 9-May-1994.) |
⊢ ((Tr A ∧ Tr B) → Tr (A ∩ B)) | ||
Theorem | tr0 3856 | The empty set is transitive. (Contributed by NM, 16-Sep-1993.) |
⊢ Tr ∅ | ||
Theorem | trv 3857 | The universe is transitive. (Contributed by NM, 14-Sep-2003.) |
⊢ Tr V | ||
Theorem | triun 3858* | The indexed union of a class of transitive sets is transitive. (Contributed by Mario Carneiro, 16-Nov-2014.) |
⊢ (∀x ∈ A Tr B → Tr ∪ x ∈ A B) | ||
Theorem | truni 3859* | The union of a class of transitive sets is transitive. Exercise 5(a) of [Enderton] p. 73. (Contributed by Scott Fenton, 21-Feb-2011.) (Proof shortened by Mario Carneiro, 26-Apr-2014.) |
⊢ (∀x ∈ A Tr x → Tr ∪ A) | ||
Theorem | trint 3860* | The intersection of a class of transitive sets is transitive. Exercise 5(b) of [Enderton] p. 73. (Contributed by Scott Fenton, 25-Feb-2011.) |
⊢ (∀x ∈ A Tr x → Tr ∩ A) | ||
Theorem | trintssm 3861* | If A is transitive and inhabited, then ∩ A is a subset of A. (Contributed by Jim Kingdon, 22-Aug-2018.) |
⊢ ((∃x x ∈ A ∧ Tr A) → ∩ A ⊆ A) | ||
Theorem | trint0m 3862* | Any inhabited transitive class includes its intersection. Similar to Exercise 2 in [TakeutiZaring] p. 44. (Contributed by Jim Kingdon, 22-Aug-2018.) |
⊢ ((Tr A ∧ ∃x x ∈ A) → ∩ A ⊆ A) | ||
Axiom | ax-coll 3863* | Axiom of Collection. Axiom 7 of [Crosilla], p. "Axioms of CZF and IZF" (with unnecessary quantifier removed). It is similar to bnd 3916 but uses a freeness hypothesis in place of one of the distinct variable constraints. (Contributed by Jim Kingdon, 23-Aug-2018.) |
⊢ Ⅎ𝑏φ ⇒ ⊢ (∀x ∈ 𝑎 ∃yφ → ∃𝑏∀x ∈ 𝑎 ∃y ∈ 𝑏 φ) | ||
Theorem | repizf 3864* | Axiom of Replacement. Axiom 7' of [Crosilla], p. "Axioms of CZF and IZF" (with unnecessary quantifier removed). In our context this is not an axiom, but a theorem proved from ax-coll 3863. It is identical to zfrep6 3865 except for the choice of a freeness hypothesis rather than a distinct variable constraint between 𝑏 and φ. (Contributed by Jim Kingdon, 23-Aug-2018.) |
⊢ Ⅎ𝑏φ ⇒ ⊢ (∀x ∈ 𝑎 ∃!yφ → ∃𝑏∀x ∈ 𝑎 ∃y ∈ 𝑏 φ) | ||
Theorem | zfrep6 3865* | A version of the Axiom of Replacement. Normally φ would have free variables x and y. Axiom 6 of [Kunen] p. 12. The Separation Scheme ax-sep 3866 cannot be derived from this version and must be stated as a separate axiom in an axiom system (such as Kunen's) that uses this version. (Contributed by NM, 10-Oct-2003.) |
⊢ (∀x ∈ z ∃!yφ → ∃w∀x ∈ z ∃y ∈ w φ) | ||
Axiom | ax-sep 3866* |
The Axiom of Separation of IZF set theory. Axiom 6 of [Crosilla], p.
"Axioms of CZF and IZF" (with unnecessary quantifier removed,
and with a
Ⅎyφ condition replaced by a distinct
variable constraint between
y and φ).
The Separation Scheme is a weak form of Frege's Axiom of Comprehension, conditioning it (with x ∈ z) so that it asserts the existence of a collection only if it is smaller than some other collection z that already exists. This prevents Russell's paradox ru 2757. In some texts, this scheme is called "Aussonderung" or the Subset Axiom. (Contributed by NM, 11-Sep-2006.) |
⊢ ∃y∀x(x ∈ y ↔ (x ∈ z ∧ φ)) | ||
Theorem | axsep2 3867* | A less restrictive version of the Separation Scheme ax-sep 3866, where variables x and z can both appear free in the wff φ, which can therefore be thought of as φ(x, z). This version was derived from the more restrictive ax-sep 3866 with no additional set theory axioms. (Contributed by NM, 10-Dec-2006.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) |
⊢ ∃y∀x(x ∈ y ↔ (x ∈ z ∧ φ)) | ||
Theorem | zfauscl 3868* | Separation Scheme (Aussonderung) using a class variable. To derive this from ax-sep 3866, we invoke the Axiom of Extensionality (indirectly via vtocl 2602), which is needed for the justification of class variable notation. (Contributed by NM, 5-Aug-1993.) |
⊢ A ∈ V ⇒ ⊢ ∃y∀x(x ∈ y ↔ (x ∈ A ∧ φ)) | ||
Theorem | bm1.3ii 3869* | Convert implication to equivalence using the Separation Scheme (Aussonderung) ax-sep 3866. Similar to Theorem 1.3ii of [BellMachover] p. 463. (Contributed by NM, 5-Aug-1993.) |
⊢ ∃x∀y(φ → y ∈ x) ⇒ ⊢ ∃x∀y(y ∈ x ↔ φ) | ||
Theorem | a9evsep 3870* | Derive a weakened version of ax-i9 1420, where x and y must be distinct, from Separation ax-sep 3866 and Extensionality ax-ext 2019. The theorem ¬ ∀x¬ x = y also holds (ax9vsep 3871), but in intuitionistic logic ∃xx = y is stronger. (Contributed by Jim Kingdon, 25-Aug-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ∃x x = y | ||
Theorem | ax9vsep 3871* | Derive a weakened version of ax-9 1421, where x and y must be distinct, from Separation ax-sep 3866 and Extensionality ax-ext 2019. In intuitionistic logic a9evsep 3870 is stronger and also holds. (Contributed by NM, 12-Nov-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ¬ ∀x ¬ x = y | ||
Theorem | zfnuleu 3872* | Show the uniqueness of the empty set (using the Axiom of Extensionality via bm1.1 2022 to strengthen the hypothesis in the form of axnul 3873). (Contributed by NM, 22-Dec-2007.) |
⊢ ∃x∀y ¬ y ∈ x ⇒ ⊢ ∃!x∀y ¬ y ∈ x | ||
Theorem | axnul 3873* |
The Null Set Axiom of ZF set theory: there exists a set with no
elements. Axiom of Empty Set of [Enderton] p. 18. In some textbooks,
this is presented as a separate axiom; here we show it can be derived
from Separation ax-sep 3866. This version of the Null Set Axiom tells us
that at least one empty set exists, but does not tell us that it is
unique - we need the Axiom of Extensionality to do that (see
zfnuleu 3872).
This theorem should not be referenced by any proof. Instead, use ax-nul 3874 below so that the uses of the Null Set Axiom can be more easily identified. (Contributed by Jeff Hoffman, 3-Feb-2008.) (Revised by NM, 4-Feb-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ∃x∀y ¬ y ∈ x | ||
Axiom | ax-nul 3874* | The Null Set Axiom of IZF set theory. It was derived as axnul 3873 above and is therefore redundant, but we state it as a separate axiom here so that its uses can be identified more easily. Axiom 4 of [Crosilla] p. "Axioms of CZF and IZF". (Contributed by NM, 7-Aug-2003.) |
⊢ ∃x∀y ¬ y ∈ x | ||
Theorem | 0ex 3875 | The Null Set Axiom of ZF set theory: the empty set exists. Corollary 5.16 of [TakeutiZaring] p. 20. For the unabbreviated version, see ax-nul 3874. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ ∅ ∈ V | ||
Theorem | csbexga 3876 | The existence of proper substitution into a class. (Contributed by NM, 10-Nov-2005.) |
⊢ ((A ∈ 𝑉 ∧ ∀x B ∈ 𝑊) → ⦋A / x⦌B ∈ V) | ||
Theorem | csbexa 3877 | The existence of proper substitution into a class. (Contributed by NM, 7-Aug-2007.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ ⦋A / x⦌B ∈ V | ||
Theorem | nalset 3878* | No set contains all sets. Theorem 41 of [Suppes] p. 30. (Contributed by NM, 23-Aug-1993.) |
⊢ ¬ ∃x∀y y ∈ x | ||
Theorem | vprc 3879 | The universal class is not a member of itself (and thus is not a set). Proposition 5.21 of [TakeutiZaring] p. 21; our proof, however, does not depend on the Axiom of Regularity. (Contributed by NM, 23-Aug-1993.) |
⊢ ¬ V ∈ V | ||
Theorem | nvel 3880 | The universal class doesn't belong to any class. (Contributed by FL, 31-Dec-2006.) |
⊢ ¬ V ∈ A | ||
Theorem | vnex 3881 | The universal class does not exist. (Contributed by NM, 4-Jul-2005.) |
⊢ ¬ ∃x x = V | ||
Theorem | inex1 3882 | Separation Scheme (Aussonderung) using class notation. Compare Exercise 4 of [TakeutiZaring] p. 22. (Contributed by NM, 5-Aug-1993.) |
⊢ A ∈ V ⇒ ⊢ (A ∩ B) ∈ V | ||
Theorem | inex2 3883 | Separation Scheme (Aussonderung) using class notation. (Contributed by NM, 27-Apr-1994.) |
⊢ A ∈ V ⇒ ⊢ (B ∩ A) ∈ V | ||
Theorem | inex1g 3884 | Closed-form, generalized Separation Scheme. (Contributed by NM, 7-Apr-1995.) |
⊢ (A ∈ 𝑉 → (A ∩ B) ∈ V) | ||
Theorem | ssex 3885 | The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22. This is one way to express the Axiom of Separation ax-sep 3866 (a.k.a. Subset Axiom). (Contributed by NM, 27-Apr-1994.) |
⊢ B ∈ V ⇒ ⊢ (A ⊆ B → A ∈ V) | ||
Theorem | ssexi 3886 | The subset of a set is also a set. (Contributed by NM, 9-Sep-1993.) |
⊢ B ∈ V & ⊢ A ⊆ B ⇒ ⊢ A ∈ V | ||
Theorem | ssexg 3887 | The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22 (generalized). (Contributed by NM, 14-Aug-1994.) |
⊢ ((A ⊆ B ∧ B ∈ 𝐶) → A ∈ V) | ||
Theorem | ssexd 3888 | A subclass of a set is a set. Deduction form of ssexg 3887. (Contributed by David Moews, 1-May-2017.) |
⊢ (φ → B ∈ 𝐶) & ⊢ (φ → A ⊆ B) ⇒ ⊢ (φ → A ∈ V) | ||
Theorem | difexg 3889 | Existence of a difference. (Contributed by NM, 26-May-1998.) |
⊢ (A ∈ 𝑉 → (A ∖ B) ∈ V) | ||
Theorem | zfausab 3890* | Separation Scheme (Aussonderung) in terms of a class abstraction. (Contributed by NM, 8-Jun-1994.) |
⊢ A ∈ V ⇒ ⊢ {x ∣ (x ∈ A ∧ φ)} ∈ V | ||
Theorem | rabexg 3891* | Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 23-Oct-1999.) |
⊢ (A ∈ 𝑉 → {x ∈ A ∣ φ} ∈ V) | ||
Theorem | rabex 3892* | Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 19-Jul-1996.) |
⊢ A ∈ V ⇒ ⊢ {x ∈ A ∣ φ} ∈ V | ||
Theorem | elssabg 3893* | Membership in a class abstraction involving a subset. Unlike elabg 2682, A does not have to be a set. (Contributed by NM, 29-Aug-2006.) |
⊢ (x = A → (φ ↔ ψ)) ⇒ ⊢ (B ∈ 𝑉 → (A ∈ {x ∣ (x ⊆ B ∧ φ)} ↔ (A ⊆ B ∧ ψ))) | ||
Theorem | inteximm 3894* | The intersection of an inhabited class exists. (Contributed by Jim Kingdon, 27-Aug-2018.) |
⊢ (∃x x ∈ A → ∩ A ∈ V) | ||
Theorem | intexr 3895 | If the intersection of a class exists, the class is non-empty. (Contributed by Jim Kingdon, 27-Aug-2018.) |
⊢ (∩ A ∈ V → A ≠ ∅) | ||
Theorem | intnexr 3896 | If a class intersection is the universe, it is not a set. In classical logic this would be an equivalence. (Contributed by Jim Kingdon, 27-Aug-2018.) |
⊢ (∩ A = V → ¬ ∩ A ∈ V) | ||
Theorem | intexabim 3897 | The intersection of an inhabited class abstraction exists. (Contributed by Jim Kingdon, 27-Aug-2018.) |
⊢ (∃xφ → ∩ {x ∣ φ} ∈ V) | ||
Theorem | intexrabim 3898 | The intersection of an inhabited restricted class abstraction exists. (Contributed by Jim Kingdon, 27-Aug-2018.) |
⊢ (∃x ∈ A φ → ∩ {x ∈ A ∣ φ} ∈ V) | ||
Theorem | iinexgm 3899* | The existence of an indexed union. x is normally a free-variable parameter in B, which should be read B(x). (Contributed by Jim Kingdon, 28-Aug-2018.) |
⊢ ((∃x x ∈ A ∧ ∀x ∈ A B ∈ 𝐶) → ∩ x ∈ A B ∈ V) | ||
Theorem | inuni 3900* | The intersection of a union ∪ A with a class B is equal to the union of the intersections of each element of A with B. (Contributed by FL, 24-Mar-2007.) |
⊢ (∪ A ∩ B) = ∪ {x ∣ ∃y ∈ A x = (y ∩ B)} |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |