Metamath Proof Explorer - mmtheorems20

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 - 1901-2000 - Page 20 of 58

Type	Label	Description
Statement
Theorem	eqvinop 1901	A variable introduction law for ordered pairs. Analogue of Lemma 15 of [Monk2] p. 109.
⊢ B ∈ V    &   ⊢ C ∈ V    ⇒   ⊢ (A = ⟨B, C⟩ ↔ ∃x∃y(A = ⟨x, y⟩ ∧ ⟨x, y⟩ = ⟨B, C⟩))
Theorem	copsexg 1902	Substitution of class A for ordered pair ⟨x, y⟩.
⊢ (A = ⟨x, y⟩ → (φ ↔ ∃x∃y(A = ⟨x, y⟩ ∧ φ)))
Theorem	copsex2g 1903	Implicit substitution inference for ordered pairs.
⊢ ((x = A ∧ y = B) → (φ ↔ ψ))    ⇒   ⊢ ((A ∈ C ∧ B ∈ D) → (∃x∃y(⟨A, B⟩ = ⟨x, y⟩ ∧ φ) ↔ ψ))
Theorem	copsex4g 1904	An implicit substitution inference for 2 ordered pairs.
⊢ (((x = A ∧ y = B) ∧ (z = C ∧ w = D)) → (φ ↔ ψ))    ⇒   ⊢ (((A ∈ R ∧ B ∈ S) ∧ (C ∈ R ∧ D ∈ S)) → (∃x∃y∃z∃w((⟨A, B⟩ = ⟨x, y⟩ ∧ ⟨C, D⟩ = ⟨z, w⟩) ∧ φ) ↔ ψ))
Theorem	opprc1 1905	Expansion of an ordered pair when the first member is a proper class.
⊢ (¬ A ∈ V → ⟨A, B⟩ = {∅, {B}})
Theorem	opprc1b 1906	A property of an ordered pair of proper classes (due to our particular definition of ordered pair).
⊢ (¬ A ∈ V ↔ ∅ ∈ ⟨A, B⟩)
Theorem	opprc2 1907	A property of an ordered pair of proper classes (due to our particular definition of ordered pair).
⊢ (¬ B ∈ V → ⟨A, B⟩ = ⟨A, A⟩)
Theorem	opprc3 1908	A property of an ordered pair of proper classes (due to our particular definition of ordered pair).
⊢ ((¬ A ∈ V ∧ ¬ B ∈ V) ↔ ⟨A, B⟩ = {∅})
Theorem	opth2 1909	Equality of the second members of equal ordered pairs. Because of our particular ordered pair definition, equality holds whether or not the first members are sets.
⊢ B ∈ V    &   ⊢ D ∈ V    ⇒   ⊢ (⟨A, B⟩ = ⟨C, D⟩ → B = D)
Theorem	moop2 1910	"At most one" property of an ordered pair. The proof is a little tricky because we do not place any restrictions on class B.
⊢ ∃*x A = ⟨B, x⟩
Theorem	mosubop 1911	"At most one" remains true inside order pair quantification.
⊢ ∃*xφ    ⇒   ⊢ ∃*x∃y∃z(A = ⟨y, z⟩ ∧ φ)
Theorem	euop2 1912	Transfer existential uniqueness to second member of an ordered pair.
⊢ (∃!x∃y(x = ⟨A, y⟩ ∧ φ) ↔ ∃!yφ)
Theorem	eusn 1913	Another way to express existential uniqueness of a wff: its class abstraction is a singleton.
⊢ (∃!xφ ↔ ∃x{x∣φ} = {x})
Theorem	opthwiener 1914	Justification theorem for the ordered pair definition in Norbert Wiener, "A simplification of the logic of relations," Proc. of the Cambridge Philos. Soc., 1914, vol. 17, pp.387-390. It is also shown as a definition in [Enderton] p. 36 and as Exercise 4.8(b) of [Mendelson] p. 230. It is meaningful only for classes that exist as sets (i.e. are not proper classes). See df-op 1815 for other ordered pair definitions.
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ ({{{A}, ∅}, {{B}}} = {{{C}, ∅}, {{D}}} ↔ (A = C ∧ B = D))
Theorem	pwin 1915	The power class of the intersection of two classes is the intersection of their power classes. Exercise 4.12(j) of [Mendelson] p. 235.
⊢ ℘(A ∩ B) = (℘A ∩ ℘B)
Theorem	pwunss 1916	The power class of the union of two classes includes the union of their power classes. Exercise 4.12(k) of [Mendelson] p. 235.
⊢ (℘A ∪ ℘B) ⊆ ℘(A ∪ B)
Theorem	pwssun 1917	The power class of the union of two classes is a subset of the union of their power classes, iff one class is a subclass of the other. Exercise 4.12(l) of [Mendelson] p. 235.
⊢ ((A ⊆ B ∨ B ⊆ A) ↔ ℘(A ∪ B) ⊆ (℘A ∪ ℘B))
Theorem	pwun 1918	The power class of the union of two classes equals the union of their power classes, iff one class is a subclass of the other. Part of Exercise 7(b) of [Enderton] p. 28.
⊢ ((A ⊆ B ∨ B ⊆ A) ↔ ℘(A ∪ B) = (℘A ∪ ℘B))
Syntax	cuni 1919	Extend class notation to include the union of a class (read: 'union A ')
class ∪A
Definition	df-uni 1920	Define the union of a class. Definition 5.5 of [TakeutiZaring] p. 16.
⊢ ∪A = {x∣∃y(x ∈ y ∧ y ∈ A)}
Theorem	dfuni2 1921	Alternate definition of class union.
⊢ ∪A = {x∣∃y ∈ A x ∈ y}
Theorem	eluni 1922	Membership in class union.
⊢ (A ∈ ∪B ↔ ∃x(A ∈ x ∧ x ∈ B))
Theorem	eluni2 1923	Membership in class union. Restricted quantifier version.
⊢ (A ∈ ∪B ↔ ∃x ∈ B A ∈ x)
Theorem	elunii 1924	Membership in class union.
⊢ ((A ∈ B ∧ B ∈ C) → A ∈ ∪C)
Theorem	hbuni 1925	Bound-variable hypothesis builder for union.
⊢ (y ∈ A → ∀x y ∈ A)    ⇒   ⊢ (y ∈ ∪A → ∀x y ∈ ∪A)
Theorem	eluniab 1926	Membership in union of a class abstract.
⊢ (A ∈ ∪{x∣φ} ↔ ∃x(A ∈ x ∧ φ))
Theorem	unieq 1927	Equality theorem for class union. Exercise 15 of [TakeutiZaring] p. 18.
⊢ (A = B → ∪A = ∪B)
Theorem	unieqi 1928	Inference of equality of two class unions.
⊢ A = B    ⇒   ⊢ ∪A = ∪B
Theorem	unieqd 1929	Deduction of equality of two class unions.
⊢ (φ → A = B)    ⇒   ⊢ (φ → ∪A = ∪B)
Theorem	unpr 1930	The union of a pair is the union of its members. Proposition 5.7 of [TakeutiZaring] p. 16.
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ ∪{A, B} = (A ∪ B)
Theorem	unop 1931	The union of an ordered pair. Theorem 65 of [Suppes] p. 39.
⊢ ∪⟨A, B⟩ = {A, B}
Theorem	unisn 1932	A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53.
⊢ A ∈ V    ⇒   ⊢ ∪{A} = A
Theorem	unisng 1933	A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53.
⊢ (A ∈ B → ∪{A} = A)
Theorem	uniun 1934	The class union of the union of two classes. Theorem 8.3 of [Quine] p. 53.
⊢ ∪(A ∪ B) = (∪A ∪ ∪B)
Theorem	uniin 1935	The class union of the intersection of two classes. Exercise 4.12(n) of [Mendelson] p. 235.
⊢ ∪(A ∩ B) ⊆ (∪A ∩ ∪B)
Theorem	uniss 1936	Subclass relationship for class union. Theorem 61 of [Suppes] p. 39.
⊢ (A ⊆ B → ∪A ⊆ ∪B)
Theorem	ssuni 1937	Subclass relationship for class union.
⊢ ((A ⊆ B ∧ B ∈ C) → A ⊆ ∪C)
Theorem	uni0 1938	The union of the empty set is the empty set. Theorem 8.7 of [Quine] p. 54.
⊢ ∪∅ = ∅
Theorem	uni0b 1939	The union of a set is empty iff the set is included in the singleton of the empty set.
⊢ (∪A = ∅ ↔ A ⊆ {∅})
Theorem	elssuni 1940	An element of a class is a subclass of its union. Theorem 8.6 of [Quine] p. 54. Also the basis for Proposition 7.20 of [TakeutiZaring] p. 40.
⊢ (A ∈ B → A ⊆ ∪B)
Theorem	unissb 1941	Relationship involving membership, subset, and union. Exercise 5 of [Enderton] p. 26 and its converse.
⊢ (∪A ⊆ B ↔ ∀x ∈ A x ⊆ B)
Theorem	uniss2 1942	A subclass condition on the members of two classes that implies a subclass relation on their unions. Proposition 8.6 of [TakeutiZaring] p. 59. See iunss2 2021 for a generalization to indexed unions.
⊢ (∀x ∈ A ∃y ∈ B x ⊆ y → ∪A ⊆ ∪B)
Theorem	unidif 1943	If the difference A ∖ B contains the largest members of A, then the union of the difference is the union of A.
⊢ (∀x ∈ A ∃y ∈ (A ∖ B)x ⊆ y → ∪(A ∖ B) = ∪A)
Theorem	unidif0 1944	The removal of the empty set from a class does not affect its union.
⊢ ∪(A ∖ {∅}) = ∪A
Theorem	ssunieq 1945	Relationship implying union.
⊢ ((A ∈ B ∧ ∀x ∈ B x ⊆ A) → A = ∪B)
Theorem	unisseq 1946	A set is a union of its subsets.
⊢ (A ∈ B → A = ∪{x ∈ B∣x ⊆ A})
Theorem	uniex 1947	The ZF Axiom of Union in class notation. This says that if A is a set i.e. A ∈ V, then the union of A is also a set. Same as Axiom 3 of [TakeutiZaring] p. 16.
⊢ A ∈ V    ⇒   ⊢ ∪A ∈ V
Theorem	uniexg 1948	The ZF Axiom of Union in class notation, in the form of a theorem instead of an inference. We use the antecedent A ∈ B instead of A ∈ V to make the theorem more general and thus shorten some proofs; obviously V is one possibility for B.
⊢ (A ∈ B → ∪A ∈ V)
Theorem	unex 1949	The union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16.
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (A ∪ B) ∈ V
Theorem	unexb 1950	Existence of union is equivalent to existence of its components.
⊢ ((A ∈ V ∧ B ∈ V) ↔ (A ∪ B) ∈ V)
Theorem	difex2 1951	If the subtrahend of a class difference exists, then the minuend exists iff the difference exists.
⊢ (B ∈ C → (A ∈ V ↔ (A ∖ B) ∈ V))
Theorem	tpex 1952	A triple of classes exists.
⊢ {A, B, C} ∈ V
Theorem	opeluu 1953	Each member of an ordered pair belongs to the union of the union of a class to which the ordered pair belongs. Lemma 3D of [Enderton] p. 41.
⊢ (⟨x, y⟩ ∈ A → (x ∈ ∪∪A ∧ y ∈ ∪∪A))
Theorem	euuni 1954	If φ is true for exactly one x, then ∪{x∣φ} is a way to express 'the unique element such that'. Some books use a special symbol such as iota to denote 'the unique element such that'.
⊢ (∃!xφ → (φ ↔ ∪{x∣φ} = x))
Theorem	reuuni1 1955	A way to express 'the unique element such that' (restricted quantifier version).
⊢ ((x ∈ A ∧ ∃!x ∈ A φ) → (φ ↔ ∪{x ∈ A∣φ} = x))
Theorem	reuuni2 1956	∪{x ∈ A∣φ} is the explicit representation of 'the unique element in A such that φ.'
⊢ (x = B → (φ ↔ ψ))    ⇒   ⊢ ((B ∈ A ∧ ∃!x ∈ A φ) → (ψ ↔ ∪{x ∈ A∣φ} = B))
Theorem	reucl 1957	Closure law for 'the unique element in A such that φ.'
⊢ (∃!x ∈ A φ → ∪{x ∈ A∣φ} ∈ A)
Theorem	reuuni3 1958	Derive the property χ of 'the unique element in A such that φ ' when expressed explicitly as ∪{y ∈ A∣ψ}.
⊢ (x = y → (φ ↔ ψ))    &   ⊢ (x = ∪{y ∈ A∣ψ} → (φ ↔ χ))    ⇒   ⊢ (∃!x ∈ A φ → χ)
Theorem	reuuni4 1959	Derive the property of 'the unique element in A such that φ ' when expressed explicitly as ∪{x ∈ A∣φ}.
⊢ (∃!x ∈ A φ → [∪{x ∈ A∣φ} / x]φ)
Theorem	unipw 1960	A class equals the union of its power class. Exercise 6(a) of [Enderton] p. 38.
⊢ ∪℘A = A
Theorem	pwuni 1961	A class is a subclass of the power class of its union. Exercise 6(b) of [Enderton] p. 38.
⊢ A ⊆ ℘∪A
Theorem	uniexb 1962	The Axiom of Union and its converse. A class is a set iff its union is a set.
⊢ (A ∈ V ↔ ∪A ∈ V)
Theorem	pwexb 1963	The Axiom of Power Sets and its converse. A class is a set iff its power class is a set.
⊢ (A ∈ V ↔ ℘A ∈ V)
Theorem	univ 1964	The union of the universe is the universe. Exercise 4.12(c) of [Mendelson] p. 235.
⊢ ∪V = V
Syntax	cint 1965	Extend class notation to include the intersection of a class (read: 'intersect A ').
class ∩A
Definition	df-int 1966	Define the intersection of a class. Definition 7.35 of [TakeutiZaring] p. 44.
⊢ ∩A = {x∣∀y(y ∈ A → x ∈ y)}
Theorem	dfint2 1967	Alternate definition of class intersection.
⊢ ∩A = {x∣∀y ∈ A x ∈ y}
Theorem	inteq 1968	Equality law for intersection.
⊢ (A = B → ∩A = ∩B)
Theorem	inteqi 1969	Equality inference for class intersection.
⊢ A = B    ⇒   ⊢ ∩A = ∩B
Theorem	inteqd 1970	Equality deduction for class intersection.
⊢ (φ → A = B)    ⇒   ⊢ (φ → ∩A = ∩B)
Theorem	elint 1971	Membership in class intersection.
⊢ A ∈ V    ⇒   ⊢ (A ∈ ∩B ↔ ∀x(x ∈ B → A ∈ x))
Theorem	elint2 1972	Membership in class intersection.
⊢ A ∈ V    ⇒   ⊢ (A ∈ ∩B ↔ ∀x ∈ B A ∈ x)
Theorem	elintg 1973	Membership in class intersection, with the sethood requirement expressed as an antecedent.
⊢ (A ∈ C → (A ∈ ∩B ↔ ∀x ∈ B A ∈ x))
Theorem	elinti 1974	Membership in class intersection.
⊢ (A ∈ ∩B → (C ∈ B → A ∈ C))
Theorem	hbint 1975	Bound-variable hypothesis builder for intersection.
⊢ (y ∈ A → ∀x y ∈ A)    ⇒   ⊢ (y ∈ ∩A → ∀x y ∈ ∩A)
Theorem	elintab 1976	Membership in the intersection of a class abstraction.
⊢ A ∈ V    ⇒   ⊢ (A ∈ ∩{x∣φ} ↔ ∀x(φ → A ∈ x))
Theorem	elintrab 1977	Membership in the intersection of a class abstraction.
⊢ A ∈ V    ⇒   ⊢ (A ∈ ∩{x ∈ B∣φ} ↔ ∀x ∈ B (φ → A ∈ x))
Theorem	int0 1978	The intersection of the empty set is the universal class. Exercise 2 of [TakeutiZaring] p. 44.
⊢ ∩∅ = V
Theorem	intss1 1979	An element of a class includes the intersection of the class. Exercise 4 of [TakeutiZaring] p. 44 (with correction), generalized to classes.
⊢ (A ∈ B → ∩B ⊆ A)
Theorem	ssint 1980	Subclass of a class intersection. Theorem 5.11(viii) of [Monk1] p. 52 and its converse.
⊢ (A ⊆ ∩B ↔ ∀x ∈ B A ⊆ x)
Theorem	ssintub 1981	Subclass of a least upper bound.
⊢ A ⊆ ∩{x ∈ B∣A ⊆ x}
Theorem	intmin 1982	Any member of a class is the smallest of those members that include it.
⊢ (A ∈ B → A = ∩{x ∈ B∣A ⊆ x})
Theorem	intss 1983	Intersection of subclasses.
⊢ (A ⊆ B → ∩B ⊆ ∩A)
Theorem	intmin2 1984	Any set is the smallest of all sets that include it.
⊢ A ∈ V    ⇒   ⊢ A = ∩{x∣A ⊆ x}
Theorem	int0el 1985	The intersection of a class containing the empty set is empty.
⊢ (∅ ∈ A → ∩A = ∅)
Theorem	intex 1986	The intersection of a non-empty class exists. Exercise 5 of [TakeutiZaring] p. 44 and its converse.
⊢ (¬ A = ∅ ↔ ∩A ∈ V)
Theorem	intexab 1987	The intersection of a non-empty class abstraction exists.
⊢ (∃xφ ↔ ∩{x∣φ} ∈ V)
Theorem	intexrab 1988	The intersection of a non-empty restricted class abstraction exists.
⊢ (∃x ∈ A φ ↔ ∩{x ∈ A∣φ} ∈ V)
Theorem	intun 1989	The class intersection of the union of two classes. Theorem 78 of [Suppes] p. 42.
⊢ ∩(A ∪ B) = (∩A ∩ ∩B)
Theorem	intpr 1990	The intersection of a pair is the intersection of its members. Theorem 71 of [Suppes] p. 42.
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ ∩{A, B} = (A ∩ B)
Theorem	intsn 1991	The intersection of a singleton is its member. Theorem 70 of [Suppes] p. 41.
⊢ A ∈ V    ⇒   ⊢ ∩{A} = A
Theorem	op1stb 1992	Extract the first member of an ordered pair. Theorem 73 of [Suppes] p. 42. (See op2ndb 2638 to extract the second member and op1sta 2635 for an alternate version.)
⊢ A ∈ V    ⇒   ⊢ ∩∩⟨A, B⟩ = A
Theorem	intunsn 1993	Theorem joining a singleton to an intersection.
⊢ B ∈ V    ⇒   ⊢ ∩(A ∪ {B}) = (∩A ∩ B)
Syntax	ciun 1994	Extend class notation to include indexed union.
class ∪x ∈ A B
Syntax	ciin 1995	Extend class notation to include indexed intersection.
class ∩x ∈ A B
Definition	df-iun 1996	Define indexed union. Ordinarily, A would be independent of x and B would depend on x. In this case x is called an index, A is called an index set, and B is called an indexed set. In most books, x ∈ A is written as a subscript or underneath the ∪. Definition of [Stoll] p. 45.
⊢ ∪x ∈ A B = {y∣∃x ∈ A y ∈ B}
Definition	df-iin 1997	Define indexed intersection. Definition of [Stoll] p. 45. See the remarks for its sibling operation of indexed union df-iun 1996.
⊢ ∩x ∈ A B = {y∣∀x ∈ A y ∈ B}
Theorem	eliun 1998	Membership in indexed union.
⊢ (A ∈ ∪x ∈ B C ↔ ∃x ∈ B A ∈ C)
Theorem	eliin 1999	Membership in indexed intersection.
⊢ (A ∈ D → (A ∈ ∩x ∈ B C ↔ ∀x ∈ B A ∈ C))
Theorem	iunconst 2000	Indexed union of a constant class, i.e. where B does not depend on x.
⊢ (¬ A = ∅ → ∪x ∈ A B = B)