mmtheorems24 - Metamath Proof Explorer

Jump to page: Contents + 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-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12229

Statement List for Metamath Proof Explorer - 2301-2400 - Page 24 of 123

Type	Label	Description
Statement
Theorem	invdif 2301	Intersection with universal complement. Remark in [Stoll] p. 20.
|- (A i^i (V \ B)) = (A \ B)
Theorem	indif 2302	Intersection with class difference. Theorem 34 of [Suppes] p. 29.
|- (A i^i (A \ B)) = (A \ B)
Theorem	indi 2303	Distributive law for intersection over union. Exercise 10 of [TakeutiZaring] p. 17.
|- (A i^i (B u. C)) = ((A i^i B) u. (A i^i C))
Theorem	undi 2304	Distributive law for union over intersection. Exercise 11 of [TakeutiZaring] p. 17.
|- (A u. (B i^i C)) = ((A u. B) i^i (A u. C))
Theorem	indir 2305	Distributive law for intersection over union. Theorem 28 of [Suppes] p. 27.
|- ((A u. B) i^i C) = ((A i^i C) u. (B i^i C))
Theorem	undir 2306	Distributive law for union over intersection. Theorem 29 of [Suppes] p. 27.
|- ((A i^i B) u. C) = ((A u. C) i^i (B u. C))
Theorem	unineq 2307	Infer equality from equalities of union and intersection. Exercise 20 of [Enderton] p. 32 and its converse.
|- (((A u. C) = (B u. C) /\ (A i^i C) = (B i^i C)) <-> A = B)
Theorem	uneqin 2308	Equality of union and intersection implies equality of their arguments.
|- ((A u. B) = (A i^i B) <-> A = B)
Theorem	difundi 2309	Distributive law for class difference. Theorem 39 of [Suppes] p. 29.
|- (A \ (B u. C)) = ((A \ B) i^i (A \ C))
Theorem	difundir 2310	Distributive law for class difference.
|- ((A u. B) \ C) = ((A \ C) u. (B \ C))
Theorem	difindi 2311	Distributive law for class difference. Theorem 40 of [Suppes] p. 29.
|- (A \ (B i^i C)) = ((A \ B) u. (A \ C))
Theorem	difindir 2312	Distributive law for class difference.
|- ((A i^i B) \ C) = ((A \ C) i^i (B \ C))
Theorem	undm 2313	DeMorgan's law for union. Theorem 5.2(13) of [Stoll] p. 19.
|- (V \ (A u. B)) = ((V \ A) i^i (V \ B))
Theorem	indm 2314	DeMorgan's law for intersection. Theorem 5.2(13') of [Stoll] p. 19.
|- (V \ (A i^i B)) = ((V \ A) u. (V \ B))
Theorem	difun1 2315	A relationship involving double difference and union.
|- (A \ (B u. C)) = ((A \ B) \ C)
Theorem	dif23 2316	Swap second and third argument of double difference.
|- ((A \ B) \ C) = ((A \ C) \ B)
Theorem	symdif1 2317	Two ways to express symmetric difference. This theorem shows the equivalence of the definition of symmetric difference in [Stoll] p. 13 and the restated definition in Example 4.1 of [Stoll] p. 262.
|- ((A \ B) u. (B \ A)) = ((A u. B) \ (A i^i B))
Theorem	symdif2 2318	Two ways to express symmetric difference.
|- ((A \ B) u. (B \ A)) = {x | -. (x e. A <-> x e. B)}
Theorem	unab 2319	Union of two class abstractions.
|- ({x | ph} u. {x | ps}) = {x | (ph \/ ps)}
Theorem	inab 2320	Intersection of two class abstractions.
|- ({x | ph} i^i {x | ps}) = {x | (ph /\ ps)}
Theorem	difab 2321	Difference of two class abstractions.
|- ({x | ph} \ {x | ps}) = {x | (ph /\ -. ps)}
Theorem	unrab 2322	Union of two restricted class abstractions.
|- ({x e. A | ph} u. {x e. A | ps}) = {x e. A | (ph \/ ps)}
Theorem	inrab 2323	Intersection of two restricted class abstractions.
|- ({x e. A | ph} i^i {x e. A | ps}) = {x e. A | (ph /\ ps)}
Theorem	inrab2 2324	Intersection with a restricted class abstraction.
|- ({x e. A | ph} i^i B) = {x e. (A i^i B) | ph}
Theorem	difrab 2325	Difference of two restricted class abstractions.
|- ({x e. A | ph} \ {x e. A | ps}) = {x e. A | (ph /\ -. ps)}
Theorem	dfrab2 2326	Alternate definition of restricted class abstraction.
|- {x e. A | ph} = ({x | ph} i^i A)
Theorem	reuss2 2327	Transfer uniqueness to a smaller subclass.
|- (((A (_ B /\ A.x e. A (ph -> ps)) /\ (E.x e. A ph /\ E!x e. B ps)) -> E!x e. A ph)
Theorem	reuss 2328	Transfer uniqueness to a smaller subclass.
|- ((A (_ B /\ E.x e. A ph /\ E!x e. B ph) -> E!x e. A ph)
Theorem	reuun1 2329	Transfer uniqueness to a smaller class.
|- ((E.x e. A ph /\ E!x e. (A u. B)(ph \/ ps)) -> E!x e. A ph)
Theorem	reuun2 2330	Transfer uniqueness to a smaller or larger class.
|- (-. E.x e. B ph -> (E!x e. (A u. B)ph <-> E!x e. A ph))
Theorem	reupick 2331	Restricted uniqueness "picks" a member of a subclass.
|- (((A (_ B /\ (E.x e. A ph /\ E!x e. B ph)) /\ ph) -> (x e. A <-> x e. B))
The empty set
Syntax	c0 2332	Extend class notation to include the empty set.
class (/)
Definition	df-nul 2333	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 2334.
|- (/) = (V \ V)
Theorem	dfnul2 2334	Alternate definition of the empty set. Definition 5.14 of [TakeutiZaring] p. 20.
|- (/) = {x | -. x = x}
Theorem	dfnul3 2335	Alternate definition of the empty set..
|- (/) = {x e. A | -. x e. A}
Theorem	noel 2336	The empty set has no elements. Theorem 6.14 of [Quine] p. 44.
|- -. A e. (/)
Theorem	n0i 2337	If a set has elements, it is not empty.
|- (B e. A -> -. A = (/))
Theorem	ne0i 2338	If a set has elements, it is not empty.
|- (B e. A -> A =/= (/))
Theorem	vn0 2339	The universal class is not equal to the empty set.
|- V =/= (/)
Theorem	ne0f 2340	A nonempty class has at least one element. Proposition 5.17(1) of [TakeutiZaring] p. 20. This version of n0 2341 requires only that x not be free in, rather than not occur in, A.
|- (y e. A -> A.x y e. A)   =>   |- (A =/= (/) <-> E.x x e. A)
Theorem	n0 2341	A nonempty class has at least one element. Proposition 5.17(1) of [TakeutiZaring] p. 20.
|- (A =/= (/) <-> E.x x e. A)
Theorem	neq0 2342	A nonempty class has at least one element. Proposition 5.17(1) of [TakeutiZaring] p. 20.
|- (-. A = (/) <-> E.x x e. A)
Theorem	abn0 2343	Nonempty class abstraction.
|- ({x | ph} =/= (/) <-> E.xph)
Theorem	rex0 2344	Vacuous existential quantification is false.
|- -. E.x e. (/) ph
Theorem	rabn0 2345	Non-empty restricted class abstraction.
|- ({x e. A | ph} =/= (/) <-> E.x e. A ph)
Theorem	rab0 2346	Any restricted class abstraction restricted to the empty set is empty.
|- {x e. (/) | ph} = (/)
Theorem	eq0 2347	The empty set has no elements. Theorem 2 of [Suppes] p. 22.
|- (A = (/) <-> A.x -. x e. A)
Theorem	eqv 2348	The universe contains every set.
|- (A = V <-> A.x x e. A)
Theorem	0el 2349	Membership of the empty set in another class.
|- ((/) e. A <-> E.x e. A A.y -. y e. x)
Theorem	un0 2350	The union of a class with the empty set is itself. Theorem 24 of [Suppes] p. 27.
|- (A u. (/)) = A
Theorem	in0 2351	The intersection of a class with the empty set is the empty set. Theorem 16 of [Suppes] p. 26.
|- (A i^i (/)) = (/)
Theorem	inv1 2352	The intersection of a class with the universal class is itself. Exercise 4.10(k) of [Mendelson] p. 231.
|- (A i^i V) = A
Theorem	unv 2353	The union of a class with the universal class is the universal class. Exercise 4.10(l) of [Mendelson] p. 231.
|- (A u. V) = V
Theorem	0ss 2354	The null set is a subset of any class. Part of Exercise 1 of [TakeutiZaring] p. 22.
|- (/) (_ A
Theorem	ss0b 2355	Any subset of the empty set is empty. Theorem 5 of [Suppes] p. 23 and its converse.
|- (A (_ (/) <-> A = (/))
Theorem	ss0 2356	Any subset of the empty set is empty. Theorem 5 of [Suppes] p. 23.
|- (A (_ (/) -> A = (/))
Theorem	sseq0 2357	A subclass of an empty class is empty.
|- ((A (_ B /\ B = (/)) -> A = (/))
Theorem	ssn0 2358	A class with a nonempty subclass is nonempty.
|- ((A (_ B /\ A =/= (/)) -> B =/= (/))
Theorem	un00 2359	Two classes are empty iff their union is empty.
|- ((A = (/) /\ B = (/)) <-> (A u. B) = (/))
Theorem	vss 2360	Only the universal class has the universal class as a subclass.
|- (V (_ A <-> A = V)
Theorem	0pss 2361	The null set is a proper subset of any non-empty set.
|- ((/) (. A <-> A =/= (/))
Theorem	npss0 2362	No set is a proper subset of the empty set.
|- -. A (. (/)
Theorem	pssv 2363	Any non-universal class is a proper subclass of the universal class.
|- (A (. V <-> -. A = V)
Theorem	disj 2364	Two ways of saying that two classes are disjoint (have no members in common).
|- ((A i^i B) = (/) <-> A.x e. A -. x e. B)
Theorem	disj1 2365	Two ways of saying that two classes are disjoint (have no members in common).
|- ((A i^i B) = (/) <-> A.x(x e. A -> -. x e. B))
Theorem	reldisj 2366	Two ways of saying that two classes are disjoint, using the complement of B relative to a universe C.
|- (A (_ C -> ((A i^i B) = (/) <-> A (_ (C \ B)))
Theorem	disj3 2367	Two ways of saying that two classes are disjoint.
|- ((A i^i B) = (/) <-> A = (A \ B))
Theorem	disjne 2368	Members of disjoint sets are not equal.
|- (((A i^i B) = (/) /\ C e. A /\ D e. B) -> C =/= D)
Theorem	disj2 2369	Two ways of saying that two classes are disjoint.
|- ((A i^i B) = (/) <-> A (_ (V \ B))
Theorem	disj4 2370	Two ways of saying that two classes are disjoint.
|- ((A i^i B) = (/) <-> -. (A \ B) (. A)
Theorem	ssdisj 2371	Intersection with a subclass of a disjoint class. (Contributed by FL, 24-Jan-2007.)
|- ((A (_ B /\ (B i^i C) = (/)) -> (A i^i C) = (/))
Theorem	disjpss 2372	A class is a proper subset of its union with a disjoint nonempty class.
|- (((A i^i B) = (/) /\ B =/= (/)) -> A (. (A u. B))
Theorem	undisj1 2373	The union of disjoint classes is disjoint.
|- (((A i^i C) = (/) /\ (B i^i C) = (/)) <-> ((A u. B) i^i C) = (/))
Theorem	undisj2 2374	The union of disjoint classes is disjoint.
|- (((A i^i B) = (/) /\ (A i^i C) = (/)) <-> (A i^i (B u. C)) = (/))
Theorem	ssindif0 2375	Subclass expressed in terms of intersection with difference from the universal class.
|- (A (_ B <-> (A i^i (V \ B)) = (/))
Theorem	inelcm 2376	The intersection of classes with a common member is nonempty.
|- ((A e. B /\ A e. C) -> (B i^i C) =/= (/))
Theorem	minel 2377	A minimum element of a class has no elements in common with the class.
|- ((A e. B /\ (C i^i B) = (/)) -> -. A e. C)
Theorem	undif4 2378	Distribute union over difference.
|- ((A i^i C) = (/) -> (A u. (B \ C)) = ((A u. B) \ C))
Theorem	disjssun 2379	Subset relation for disjoint classes.
|- ((A i^i B) = (/) -> (A (_ (B u. C) <-> A (_ C))
Theorem	ssdif0 2380	Subclass expressed in terms of difference. Exercise 7 of [TakeutiZaring] p. 22.
|- (A (_ B <-> (A \ B) = (/))
Theorem	vdif0 2381	Universal class equality in terms of empty difference.
|- (A = V <-> (V \ A) = (/))
Theorem	pssdifn0 2382	A proper subclass has a nonempty difference.
|- ((A (_ B /\ A =/= B) -> (B \ A) =/= (/))
Theorem	ssnelpss 2383	A subclass missing a member is a proper subclass.
|- (A (_ B -> ((C e. B /\ -. C e. A) -> A (. B))
Theorem	pssnel 2384	A proper subclass has a member in one argument that's not in both.
|- (A (. B -> E.x(x e. B /\ -. x e. A))
Theorem	difin0ss 2385	Difference, intersection, and subclass relationship.
|- (((A \ B) i^i C) = (/) -> (C (_ A -> C (_ B))
Theorem	inssdif0 2386	Intersection, subclass, and difference relationship.
|- ((A i^i B) (_ C <-> (A i^i (B \ C)) = (/))
Theorem	difid 2387	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 2388	The difference between a class and the empty set. Part of Exercise 4.4 of [Stoll] p. 16.
|- (A \ (/)) = A
Theorem	0dif 2389	The difference between the empty set and a class. Part of Exercise 4.4 of [Stoll] p. 16.
|- ((/) \ A) = (/)
Theorem	difdisj 2390	A class and its relative complement are disjoint. Theorem 38 of [Suppes] p. 29.
|- (A i^i (B \ A)) = (/)
Theorem	difin0 2391	The difference of a class from its intersection is empty. Theorem 37 of [Suppes] p. 29.
|- ((A i^i B) \ B) = (/)
Theorem	undifv 2392	The union of a class and its complement is the universe. Theorem 5.1(5) of [Stoll] p. 17.
|- (A u. (V \ A)) = V
Theorem	undif1 2393	Absorption of difference by union. This decomposes a union into two disjoint classes (see difdisj 2390). Theorem 35 of [Suppes] p. 29.
|- ((A \ B) u. B) = (A u. B)
Theorem	undif2 2394	Absorption of difference by union. This decomposes a union into two disjoint classes (see difdisj 2390). Part of proof of Corollary 6K of [Enderton] p. 144.
|- (A u. (B \ A)) = (A u. B)
Theorem	inundif 2395	The intersection and class difference of a class with another class unite to give the original class. (Contributed by Paul Chapman, 5-Jun-2009.)
|- ((A i^i B) u. (A \ B)) = A
Theorem	difun2 2396	Absorption of union by difference. Theorem 36 of [Suppes] p. 29.
|- ((A u. B) \ B) = (A \ B)
Theorem	undif 2397	Union of complementary parts into whole.
|- (A (_ B <-> (A u. (B \ A)) = B)
Theorem	ssundif 2398	A condition equivalent to inclusion in the union of two classes.
|- (A (_ (B u. C) <-> (A \ B) (_ C)
Theorem	difcom 2399	Swap the arguments of a class difference.
|- ((A \ B) (_ C <-> (A \ C) (_ B)
Theorem	difdifdir 2400	Distributive law for class difference. Exercise 4.8 of [Stoll] p. 16.
|- ((A \ B) \ C) = ((A \ C) \ (B \ C))