Metamath Proof Explorer - mmtheorems18

Jump to page: 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5787

Statement List for Metamath Proof Explorer - 1701-1800 - Page 18 of 58

Type	Label	Description
Statement
Theorem	ssexi 1701	The subset of a set is also a set.
⊢ B ∈ V    &   ⊢ A ⊆ B    ⇒   ⊢ A ∈ V
Theorem	ssexg 1702	The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22 (generalized).
⊢ (B ∈ C → (A ⊆ B → A ∈ V))
Theorem	difexg 1703	Existence of a difference.
⊢ (A ∈ C → (A ∖ B) ∈ V)
Theorem	zfausab 1704	Separation Scheme in terms of a class abstraction.
⊢ A ∈ V    ⇒   ⊢ {x∣(x ∈ A ∧ φ)} ∈ V
Theorem	rabexg 1705	Separation Scheme in terms of a restricted class abstraction.
⊢ (A ∈ B → {x ∈ A∣φ} ∈ V)
Theorem	rabex 1706	Separation Scheme in terms of a restricted class abstraction.
⊢ A ∈ V    ⇒   ⊢ {x ∈ A∣φ} ∈ V
Syntax	c0 1707	Extend class notation to include the empty set.
class ∅
Definition	df-nul 1708	Define the empty set. Special case of Exercise 4.10(o) of [Mendelson] p. 231. For a more traditional definition, but requiring a dummy variable, see dfnul2 1709.
⊢ ∅ = (V ∖ V)
Theorem	dfnul2 1709	Alternate definition of the empty set. Definition 5.14 of [TakeutiZaring] p. 20.
⊢ ∅ = {x∣ ¬ x = x}
Theorem	dfnul3 1710	Alternate definition of the empty set..
⊢ ∅ = {x ∈ A∣ ¬ x ∈ A}
Theorem	noel 1711	The empty set has no elements. Theorem 6.14 of [Quine] p. 44.
⊢ ¬ A ∈ ∅
Theorem	n0i 1712	If a set has elements, it is not empty.
⊢ (B ∈ A → ¬ A = ∅)
Theorem	n0f 1713	A nonempty class has at least one element. Proposition 5.17(1) of [TakeutiZaring] p. 20. This version of n0 1714 requires only that x not be free in, rather than not occur in, A.
⊢ (y ∈ A → ∀x y ∈ A)    ⇒   ⊢ (¬ A = ∅ ↔ ∃x x ∈ A)
Theorem	n0 1714	A nonempty class has at least one element. Proposition 5.17(1) of [TakeutiZaring] p. 20.
⊢ (¬ A = ∅ ↔ ∃x x ∈ A)
Theorem	abn0 1715	Non-empty class abstraction.
⊢ (¬ {x∣φ} = ∅ ↔ ∃xφ)
Theorem	rabn0 1716	Non-empty restricted class abstraction.
⊢ (¬ {x ∈ A∣φ} = ∅ ↔ ∃x ∈ A φ)
Theorem	rex0 1717	Existential quantification restricted to the empty set is false.
⊢ ¬ ∃x ∈ ∅ φ
Theorem	rab0 1718	Any restricted class abstraction restricted to the empty set is empty.
⊢ {x ∈ ∅∣φ} = ∅
Theorem	eq0 1719	The empty set has no elements. Theorem 2 of [Suppes] p. 22.
⊢ (A = ∅ ↔ ∀x ¬ x ∈ A)
Theorem	0el 1720	Membership of the empty set in another class.
⊢ (∅ ∈ A ↔ ∃x ∈ A ∀y ¬ y ∈ x)
Theorem	un0 1721	The union of a class with the empty set is itself. Theorem 24 of [Suppes] p. 27.
⊢ (A ∪ ∅) = A
Theorem	in0 1722	The intersection of a class with the empty set is the empty set. Theorem 16 of [Suppes] p. 26.
⊢ (A ∩ ∅) = ∅
Theorem	inv 1723	The intersection of a class with the universal class is itself. Exercise 4.10(k) of [Mendelson] p. 231.
⊢ (A ∩ V) = A
Theorem	unv 1724	The union of a class with the universal class is the universal class. Exercise 4.10(l) of [Mendelson] p. 231.
⊢ (A ∪ V) = V
Theorem	0ss 1725	The null set is a subset of any class. Part of Exercise 1 of [TakeutiZaring] p. 22.
⊢ ∅ ⊆ A
Theorem	ss0b 1726	Any subset of the empty set is empty. Theorem 5 of [Suppes] p. 23 and its converse.
⊢ (A ⊆ ∅ ↔ A = ∅)
Theorem	ss0 1727	Any subset of the empty set is empty. Theorem 5 of [Suppes] p. 23.
⊢ (A ⊆ ∅ → A = ∅)
Theorem	un00 1728	Two classes are empty iff their union is empty.
⊢ ((A = ∅ ∧ B = ∅) ↔ (A ∪ B) = ∅)
Theorem	vss 1729	Only the universal class has the universal class as a subclass.
⊢ (V ⊆ A ↔ A = V)
Theorem	0pss 1730	The null set is a proper subset of any non-empty set.
⊢ (∅ ⊂ A ↔ ¬ A = ∅)
Theorem	npss0 1731	No set is a proper subset of the empty set.
⊢ ¬ A ⊂ ∅
Theorem	pssv 1732	Any non-universal class is a proper subclass of the universal class.
⊢ (A ⊂ V ↔ ¬ A = V)
Theorem	disj 1733	Two ways of saying that two classes are disjoint (have no members in common).
⊢ ((A ∩ B) = ∅ ↔ ∀x ∈ A ¬ x ∈ B)
Theorem	disj1 1734	Two ways of saying that two classes are disjoint (have no members in common).
⊢ ((A ∩ B) = ∅ ↔ ∀x(x ∈ A → ¬ x ∈ B))
Theorem	disj2 1735	Two ways of saying that two classes are disjoint.
⊢ ((A ∩ B) = ∅ ↔ A ⊆ (V ∖ B))
Theorem	disj3 1736	Two ways of saying that two classes are disjoint.
⊢ ((A ∩ B) = ∅ ↔ A = (A ∖ B))
Theorem	disj4 1737	Two ways of saying that two classes are disjoint.
⊢ ((A ∩ B) = ∅ ↔ ¬ (A ∖ B) ⊂ A)
Theorem	disjpss 1738	A class is a proper subset of its union with a disjoint nonempty class.
⊢ (((A ∩ B) = ∅ ∧ ¬ B = ∅) → A ⊂ (A ∪ B))
Theorem	undisj1 1739	The union of disjoint classes is disjoint.
⊢ (((A ∩ C) = ∅ ∧ (B ∩ C) = ∅) ↔ ((A ∪ B) ∩ C) = ∅)
Theorem	undisj2 1740	The union of disjoint classes is disjoint.
⊢ (((A ∩ B) = ∅ ∧ (A ∩ C) = ∅) ↔ (A ∩ (B ∪ C)) = ∅)
Theorem	ssindif0 1741	Subclass expressed in terms of intersection with difference from the universal class.
⊢ (A ⊆ B ↔ (A ∩ (V ∖ B)) = ∅)
Theorem	inelcm 1742	The intersection of classes with a common member is nonempty.
⊢ ((A ∈ B ∧ A ∈ C) → ¬ (B ∩ C) = ∅)
Theorem	minel 1743	A minimum element of a class has no elements in common with the class.
⊢ ((A ∈ B ∧ (C ∩ B) = ∅) → ¬ A ∈ C)
Theorem	undif4 1744	Distribute union over difference.
⊢ ((A ∩ C) = ∅ → (A ∪ (B ∖ C)) = ((A ∪ B) ∖ C))
Theorem	0ex 1745	The Null Set axiom of ZF set theory: the empty set exists. Corollary 5.16 of [TakeutiZaring] p. 20. In some textbooks this is presented as a separate axiom; here we show it can be derived from the Extensionality and Replacement axioms. It cannot be derived from these unless our predicate calculus includes an axiom stating that at least one set exists (which it does in the form of ax-9 799). For another version, see zfnul 1746.
⊢ ∅ ∈ V
Theorem	zfnul 1746	Another version of the Null Set axiom, expressed in terms of logical primitives and proved directly from Aussonderung. Axiom of Empty Set of [Enderton] p. 18.
⊢ ∃x∀y ¬ y ∈ x
Theorem	class2set 1747	Construct, from any class A, a set equal to it when the class exists and equal to the empty set when the class is proper. This theorem shows that the constructed set always exists.
⊢ {x ∈ A∣A ∈ V} ∈ V
Theorem	ssdif0 1748	Subclass expressed in terms of difference. Exercise 7 of [TakeutiZaring] p. 22.
⊢ (A ⊆ B ↔ (A ∖ B) = ∅)
Theorem	vdif0 1749	Universal class equality in terms of empty difference.
⊢ (A = V ↔ (V ∖ A) = ∅)
Theorem	pssdifn0 1750	A proper subclass has a nonempty difference.
⊢ ((A ⊆ B ∧ ¬ A = B) → ¬ (B ∖ A) = ∅)
Theorem	ssnelpss 1751	A subclass missing a member is a proper subclass.
⊢ (A ⊆ B → ((C ∈ B ∧ ¬ C ∈ A) → A ⊂ B))
Theorem	pssnel 1752	A proper subclass has a member in one argument that's not in both.
⊢ (A ⊂ B → ∃x(x ∈ B ∧ ¬ x ∈ A))
Theorem	difin0ss 1753	Difference, intersection, and subclass relationship.
⊢ (((A ∖ B) ∩ C) = ∅ → (C ⊆ A → C ⊆ B))
Theorem	inssdif0 1754	Intersection, subclass, and difference relationship.
⊢ ((A ∩ B) ⊆ C ↔ (A ∩ (B ∖ C)) = ∅)
Theorem	difid 1755	The difference between a class and itself is the empty set. Proposition 5.15 of [TakeutiZaring] p. 20. Also Theorem 32 of [Suppes] p. 28.
⊢ (A ∖ A) = ∅
Theorem	dif0 1756	The difference between a class and the empty set. Part of Exercise 4.4 of [Stoll] p. 16.
⊢ (A ∖ ∅) = A
Theorem	0dif 1757	The difference between the empty set and a class. Part of Exercise 4.4 of [Stoll] p. 16.
⊢ (∅ ∖ A) = ∅
Theorem	difdisj 1758	A class and its relative complement are disjoint. Theorem 38 of [Suppes] p. 29.
⊢ (A ∩ (B ∖ A)) = ∅
Theorem	difin0 1759	The difference of a class from its intersection is empty. Theorem 37 of [Suppes] p. 29.
⊢ ((A ∩ B) ∖ B) = ∅
Theorem	undifv 1760	The union of a class and its complement is the universe. Theorem 5.1(5) of [Stoll] p. 17.
⊢ (A ∪ (V ∖ A)) = V
Theorem	undif1 1761	Absorption of difference by union. This decomposes a union into two disjoint classes (see difdisj 1758). Theorem 35 of [Suppes] p. 29.
⊢ ((A ∖ B) ∪ B) = (A ∪ B)
Theorem	undif2 1762	Absorption of difference by union. This decomposes a union into two disjoint classes (see difdisj 1758). Part of proof of Corollary 6K of [Enderton] p. 144.
⊢ (A ∪ (B ∖ A)) = (A ∪ B)
Theorem	difun2 1763	Absorption of union by difference. Theorem 36 of [Suppes] p. 29.
⊢ ((A ∪ B) ∖ B) = (A ∖ B)
Theorem	ssundif 1764	Union of complementary parts into whole.
⊢ (A ⊆ B ↔ (A ∪ (B ∖ A)) = B)
Theorem	difdifdir 1765	Distributive law for class difference. Exercise 4.8 of [Stoll] p. 16.
⊢ ((A ∖ B) ∖ C) = ((A ∖ C) ∖ (B ∖ C))
Theorem	r19.2z 1766	Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 713). The restricted version is valid only when the domain of quantification is not empty.
⊢ (¬ A = ∅ → (∀x ∈ A φ → ∃x ∈ A φ))
Theorem	r19.3rzv 1767	Restricted quantification of wff not containing quantified variable.
⊢ (¬ A = ∅ → (φ ↔ ∀x ∈ A φ))
Theorem	r19.9rzv 1768	Restricted quantification of wff not containing quantified variable.
⊢ (¬ A = ∅ → (φ ↔ ∃x ∈ A φ))
Theorem	r19.28zv 1769	Restricted quantifier version of Theorem 19.28 of [Margaris] p. 90. It is valid only when the domain of quantification is not empty.
⊢ (¬ A = ∅ → (∀x ∈ A (φ ∧ ψ) ↔ (φ ∧ ∀x ∈ A ψ)))
Theorem	r19.45zv 1770	Restricted version of Theorem 19.45 of [Margaris] p. 90.
⊢ (¬ A = ∅ → (∃x ∈ A (φ ∨ ψ) ↔ (φ ∨ ∃x ∈ A ψ)))
Theorem	r19.27zv 1771	Restricted quantifier version of Theorem 19.27 of [Margaris] p. 90. It is valid only when the domain of quantification is not empty.
⊢ (¬ A = ∅ → (∀x ∈ A (φ ∧ ψ) ↔ (∀x ∈ A φ ∧ ψ)))
Theorem	r19.36zv 1772	Restricted quantifier version of Theorem 19.36 of [Margaris] p. 90. It is valid only when the domain of quantification is not empty.
⊢ (¬ A = ∅ → (∃x ∈ A (φ → ψ) ↔ (∀x ∈ A φ → ψ)))
Theorem	rzal 1773	Vacuous quantification makes any wff true.
⊢ (A = ∅ → ∀x ∈ A φ)
Theorem	ralidm 1774	Idempotent law for restricted quantifier.
⊢ (∀x ∈ A ∀x ∈ A φ ↔ ∀x ∈ A φ)
Theorem	raaan 1775	Rearrange restricted quantifiers.
⊢ (∀x ∈ A ∀y ∈ A (φ ∧ ψ) ↔ (∀x ∈ A φ ∧ ∀y ∈ A ψ))
Syntax	cif 1776	Extend class notation to include the conditional operator. See df-if 1777 for a description. In older databases this was called "ded".
class if(φ, A, B)
Definition	df-if 1777	Define the conditional operator. Read if(φ, A, B) as "if φ then A else B." See iftrue 1780 and iffalse 1781 for its values. In mathematical literature, this operator is rarely defined formally but is implicit in informal definitions such as "let f(x)=0 if x=0 and 1/x otherwise." (In older versions of this database, this operator was denoted "ded" and called the "deduction class.") An important use for us is in conjunction with the weak deduction theorem, which converts a hypothesis into an antecedent. In that role, A is a class variable in the hypothesis and B is a class (usually a constant) that makes the hypothesis true when it is substituted for A. See dedth 1784 for the main part of the weak deduction theorem, elimhyp 1790 to eliminate a hypothesis, and keephyp 1794 to keep a hypothesis. See the Deduction Theorem link on the Metamath Proof Explorer Home Page for a description of the weak deduction theorem.
⊢ if(φ, A, B) = {x∣((x ∈ A ∧ φ) ∨ (x ∈ B ∧ ¬ φ))}
Theorem	ifeq1 1778	Equality theorem for conditional operator.
⊢ (A = B → if(φ, A, C) = if(φ, B, C))
Theorem	ifeq2 1779	Equality theorem for conditional operators.
⊢ (B = C → if(φ, A, B) = if(φ, A, C))
Theorem	iftrue 1780	Value of the conditional operator when its first argument is true.
⊢ (φ → if(φ, A, B) = A)
Theorem	iffalse 1781	Value of the conditional operator when its first argument is false.
⊢ (¬ φ → if(φ, A, B) = B)
Theorem	ifeq12 1782	Equality theorem for conditional operators.
⊢ ((A = B ∧ C = D) → if(φ, A, C) = if(φ, B, D))
Theorem	ifbi 1783	Equivalence theorem for conditional operators. (Contributed by Raph Levien, 15-Jan-04.)
⊢ ((φ ↔ ψ) → if(φ, A, B) = if(ψ, A, B))
Theorem	dedth 1784	Weak deduction theorem that eliminates a hypothesis φ, making it become an antecedent. We assume that a proof exists for φ when the class variable A is replaced with a specific class B. The hypothesis χ should be assigned to the inference, and the inference's hypothesis eliminated with elimhyp 1790. If the inference has other hypotheses with class variable A, these can be kept by assigning keephyp 1794 to them. For more information, see the Deduction Theorem link on the Metamath Proof Explorer home page.
⊢ (A = if(φ, A, B) → (ψ ↔ χ))    &   ⊢ χ    ⇒   ⊢ (φ → ψ)
Theorem	dedth2v 1785	Weak deduction theorem for eliminating hypotheses with 2 class variables.
⊢ (A = if(φ, A, C) → (ψ ↔ χ))    &   ⊢ (B = if(φ, B, D) → (χ ↔ θ))    &   ⊢ θ    ⇒   ⊢ (φ → ψ)
Theorem	dedth3v 1786	Weak deduction theorem for eliminating hypothesis with 3 class variables.
⊢ (A = if(φ, A, D) → (ψ ↔ χ))    &   ⊢ (B = if(φ, B, R) → (χ ↔ θ))    &   ⊢ (C = if(φ, C, S) → (θ ↔ τ))    &   ⊢ τ    ⇒   ⊢ (φ → ψ)
Theorem	dedth2h 1787	Weak deduction theorem eliminating two hypotheses.
⊢ (A = if(φ, A, C) → (χ ↔ θ))    &   ⊢ (B = if(ψ, B, D) → (θ ↔ τ))    &   ⊢ τ    ⇒   ⊢ ((φ ∧ ψ) → χ)
Theorem	dedth3h 1788	Weak deduction theorem eliminating three hypotheses.
⊢ (A = if(φ, A, D) → (θ ↔ τ))    &   ⊢ (B = if(ψ, B, R) → (τ ↔ η))    &   ⊢ (C = if(χ, C, S) → (η ↔ ζ))    &   ⊢ ζ    ⇒   ⊢ ((φ ∧ ψ ∧ χ) → θ)
Theorem	dedth4h 1789	Weak deduction theorem eliminating four hypotheses.
⊢ (A = if(φ, A, R) → (τ ↔ η))    &   ⊢ (B = if(ψ, B, S) → (η ↔ ζ))    &   ⊢ (C = if(χ, C, F) → (ζ ↔ σ))    &   ⊢ (D = if(θ, D, G) → (σ ↔ ρ))    &   ⊢ ρ    ⇒   ⊢ (((φ ∧ ψ) ∧ (χ ∧ θ)) → τ)
Theorem	elimhyp 1790	Eliminate a hypothesis containing class variable A when it is known for a specific class B. For more information, see the Deduction Theorem link on the Metamath Proof Explorer home page.
⊢ (A = if(φ, A, B) → (φ ↔ ψ))    &   ⊢ (B = if(φ, A, B) → (χ ↔ ψ))    &   ⊢ χ    ⇒   ⊢ ψ
Theorem	elimhyp2v 1791	Eliminate a hypothesis containing 2 class variables.
⊢ (A = if(φ, A, C) → (φ ↔ χ))    &   ⊢ (B = if(φ, B, D) → (χ ↔ θ))    &   ⊢ (C = if(φ, A, C) → (τ ↔ η))    &   ⊢ (D = if(φ, B, D) → (η ↔ θ))    &   ⊢ τ    ⇒   ⊢ θ
Theorem	elimhyp3v 1792	Eliminate a hypothesis containing 3 class variables.
⊢ (A = if(φ, A, D) → (φ ↔ χ))    &   ⊢ (B = if(φ, B, R) → (χ ↔ θ))    &   ⊢ (C = if(φ, C, S) → (θ ↔ τ))    &   ⊢ (D = if(φ, A, D) → (η ↔ ζ))    &   ⊢ (R = if(φ, B, R) → (ζ ↔ σ))    &   ⊢ (S = if(φ, C, S) → (σ ↔ τ))    &   ⊢ η    ⇒   ⊢ τ
Theorem	elimel 1793	Eliminate a membership hypothesis for weak deduction theorem, when special case B ∈ C is provable.
⊢ B ∈ C    ⇒   ⊢ if(A ∈ C, A, B) ∈ C
Theorem	keephyp 1794	Transform a hypothesis ψ that we want to keep (but contains the same class variable A used in the eliminated hypothesis) for use with the weak deduction theorem.
⊢ (A = if(φ, A, B) → (ψ ↔ θ))    &   ⊢ (B = if(φ, A, B) → (χ ↔ θ))    &   ⊢ ψ    &   ⊢ χ    ⇒   ⊢ θ
Theorem	keephyp3v 1795	Keep a hypothesis containing 3 class variables.
⊢ (A = if(φ, A, D) → (ρ ↔ χ))    &   ⊢ (B = if(φ, B, R) → (χ ↔ θ))    &   ⊢ (C = if(φ, C, S) → (θ ↔ τ))    &   ⊢ (D = if(φ, A, D) → (η ↔ ζ))    &   ⊢ (R = if(φ, B, R) → (ζ ↔ σ))    &   ⊢ (S = if(φ, C, S) → (σ ↔ τ))    &   ⊢ ρ    &   ⊢ η    ⇒   ⊢ τ
Theorem	keepel 1796	Keep a membership hypothesis for weak deduction theorem, when special case B ∈ C is provable.
⊢ A ∈ C    &   ⊢ B ∈ C    ⇒   ⊢ if(φ, A, B) ∈ C
Theorem	ifex 1797	Conditional operator existence.
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ if(φ, A, B) ∈ V
Syntax	cpw 1798	Extend class notation to include power class.
class ℘A
Definition	df-pw 1799	Define power class. Definition 5.10 of [TakeutiZaring] p. 17, but we also let it apply to proper classes, i.e. those that are not members of V.
⊢ ℘A = {x∣x ⊆ A}
Theorem	pweq 1800	Equality theorem for the power class.
⊢ (A = B → ℘A = ℘B)