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-10781

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

Type	Label	Description
Statement
Theorem	0ss 2301	The null set is a subset of any class. Part of Exercise 1 of [TakeutiZaring] p. 22.
|- (/) (_ A
Theorem	ss0b 2302	Any subset of the empty set is empty. Theorem 5 of [Suppes] p. 23 and its converse.
|- (A (_ (/) <-> A = (/))
Theorem	ss0 2303	Any subset of the empty set is empty. Theorem 5 of [Suppes] p. 23.
|- (A (_ (/) -> A = (/))
Theorem	sseq0 2304	A subclass of an empty class is empty.
|- ((A (_ B /\ B = (/)) -> A = (/))
Theorem	ssne0 2305	A class with a nonempty subclass is nonempty.
|- ((A (_ B /\ A =/= (/)) -> B =/= (/))
Theorem	un00 2306	Two classes are empty iff their union is empty.
|- ((A = (/) /\ B = (/)) <-> (A u. B) = (/))
Theorem	vss 2307	Only the universal class has the universal class as a subclass.
|- (V (_ A <-> A = V)
Theorem	0pss 2308	The null set is a proper subset of any non-empty set.
|- ((/) (. A <-> A =/= (/))
Theorem	npss0 2309	No set is a proper subset of the empty set.
|- -. A (. (/)
Theorem	pssv 2310	Any non-universal class is a proper subclass of the universal class.
|- (A (. V <-> -. A = V)
Theorem	disj 2311	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 2312	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 2313	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 2314	Two ways of saying that two classes are disjoint.
|- ((A i^i B) = (/) <-> A = (A \ B))
Theorem	disjne 2315	Members of disjoint sets are not equal.
|- (((A i^i B) = (/) /\ C e. A /\ D e. B) -> C =/= D)
Theorem	disj2 2316	Two ways of saying that two classes are disjoint.
|- ((A i^i B) = (/) <-> A (_ (V \ B))
Theorem	disj4 2317	Two ways of saying that two classes are disjoint.
|- ((A i^i B) = (/) <-> -. (A \ B) (. A)
Theorem	ssdisj 2318	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 2319	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 2320	The union of disjoint classes is disjoint.
|- (((A i^i C) = (/) /\ (B i^i C) = (/)) <-> ((A u. B) i^i C) = (/))
Theorem	undisj2 2321	The union of disjoint classes is disjoint.
|- (((A i^i B) = (/) /\ (A i^i C) = (/)) <-> (A i^i (B u. C)) = (/))
Theorem	ssindif0 2322	Subclass expressed in terms of intersection with difference from the universal class.
|- (A (_ B <-> (A i^i (V \ B)) = (/))
Theorem	inelcm 2323	The intersection of classes with a common member is nonempty.
|- ((A e. B /\ A e. C) -> (B i^i C) =/= (/))
Theorem	minel 2324	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 2325	Distribute union over difference.
|- ((A i^i C) = (/) -> (A u. (B \ C)) = ((A u. B) \ C))
Theorem	disjssun 2326	Subset relation for disjoint classes.
|- ((A i^i B) = (/) -> (A (_ (B u. C) <-> A (_ C))
Theorem	ssdif0 2327	Subclass expressed in terms of difference. Exercise 7 of [TakeutiZaring] p. 22.
|- (A (_ B <-> (A \ B) = (/))
Theorem	vdif0 2328	Universal class equality in terms of empty difference.
|- (A = V <-> (V \ A) = (/))
Theorem	pssdifn0 2329	A proper subclass has a nonempty difference.
|- ((A (_ B /\ A =/= B) -> (B \ A) =/= (/))
Theorem	ssnelpss 2330	A subclass missing a member is a proper subclass.
|- (A (_ B -> ((C e. B /\ -. C e. A) -> A (. B))
Theorem	pssnel 2331	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 2332	Difference, intersection, and subclass relationship.
|- (((A \ B) i^i C) = (/) -> (C (_ A -> C (_ B))
Theorem	inssdif0 2333	Intersection, subclass, and difference relationship.
|- ((A i^i B) (_ C <-> (A i^i (B \ C)) = (/))
Theorem	difid 2334	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 2335	The difference between a class and the empty set. Part of Exercise 4.4 of [Stoll] p. 16.
|- (A \ (/)) = A
Theorem	0dif 2336	The difference between the empty set and a class. Part of Exercise 4.4 of [Stoll] p. 16.
|- ((/) \ A) = (/)
Theorem	difdisj 2337	A class and its relative complement are disjoint. Theorem 38 of [Suppes] p. 29.
|- (A i^i (B \ A)) = (/)
Theorem	difin0 2338	The difference of a class from its intersection is empty. Theorem 37 of [Suppes] p. 29.
|- ((A i^i B) \ B) = (/)
Theorem	undifv 2339	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 2340	Absorption of difference by union. This decomposes a union into two disjoint classes (see difdisj 2337). Theorem 35 of [Suppes] p. 29.
|- ((A \ B) u. B) = (A u. B)
Theorem	undif2 2341	Absorption of difference by union. This decomposes a union into two disjoint classes (see difdisj 2337). Part of proof of Corollary 6K of [Enderton] p. 144.
|- (A u. (B \ A)) = (A u. B)
Theorem	difun2 2342	Absorption of union by difference. Theorem 36 of [Suppes] p. 29.
|- ((A u. B) \ B) = (A \ B)
Theorem	undif 2343	Union of complementary parts into whole.
|- (A (_ B <-> (A u. (B \ A)) = B)
Theorem	ssundif 2344	A condition equivalent to inclusion in the union of two classes.
|- (A (_ (B u. C) <-> (A \ B) (_ C)
Theorem	difcom 2345	Swap the arguments of a class difference.
|- ((A \ B) (_ C <-> (A \ C) (_ B)
Theorem	difdifdir 2346	Distributive law for class difference. Exercise 4.8 of [Stoll] p. 16.
|- ((A \ B) \ C) = ((A \ C) \ (B \ C))
Theorem	r19.2z 2347	Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1030). The restricted version is valid only when the domain of quantification is not empty.
|- ((A =/= (/) /\ A.x e. A ph) -> E.x e. A ph)
Theorem	r19.3rzv 2348	Restricted quantification of wff not containing quantified variable.
|- (A =/= (/) -> (ph <-> A.x e. A ph))
Theorem	r19.9rzv 2349	Restricted quantification of wff not containing quantified variable.
|- (A =/= (/) -> (ph <-> E.x e. A ph))
Theorem	r19.28zv 2350	Restricted quantifier version of Theorem 19.28 of [Margaris] p. 90. It is valid only when the domain of quantification is not empty.
|- (A =/= (/) -> (A.x e. A (ph /\ ps) <-> (ph /\ A.x e. A ps)))
Theorem	r19.37zv 2351	Restricted quantifier version of Theorem 19.37 of [Margaris] p. 90. It is valid only when the domain of quantification is not empty. (Contributed by Paul Chapman, 8-Oct-2007.)
|- (A =/= (/) -> (E.x e. A (ph -> ps) <-> (ph -> E.x e. A ps)))
Theorem	r19.45zv 2352	Restricted version of Theorem 19.45 of [Margaris] p. 90.
|- (A =/= (/) -> (E.x e. A (ph \/ ps) <-> (ph \/ E.x e. A ps)))
Theorem	r19.27zv 2353	Restricted quantifier version of Theorem 19.27 of [Margaris] p. 90. It is valid only when the domain of quantification is not empty.
|- (A =/= (/) -> (A.x e. A (ph /\ ps) <-> (A.x e. A ph /\ ps)))
Theorem	r19.36zv 2354	Restricted quantifier version of Theorem 19.36 of [Margaris] p. 90. It is valid only when the domain of quantification is not empty.
|- (A =/= (/) -> (E.x e. A (ph -> ps) <-> (A.x e. A ph -> ps)))
Theorem	rzal 2355	Vacuous quantification is always true.
|- (A = (/) -> A.x e. A ph)
Theorem	rexn0 2356	Restricted existential quantification implies its restriction is nonempty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.)
|- (E.x e. A ph -> A =/= (/))
Theorem	ralidm 2357	Idempotent law for restricted quantifier.
|- (A.x e. A A.x e. A ph <-> A.x e. A ph)
Theorem	ral0 2358	Vacuous universal quantification is always true.
|- A.x e. (/) ph
Theorem	ralf0 2359	The quantification of a falsehood is vacuous when true.
|- -. ph   =>   |- (A.x e. A ph <-> A = (/))
Theorem	raaan 2360	Rearrange restricted quantifiers.
|- (A.x e. A A.y e. A (ph /\ ps) <-> (A.x e. A ph /\ A.y e. A ps))
"Weak deduction theorem" for set theory
Syntax	cif 2361	Extend class notation to include the conditional operator. See df-if 2362 for a description. (In older databases this was denoted "ded".)
class if(ph, A, B)
Definition	df-if 2362	Define the conditional operator. Read if(ph, A, B) as "if ph then A else B." See iftrue 2366 and iffalse 2367 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 2383 for the main part of the weak deduction theorem, elimhyp 2390 to eliminate a hypothesis, and keephyp 2396 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(ph, A, B) = {x | ((x e. A /\ ph) \/ (x e. B /\ -. ph))}
Theorem	dfif2 2363	An alternate definition of the conditional operator df-if 2362 with one fewer connectives (but probably less intuitive to understand).
|- if(ph, A, B) = {x | ((x e. B -> ph) -> (x e. A /\ ph))}
Theorem	ifeq1 2364	Equality theorem for conditional operator.
|- (A = B -> if(ph, A, C) = if(ph, B, C))
Theorem	ifeq2 2365	Equality theorem for conditional operator.
|- (A = B -> if(ph, C, A) = if(ph, C, B))
Theorem	iftrue 2366	Value of the conditional operator when its first argument is true.
|- (ph -> if(ph, A, B) = A)
Theorem	iffalse 2367	Value of the conditional operator when its first argument is false.
|- (-. ph -> if(ph, A, B) = B)
Theorem	ifeq12 2368	Equality theorem for conditional operators.
|- ((A = B /\ C = D) -> if(ph, A, C) = if(ph, B, D))
Theorem	ifeq1d 2369	Equality deduction for conditional operator.
|- (ph -> A = B)   =>   |- (ph -> if(ps, A, C) = if(ps, B, C))
Theorem	ifeq2d 2370	Equality deduction for conditional operator.
|- (ph -> A = B)   =>   |- (ph -> if(ps, C, A) = if(ps, C, B))
Theorem	ifbi 2371	Equivalence theorem for conditional operators. (Contributed by Raph Levien, 15-Jan-2004.)
|- ((ph <-> ps) -> if(ph, A, B) = if(ps, A, B))
Theorem	ifbid 2372	Equivalence deduction for conditional operators.
|- (ph -> (ps <-> ch))   =>   |- (ph -> if(ps, A, B) = if(ch, A, B))
Theorem	hbif 2373	Bound-variable hypothesis builder for a conditional operator.
|- (ph -> A.xph)   &   |- (y e. A ->