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

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

Type	Label	Description
Statement
Theorem	ssnelpss 2301	A subclass missing a member is a proper subclass.
|- (A (_ B -> ((C e. B /\ -. C e. A) -> A (. B))
Theorem	pssnel 2302	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 2303	Difference, intersection, and subclass relationship.
|- (((A \ B) i^i C) = (/) -> (C (_ A -> C (_ B))
Theorem	inssdif0 2304	Intersection, subclass, and difference relationship.
|- ((A i^i B) (_ C <-> (A i^i (B \ C)) = (/))
Theorem	difid 2305	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 2306	The difference between a class and the empty set. Part of Exercise 4.4 of [Stoll] p. 16.
|- (A \ (/)) = A
Theorem	0dif 2307	The difference between the empty set and a class. Part of Exercise 4.4 of [Stoll] p. 16.
|- ((/) \ A) = (/)
Theorem	difdisj 2308	A class and its relative complement are disjoint. Theorem 38 of [Suppes] p. 29.
|- (A i^i (B \ A)) = (/)
Theorem	difin0 2309	The difference of a class from its intersection is empty. Theorem 37 of [Suppes] p. 29.
|- ((A i^i B) \ B) = (/)
Theorem	undifv 2310	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 2311	Absorption of difference by union. This decomposes a union into two disjoint classes (see difdisj 2308). Theorem 35 of [Suppes] p. 29.
|- ((A \ B) u. B) = (A u. B)
Theorem	undif2 2312	Absorption of difference by union. This decomposes a union into two disjoint classes (see difdisj 2308). Part of proof of Corollary 6K of [Enderton] p. 144.
|- (A u. (B \ A)) = (A u. B)
Theorem	difun2 2313	Absorption of union by difference. Theorem 36 of [Suppes] p. 29.
|- ((A u. B) \ B) = (A \ B)
Theorem	undif 2314	Union of complementary parts into whole.
|- (A (_ B <-> (A u. (B \ A)) = B)
Theorem	ssundif 2315	A condition equivalent to inclusion in the union of two classes.
|- (A (_ (B u. C) <-> (A \ B) (_ C)
Theorem	difcom 2316	Swap the arguments of a class difference.
|- ((A \ B) (_ C <-> (A \ C) (_ B)
Theorem	difdifdir 2317	Distributive law for class difference. Exercise 4.8 of [Stoll] p. 16.
|- ((A \ B) \ C) = ((A \ C) \ (B \ C))
Theorem	r19.2z 2318	Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1006). 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 2319	Restricted quantification of wff not containing quantified variable.
|- (A =/= (/) -> (ph <-> A.x e. A ph))
Theorem	r19.9rzv 2320	Restricted quantification of wff not containing quantified variable.
|- (A =/= (/) -> (ph <-> E.x e. A ph))
Theorem	r19.28zv 2321	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 2322	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 2323	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 2324	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 2325	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 2326	Vacuous quantification is always true.
|- (A = (/) -> A.x e. A ph)
Theorem	rexn0 2327	Restricted existential quantification implies its restriction is nonempty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.)
|- (E.x e. A ph -> A =/= (/))
Theorem	ralidm 2328	Idempotent law for restricted quantifier.
|- (A.x e. A A.x e. A ph <-> A.x e. A ph)
Theorem	ral0 2329	Vacuous universal quantification is always true.
|- A.x e. (/) ph
Theorem	ralf0 2330	The quantification of a falsehood is vacuous when true.
|- -. ph   =>   |- (A.x e. A ph <-> A = (/))
Theorem	raaan 2331	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 2332	Extend class notation to include the conditional operator. See df-if 2333 for a description. (In older databases this was denoted "ded".)
class if(ph, A, B)
Definition	df-if 2333	Define the conditional operator. Read if(ph, A, B) as "if ph then A else B." See iftrue 2337 and iffalse 2338 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 2354 for the main part of the weak deduction theorem, elimhyp 2361 to eliminate a hypothesis, and keephyp 2367 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 2334	An alternate definition of the conditional operator df-if 2333 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 2335	Equality theorem for conditional operator.
|- (A = B -> if(ph, A, C) = if(ph, B, C))
Theorem	ifeq2 2336	Equality theorem for conditional operator.
|- (A = B -> if(ph, C, A) = if(ph, C, B))
Theorem	iftrue 2337	Value of the conditional operator when its first argument is true.
|- (ph -> if(ph, A, B) = A)
Theorem	iffalse 2338	Value of the conditional operator when its first argument is false.
|- (-. ph -> if(ph, A, B) = B)
Theorem	ifeq12 2339	Equality theorem for conditional operators.
|- ((A = B /\ C = D) -> if(ph, A, C) = if(ph, B, D))
Theorem	ifeq1d 2340	Equality deduction for conditional operator.
|- (ph -> A = B)   =>   |- (ph -> if(ps, A, C) = if(ps, B, C))
Theorem	ifeq2d 2341	Equality deduction for conditional operator.
|- (ph -> A = B)   =>   |- (ph -> if(ps, C, A) = if(ps, C, B))
Theorem	ifbi 2342	Equivalence theorem for conditional operators. (Contributed by Raph Levien, 15-Jan-2004.)
|- ((ph <-> ps) -> if(ph, A, B) = if(ps, A, B))
Theorem	ifbid 2343	Equivalence deduction for conditional operators.
|- (ph -> (ps <-> ch))   =>   |- (ph -> if(ps, A, B) = if(ch, A, B))
Theorem	hbif 2344	Bound-variable hypothesis builder for a conditional operator.
|- (ph -> A.xph)   &   |- (y e. A -> A.x y e. A)   &   |- (y e. B -> A.x y e. B)   =>   |- (y e. if(ph, A, B) -> A.x y e. if(ph, A, B))
Theorem	elimif 2345	Elimination of a conditional operator contained in a wff ps.
|- (if(ph, A, B) = A -> (ps <-> ch))   &   |- (if(ph, A, B) = B -> (ps <-> th))   =>   |- (ps <-> ((ph /\ ch) \/ (-. ph /\ th)))
Theorem	ifboth 2346	A wff th containing a conditional operator is true when both of its cases are true.
|- (A = if(ph, A, B) -> (ps <-> th))   &   |- (B = if(ph, A, B) -> (ch <-> th))   =>   |- ((ps /\ ch) -> th)
Theorem	ifid 2347	Identical true and false arguments in the conditional operator.
|- if(ph, A, A) = A
Theorem	eqif 2348	Expansion of an equality with a conditional operator.
|- (A = if(ph, B, C) <-> ((ph /\ A = B) \/ (-. ph /\ A = C)))
Theorem	elif 2349	Membership in a conditional operator.
|- (A e. if(ph, B, C) <-> ((ph /\ A e. B) \/ (-. ph /\ A e. C)))
Theorem	ifel 2350	Membership of a conditional operator.
|- (if(ph, A, B) e. C <-> ((ph /\ A e. C) \/ (-. ph /\ B e. C)))
Theorem	ifcl 2351	Membership (closure) of a conditional operator.
|- ((A e. C /\ B e. C) -> if(ph, A, B) e. C)
Theorem	ifor 2352	The possible values of a conditional operator.
|- (if(ph, A, B) = A \/ if(ph, A, B) = B)
Theorem	ifswap 2353	Negating the first argument swaps the last two arguments of a conditional operator.
|- if(-. ph, A, B) = if(ph, B, A)
Theorem	dedth 2354	Weak deduction theorem that eliminates a hypothesis ph, making it become an antecedent. We assume that a proof exists for ph when the class variable A is replaced with a specific class B. The hypothesis ch should be assigned to the inference, and the inference's hypothesis eliminated with elimhyp 2361. If the inference has other hypotheses with class variable A, these can be kept by assigning keephyp 2367 to them. For more information, see the Deduction Theorem http://us.metamath.org/mpegif/mmdeduction.html.
|- (A = if(ph, A, B) -> (ps <-> ch))   &   |- ch   =>   |- (ph -> ps)
Theorem	dedth2v 2355	Weak deduction theorem for eliminating a hypothesis with 2 class variables. Note: if the hypothesis can be separated into two hypotheses, each with one class variable, then dedth2h 2358 is simpler to use. See also comments in dedth 2354.
|- (A = if(ph, A, C) -> (ps <-> ch))   &   |- (B = if(ph, B, D) -> (ch <-> th))   &   |- th   =>   |- (ph -> ps)
Theorem	dedth3v 2356	Weak deduction theorem for eliminating a hypothesis with 3 class variables. See comments in dedth2v 2355.
|- (A = if(ph, A, D) -> (ps <-> ch))   &   |- (B = if(ph, B, R) -> (ch <-> th))   &   |- (C = if(ph, C, S) -> (th <-> ta))   &   |- ta   =>   |- (ph -> ps)
Theorem	dedth4v 2357	Weak deduction theorem for eliminating a hypothesis with 4 class variables. See comments in dedth2v 2355.
|- (A = if(ph, A, R) -> (ps <-> ch))   &   |- (B = if(ph, B, S) -> (ch <-> th))   &   |- (C = if(ph, C, T) -> (th <-> ta))   &   |- (D = if(ph, D, U) -> (ta <-> et))   &   |- et   =>   |- (ph -> ps)
Theorem	dedth2h 2358	Weak deduction theorem eliminating two hypotheses. This theorem is simpler to use than dedth2v 2355 but requires that each hypothesis has exactly one class variable. See also comments in dedth 2354.
|- (A = if(ph, A, C) -> (ch <-> th))   &   |- (B = if(ps, B, D