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 e. V   &   |- C e. V   =>   |- (A = <.B, C>. <-> E.xE.y(A = <.x, y>. /\ <.x, y>. = <.B, C>.))
Theorem	copsexg 1902	Substitution of class A for ordered pair <.x, y>..
|- (A = <.x, y>. -> (ph <-> E.xE.y(A = <.x, y>. /\ ph)))
Theorem	copsex2g 1903	Implicit substitution inference for ordered pairs.
|- ((x = A /\ y = B) -> (ph <-> ps))   =>   |- ((A e. C /\ B e. D) -> (E.xE.y(<.A, B>. = <.x, y>. /\ ph) <-> ps))
Theorem	copsex4g 1904	An implicit substitution inference for 2 ordered pairs.
|- (((x = A /\ y = B) /\ (z = C /\ w = D)) -> (ph <-> ps))   =>   |- (((A e. R /\ B e. S) /\ (C e. R /\ D e. S)) -> (E.xE.yE.zE.w((<.A, B>. = <.x, y>. /\ <.C, D>. = <.z, w>.) /\ ph) <-> ps))
Theorem	opprc1 1905	Expansion of an ordered pair when the first member is a proper class.
|- (-. A e. 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 e. V <-> (/) e. <.A, B>.)
Theorem	opprc2 1907	A property of an ordered pair of proper classes (due to our particular definition of ordered pair).
|- (-. B e. 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 e. V /\ -. B e. 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 e. V   &   |- D e. 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.
|- E*x A = <.B, x>.
Theorem	mosubop 1911	"At most one" remains true inside order pair quantification.
|- E*xph   =>   |- E*xE.yE.z(A = <.y, z>. /\ ph)
Theorem	euop2 1912	Transfer existential uniqueness to second member of an ordered pair.
|- (E!xE.y(x = <.A, y>. /\ ph) <-> E!yph)
Theorem	eusn 1913	Another way to express existential uniqueness of a wff: its class abstraction is a singleton.
|- (E!xph <-> E.x{x | ph} = {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 e. V   &   |- B e. 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.
|- P~(A i^i B) = (P~A i^i P~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.
|- (P~A u. P~B) (_ P~(A u. 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) <-> P~(A u. B) (_ (P~A u. P~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) <-> P~(A u. B) = (P~A u. P~B))
Syntax	cuni 1919	Extend class notation to include the union of a class (read: 'union A ')
class U.A
Definition	df-uni 1920	Define the union of a class. Definition 5.5 of [TakeutiZaring] p. 16.
|- U.A = {x | E.y(x e. y /\ y e. A)}
Theorem	dfuni2 1921	Alternate definition of class union.
|- U.A = {x | E.y e. A x e. y}
Theorem	eluni 1922	Membership in class union.
|- (A e. U.B <-> E.x(A e. x /\ x e. B))
Theorem	eluni2 1923	Membership in class union. Restricted quantifier version.
|- (A e. U.B <-> E.x e. B A e. x)
Theorem	elunii 1924	Membership in class union.
|- ((A e. B /\ B e. C) -> A e. U.C)
Theorem	hbuni 1925	Bound-variable hypothesis builder for union.
|- (y e. A -> A.x y e. A)   =>   |- (y e. U.A -> A.x y e. U.A)
Theorem	eluniab 1926	Membership in union of a class abstract.
|- (A e. U.{x | ph} <-> E.x(A e. x /\ ph))
Theorem	unieq 1927	Equality theorem for class union. Exercise 15 of [TakeutiZaring] p. 18.
|- (A = B -> U.A = U.B)
Theorem	unieqi 1928	Inference of equality of two class unions.
|- A = B   =>   |- U.A = U.B
Theorem	unieqd 1929	Deduction of equality of two class unions.
|- (ph -> A = B)   =>   |- (ph -> U.A = U.B)
Theorem	unpr 1930	The union of a pair is the union of its members. Proposition 5.7 of [TakeutiZaring] p. 16.
|- A e. V   &   |- B e. V   =>   |- U.{A, B} = (A u. B)
Theorem	unop 1931	The union of an ordered pair. Theorem 65 of [Suppes] p. 39.
|- U.<.A, B>. = {A, B}
Theorem	unisn 1932	A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53.
|- A e. V   =>   |- U.{A} = A
Theorem	unisng 1933	A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53.
|- (A e. B -> U.{A} = A)
Theorem	uniun 1934	The class union of the union of two classes. Theorem 8.3 of [Quine] p. 53.
|- U.(A u. B) = (U.A u. U.B)
Theorem	uniin 1935	The class union of the intersection of two classes. Exercise 4.12(n) of [Mendelson] p. 235.
|- U.(A i^i B) (_ (U.A i^i U.B)
Theorem	uniss 1936	Subclass relationship for class union. Theorem 61 of [Suppes] p. 39.
|- (A (_ B -> U.A (_ U.B)
Theorem	ssuni 1937	Subclass relationship for class union.
|- ((A (_ B /\ B e. C) -> A (_ U.C)
Theorem	uni0 1938	The union of the empty set is the empty set. Theorem 8.7 of [Quine] p. 54.
|- U.(/) = (/)
Theorem	uni0b 1939	The union of a set is empty iff the set is included in the singleton of the empty set.
|- (U.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 e. B -> A (_ U.B)
Theorem	unissb 1941	Relationship involving membership, subset, and union. Exercise 5 of [Enderton] p. 26 and its converse.
|- (U.A (_ B <-> A.x e. 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.
|- (A.x e. A E.y e. B x (_ y -> U.A (_ U.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.
|- (A.x e. A E.y e. (A \ B)x (_ y -> U.(A \ B) = U.A)
Theorem	unidif0 1944	The removal of the empty set from a class does not affect its union.
|- U.(A \ {(/)}) = U.A
Theorem	ssunieq 1945	Relationship implying union.
|- ((A e. B /\ A.x e. B x (_ A) -> A = U.B)
Theorem	unisseq 1946	A set is a union of its subsets.
|- (A e. B -> A = U.{x e. 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 e. V, then the union of A is also a set. Same as Axiom 3 of [TakeutiZaring] p. 16.
|- A e. V   =>   |- U.A e. 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 e. B instead of A e. V to make the theorem more general and thus shorten some proofs; obviously V is one possibility for B.
|- (A e. B -> U.A e. V)
Theorem	unex 1949	The union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16.
|- A e. V   &   |- B e. V   =>   |- (A u. B) e. V
Theorem	unexb 1950	Existence of union is equivalent to existence of its components.
|- ((A e. V /\ B e. V) <-> (A u. B) e. V)
Theorem	difex2 1951	If the subtrahend of a class difference exists, then the minuend exists iff the difference exists.
|- (B e. C -> (A e. V <-> (A \ B) e. V))
Theorem	tpex 1952	A triple of classes exists.
|- {A, B, C} e. 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>. e. A -> (x e. U.U.A /\ y e. U.U.A))
Theorem	euuni 1954	If ph is true for exactly one x, then U.{x | ph} 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'.
|- (E!xph -> (ph <-> U.{x | ph} = x))
Theorem	reuuni1 1955	A way to express 'the unique element such that' (restricted quantifier version).
|- ((x e. A /\ E!x e. A ph) -> (ph <-> U.{x e. A | ph} = x))
Theorem	reuuni2 1956	U.{x e. A | ph} is the explicit representation of 'the unique element in A such that ph.'
|- (x = B -> (ph <-> ps))   =>   |- ((B e. A /\ E!x e. A ph) -> (ps <-> U.{x e. A | ph} = B))
Theorem	reucl 1957	Closure law for 'the unique element in A such that ph.'
|- (E!x e. A ph -> U.{x e. A | ph} e. A)
Theorem	reuuni3 1958	Derive the property ch of 'the unique element in A such that ph ' when expressed explicitly as U.{y e. A | ps}.
|- (x = y -> (ph <-> ps))   &   |- (x = U.{y e. A | ps} -> (ph <-> ch))   =>   |- (E!x e. A ph -> ch)
Theorem	reuuni4 1959	Derive the property of 'the unique element in A such that ph ' when expressed explicitly as U.{x e. A | ph}.
|- (E!x e. A ph -> [U.{x e. A | ph} / x]ph)
Theorem	unipw 1960	A class equals the union of its power class. Exercise 6(a) of [Enderton] p. 38.
|- U.P~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 (_ P~U.A
Theorem	uniexb 1962	The Axiom of Union and its converse. A class is a set iff its union is a set.
|- (A e. V <-> U.A e. 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 e. V <-> P~A e. V)
Theorem	univ 1964	The union of the universe is the universe. Exercise 4.12(c) of [Mendelson] p. 235.
|- U.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 | A.y(y e. A -> x e. y)}
Theorem	dfint2 1967	Alternate definition of class intersection.
|- |^|A = {x | A.y e. A x e. 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.
|- (ph -> A = B)   =>   |- (ph -> |^|A = |^|B)
Theorem	elint 1971	Membership in class intersection.
|- A e. V   =>   |- (A e. |^|B <-> A.x(x e. B -> A e. x))
Theorem	elint2 1972	Membership in class intersection.
|- A e. V   =>   |- (A e. |^|B <-> A.x e. B A e. x)
Theorem	elintg 1973	Membership in class intersection, with the sethood requirement expressed as an antecedent.
|- (A e. C -> (A e. |^|B <-> A.x e. B A e. x))
Theorem	elinti 1974	Membership in class intersection.
|- (A e.