Metamath Proof Explorer - mmtheorems19

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 - 1801-1900 - Page 19 of 58

Type	Label	Description
Statement
Theorem	elpw 1801	Membership in a power class. Theorem 86 of [Suppes] p. 47.
⊢ A ∈ V    ⇒   ⊢ (A ∈ ℘B ↔ A ⊆ B)
Theorem	elpwg 1802	Membership in a power class. Theorem 86 of [Suppes] p. 47.
⊢ (A ∈ C → (A ∈ ℘B ↔ A ⊆ B))
Theorem	elpw2g 1803	Membership in a power class. Theorem 86 of [Suppes] p. 47.
⊢ (B ∈ C → (A ∈ ℘B ↔ A ⊆ B))
Theorem	hbpw 1804	Bound-variable hypothesis builder for power class.
⊢ (y ∈ A → ∀x y ∈ A)    ⇒   ⊢ (y ∈ ℘A → ∀x y ∈ ℘A)
Theorem	pwid 1805	A set is a member of its power set. Theorem 87 of [Suppes] p. 47.
⊢ A ∈ V    ⇒   ⊢ A ∈ ℘A
Theorem	pwex 1806	Power set axiom expressed in class notation. Axiom 4 of [TakeutiZaring] p. 17.
⊢ A ∈ V    ⇒   ⊢ ℘A ∈ V
Theorem	pwexg 1807	Power set axiom expressed in class notation, with the sethood requirement as an antecedent. Axiom 4 of [TakeutiZaring] p. 17.
⊢ (A ∈ B → ℘A ∈ V)
Syntax	csn 1808	Extend class notation to include singleton.
class {A}
Syntax	cpr 1809	Extend class notation to include unordered pair.
class {A, B}
Syntax	cop 1810	Extend class notation to include ordered pair.
class ⟨A, B⟩
Definition	df-sn 1811	Define the singleton of a class. Definition 7.1 of [Quine] p. 48. For convenience, it is well-defined for proper classes, i.e., those that are not elements of V, although it is not very meaningful in this case. For an alternate definition see dfsn2 1819.
⊢ {A} = {x∣x = A}
Definition	df-pr 1812	Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. For a more traditional definition, but requiring a dummy variable, see dfpr2 1821.
⊢ {A, B} = ({A} ∪ {B})
Syntax	ctp 1813	Extend class notation to include unordered triplet.
class {A, B, C}
Definition	df-tp 1814	Define unordered triple of classes. Definition of [Enderton] p. 19.
⊢ {A, B, C} = ({A, B} ∪ {C})
Definition	df-op 1815	Kuratowski's ordered pair definition. Definition 9.1 of [Quine] p. 58. For proper classes it is not meaningful but is well-defined and we allow it for convenience. For the justifying theorem (for sets) see opth 1898. There are other ways to define ordered pairs; the basic requirement is that two ordered pairs are equal iff their respective members are equal. In 1914 Norbert Wiener gave the first successful definition ⟨A, B⟩1 = {{{A}, ∅}, {{B}}}, justified by opthwiener 1914, which was simplified by Kazimierz Kuratowski in 1921 to our present definition. An even simpler definition ⟨A, B⟩2 = {A, {A, B}} is justified by opthreg 3455, but it requires the Axiom of Regularity for its justification and is not commonly used. A definition that also works for proper classes is ⟨A, B⟩3 = ((A × {∅}) ∪ (B × {{∅}})), justified by opthprc 2457. If we restrict our sets to nonnegative integers, an ordered pair definition that involves only elementary arithmetic is provided by nn0opth 4724. Finally, an ordered pair of real numbers can be represented by a complex number as shown by cru 4529.
⊢ ⟨A, B⟩ = {{A}, {A, B}}
Theorem	sneq 1816	Equality theorem for singletons. Part of Exercise 4 of [TakeutiZaring] p. 15.
⊢ (A = B → {A} = {B})
Theorem	sneqi 1817	Equality inference for singletons.
⊢ A = B    ⇒   ⊢ {A} = {B}
Theorem	sneqd 1818	Equality deduction for singletons.
⊢ (φ → A = B)    ⇒   ⊢ (φ → {A} = {B})
Theorem	dfsn2 1819	Alternate definition of singleton. Definition 5.1 of [TakeutiZaring] p. 15.
⊢ {A} = {A, A}
Theorem	elsn 1820	There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15.
⊢ (x ∈ {A} ↔ x = A)
Theorem	dfpr2 1821	Alternate definition of unordered pair. Definition 5.1 of [TakeutiZaring] p. 15.
⊢ {A, B} = {x∣(x = A ∨ x = B)}
Theorem	elprg 1822	A member of an unordered pair of classes is one or the other of them. Exercise 1 of [TakeutiZaring] p. 15, generalized.
⊢ (A ∈ D → (A ∈ {B, C} ↔ (A = B ∨ A = C)))
Theorem	elpr 1823	A member of an unordered pair of classes is one or the other of them. Exercise 1 of [TakeutiZaring] p. 15.
⊢ A ∈ V    ⇒   ⊢ (A ∈ {B, C} ↔ (A = B ∨ A = C))
Theorem	hbpr 1824	Bound-variable hypothesis builder for unordered pairs.
⊢ (y ∈ A → ∀x y ∈ A)    &   ⊢ (y ∈ B → ∀x y ∈ B)    ⇒   ⊢ (y ∈ {A, B} → ∀x y ∈ {A, B})
Theorem	elsncg 1825	There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15 (generalized).
⊢ (A ∈ C → (A ∈ {B} ↔ A = B))
Theorem	elsnc 1826	There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15.
⊢ A ∈ V    ⇒   ⊢ (A ∈ {B} ↔ A = B)
Theorem	elsni 1827	There is only one element in a singleton.
⊢ (A ∈ {B} → A = B)
Theorem	snidg 1828	A set is a member of its singleton. Part of Theorem 7.6 of [Quine] p. 49.
⊢ (A ∈ B → A ∈ {A})
Theorem	snidb 1829	A class is a set iff it is a member of its singleton.
⊢ (A ∈ V ↔ A ∈ {A})
Theorem	snid 1830	A set is a member of its singleton. Part of Theorem 7.6 of [Quine] p. 49.
⊢ A ∈ V    ⇒   ⊢ A ∈ {A}
Theorem	elsnc2g 1831	There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. This variation requires only that B, rather than A, be a set.
⊢ (B ∈ C → (A ∈ {B} ↔ A = B))
Theorem	elsnc2 1832	There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. This variation requires only that B, rather than A, be a set.
⊢ B ∈ V    ⇒   ⊢ (A ∈ {B} ↔ A = B)
Theorem	hbsn 1833	Bound-variable hypothesis builder for singletons.
⊢ (y ∈ A → ∀x y ∈ A)    ⇒   ⊢ (y ∈ {A} → ∀x y ∈ {A})
Theorem	eltp 1834	A member of an unordered triple of classes is one of them. Special case of Exercise 1 of [TakeutiZaring] p. 17.
⊢ A ∈ V    ⇒   ⊢ (A ∈ {B, C, D} ↔ (A = B ∨ A = C ∨ A = D))
Theorem	dftp2 1835	Alternate definition of unordered triple of classes. Special case of Definition 5.3 of [TakeutiZaring] p. 16.
⊢ {A, B, C} = {x∣(x = A ∨ x = B ∨ x = C)}
Theorem	disjsn 1836	Intersection with singleton of non-member is disjoint.
⊢ ((A ∩ {B}) = ∅ ↔ ¬ B ∈ A)
Theorem	disjsn2 1837	Intersection of distinct singletons is disjoint.
⊢ (¬ A = B → ({A} ∩ {B}) = ∅)
Theorem	snprc 1838	The singleton of a proper class (one that doesn't exist) is the empty set. Theorem 7.2 of [Quine] p. 48.
⊢ (¬ A ∈ V ↔ {A} = ∅)
Theorem	prprc 1839	An unordered pair containing a proper class equals a singleton.
⊢ (¬ A ∈ V → {A, B} = {B})
Theorem	prcom 1840	Commutative law for unordered pairs.
⊢ {A, B} = {B, A}
Theorem	pri1 1841	One of the two elements of an unordered pair. Part of Theorem 7.6 of [Quine] p. 49.
⊢ A ∈ V    ⇒   ⊢ A ∈ {A, B}
Theorem	pri2 1842	One of the two elements of an unordered pair. Part of Theorem 7.6 of [Quine] p. 49.
⊢ B ∈ V    ⇒   ⊢ B ∈ {A, B}
Theorem	tpi1 1843	One of the three elements of an unordered triple.
⊢ A ∈ V    ⇒   ⊢ A ∈ {A, B, C}
Theorem	tpi2 1844	One of the three elements of an unordered triple.
⊢ B ∈ V    ⇒   ⊢ B ∈ {A, B, C}
Theorem	tpi3 1845	One of the three elements of an unordered triple.
⊢ C ∈ V    ⇒   ⊢ C ∈ {A, B, C}
Theorem	snnz 1846	The singleton of a set is not empty.
⊢ A ∈ V    ⇒   ⊢ ¬ {A} = ∅
Theorem	prnz 1847	A pair containing a set is not empty.
⊢ A ∈ V    ⇒   ⊢ ¬ {A, B} = ∅
Theorem	tpnz 1848	A triplet containing a set is not empty.
⊢ A ∈ V    ⇒   ⊢ ¬ {A, B, C} = ∅
Theorem	snss 1849	The singleton of an element of a class is a subset of the class. Theorem 7.4 of [Quine] p. 49.
⊢ A ∈ V    ⇒   ⊢ (A ∈ B ↔ {A} ⊆ B)
Theorem	snssg 1850	The singleton of an element of a class is a subset of the class. Theorem 7.4 of [Quine] p. 49.
⊢ (A ∈ C → (A ∈ B ↔ {A} ⊆ B))
Theorem	snssi 1851	The singleton of an element of a class is a subset of the class.
⊢ (A ∈ B → {A} ⊆ B)
Theorem	sssn 1852	The only subsets of a singleton are the singleton and the empty set.
⊢ (A ⊆ {B} ↔ (A = ∅ ∨ A = {B}))
Theorem	snsspr 1853	A singleton is a subset of an unordered pair containing its member.
⊢ {A} ⊆ {A, B}
Theorem	prss 1854	A pair of elements of a class is a subset of the class. Theorem 7.5 of [Quine] p. 49.
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ ((A ∈ C ∧ B ∈ C) ↔ {A, B} ⊆ C)
Theorem	tpss 1855	A triplet of elements of a class is a subset of the class.
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ C ∈ V    ⇒   ⊢ ((A ∈ D ∧ B ∈ D ∧ C ∈ D) ↔ {A, B, C} ⊆ D)
Theorem	sneqr 1856	If the singletons of two sets are equal, the two sets are equal. Part of Exercise 4 of [TakeutiZaring] p. 15.
⊢ A ∈ V    ⇒   ⊢ ({A} = {B} → A = B)
Theorem	snsspw 1857	The singleton of a class is a subset of its power class.
⊢ {A} ⊆ ℘A
Theorem	prsspw 1858	An unordered pair belongs to the power class of a class iff each member belongs to the class.
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ ({A, B} ⊆ ℘C ↔ (A ⊆ C ∧ B ⊆ C))
Theorem	snex 1859	A singleton is a set. Theorem 7.13 of [Quine] p. 51, but proved using only Extensionality, Power Set, and Separation.
⊢ {A} ∈ V
Theorem	el 1860	Every set is a member of some other set.
⊢ ∃y x ∈ y
Theorem	snelpw 1861	A singleton of a set belongs to the power class of a class containing the set.
⊢ A ∈ V    ⇒   ⊢ (A ∈ B ↔ {A} ∈ ℘B)
Theorem	rext 1862	A theorem similar to extensionality, requiring the existence of a singleton. Exercise 8 of [TakeutiZaring] p. 16.
⊢ (∀z(x ∈ z → y ∈ z) → x = y)
Theorem	sspwb 1863	Classes are subclasses if and only if their power classes are subclasses. Exercise 18 of [TakeutiZaring] p. 18.
⊢ (A ⊆ B ↔ ℘A ⊆ ℘B)
Theorem	ssextss 1864	An extensionality-like principle defining subclass in terms of subsets.
⊢ (A ⊆ B ↔ ∀x(x ⊆ A → x ⊆ B))
Theorem	ssext 1865	An extensionality-like principle that uses the subset instead of the membership relation: two classes are equal iff they have the same subsets.
⊢ (A = B ↔ ∀x(x ⊆ A ↔ x ⊆ B))
Theorem	nssss 1866	Negation of subclass relationship. Compare nss 1550.
⊢ (¬ A ⊆ B ↔ ∃x(x ⊆ A ∧ ¬ x ⊆ B))
Theorem	pweqb 1867	Classes are equal if and only if their power classes are equal. Exercise 19 of [TakeutiZaring] p. 18.
⊢ (A = B ↔ ℘A = ℘B)
Theorem	moabex 1868	"At most one" existence implies a class abstraction exists.
⊢ (∃*xφ → {x∣φ} ∈ V)
Theorem	euabex 1869	The abstraction of a wff with existential uniqueness exists.
⊢ (∃!xφ → {x∣φ} ∈ V)
Theorem	preq1 1870	An equality theorem for unordered pairs.
⊢ (A = B → {A, C} = {B, C})
Theorem	preq2 1871	An equality theorem for unordered pairs.
⊢ (A = B → {C, A} = {C, B})
Theorem	preqr1 1872	Reverse equality lemma for unordered pairs. If two unordered pairs have the same second element, the first elements are equal.
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ ({A, C} = {B, C} → A = B)
Theorem	prer2 1873	Reverse equality lemma for unordered pairs. If two unordered pairs have the same first element, the second elements are equal.
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ ({C, A} = {C, B} → A = B)
Theorem	preq12b 1874	Equality relationship for two unordered pairs.
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ C ∈ V    &   ⊢ D ∈ V    ⇒   ⊢ ({A, B} = {C, D} ↔ ((A = C ∧ B = D) ∨ (A = D ∧ B = C)))
Theorem	prel12 1875	Equality of two unordered pairs.
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ C ∈ V    &   ⊢ D ∈ V    ⇒   ⊢ (¬ A = B → ({A, B} = {C, D} ↔ (A ∈ {C, D} ∧ B ∈ {C, D})))
Theorem	opeq1 1876	Equality theorem for ordered pairs.
⊢ (A = B → ⟨A, C⟩ = ⟨B, C⟩)
Theorem	opeq2 1877	Equality theorem for ordered pairs.
⊢ (A = B → ⟨C, A⟩ = ⟨C, B⟩)
Theorem	opeq12 1878	Equality theorem for ordered pairs.
⊢ ((A = C ∧ B = D) → ⟨A, B⟩ = ⟨C, D⟩)
Theorem	hbop 1879	Bound-variable hypothesis builder for ordered pairs.
⊢ (y ∈ A → ∀x y ∈ A)    &   ⊢ (y ∈ B → ∀x y ∈ B)    ⇒   ⊢ (y ∈ ⟨A, B⟩ → ∀x y ∈ ⟨A, B⟩)
Theorem	nnullss 1880	A non-empty class (even if proper) has a non-empty subset.
⊢ (¬ A = ∅ → ∃x(x ⊆ A ∧ ¬ x = ∅))
Theorem	exss 1881	Restricted existence in a class (even if proper) implies restricted existence in a subset.
⊢ (∃x ∈ A φ → ∃y(y ⊆ A ∧ ∃x ∈ y φ))
Theorem	pw0 1882	Compute the power set of the empty set. Theorem 89 of [Suppes] p. 47.
⊢ ℘∅ = {∅}
Theorem	pwpw0 1883	Compute the power set of the power set of the empty set. (See pw0 1882 for the power set of the empty set.) Theorem 90 of [Suppes] p. 48.
⊢ ℘{∅} = {∅, {∅}}
Theorem	pwv 1884	The power class of the universe is the universe. Exercise 4.12(d) of [Mendelson] p. 235.
⊢ ℘V = V
Theorem	p0ex 1885	The power set of the empty set is a set.
⊢ {∅} ∈ V
Theorem	pp0ex 1886	The power set of the power set of the empty set is a set.
⊢ {∅, {∅}} ∈ V
Theorem	0nep0 1887	The empty set and its power set are not equal.
⊢ ¬ ∅ = {∅}
Theorem	0inp0 1888	Something cannot be equal to both the null set and the power set of the null set.
⊢ (A = ∅ → ¬ A = {∅})
Theorem	dtru 1889	A 'distinctor' is true in set theory. This says that at least two sets exist (or in terms of first-order logic, that the universe of discourse has two or more objects).
⊢ ¬ ∀x x = y
Theorem	dtrucor 1890	Corollary of dtru 1889. This example illustrates the danger of blindly trusting the standard Deduction Theorem without accounting for free variables: the theorem form of this deduction is not valid.
⊢ x = y    ⇒   ⊢ x ≠ y
Theorem	zfpair 1891	The Pairing axiom of Zermelo-Fraenkel set theory. Axiom 2 of [TakeutiZaring] p. 15. In some textbooks this is stated as a separate axiom; here we show it can be derived from the Extensionality, Replacement, and Power Set axioms.
⊢ {x, y} ∈ V
Theorem	prex 1892	The Axiom of Pairing using class variables. Theorem 7.13 of [Quine] p. 51. Note that an unordered pair is a set even if its components are proper classes.
⊢ {A, B} ∈ V
Theorem	opex 1893	An ordered pair of classes is a set. Exercise 7 of [TakeutiZaring] p. 16.
⊢ ⟨A, B⟩ ∈ V
Theorem	elop 1894	An ordered pair has two elements. Exercise 3 of [TakeutiZaring] p. 15.
⊢ A ∈ V    ⇒   ⊢ (A ∈ ⟨B, C⟩ ↔ (A = {B} ∨ A = {B, C}))
Theorem	opi1 1895	One of the two elements in an ordered pair.
⊢ {A} ∈ ⟨A, B⟩
Theorem	opi2 1896	One of the two elements of an ordered pair.
⊢ {A, B} ∈ ⟨A, B⟩
Theorem	opnz 1897	An ordered pair is not empty.
⊢ ¬ ⟨A, B⟩ = ∅
Theorem	opth 1898	The ordered pair theorem. If two ordered pairs are equal, their first elements are equal and their second elements are equal. Exercise 6 of [TakeutiZaring] p. 16. Note that C is not required to be a set due to a peculiarity of our specific ordered pair definition.
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ D ∈ V    ⇒   ⊢ (⟨A, B⟩ = ⟨C, D⟩ ↔ (A = C ∧ B = D))
Theorem	opthg 1899	Ordered pair theorem.
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (D ∈ R → (⟨A, B⟩ = ⟨C, D⟩ ↔ (A = C ∧ B = D)))
Theorem	otthg 1900	Ordered triple theorem.
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ R ∈ V    ⇒   ⊢ ((D ∈ F ∧ S ∈ G) → (⟨⟨A, B⟩, R⟩ = ⟨⟨C, D⟩, S⟩ ↔ (A = C ∧ B = D ∧ R = S)))