mmtheorems30 - 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-10766

Statement List for Metamath Proof Explorer - 2901-3000 - Page 30 of 108

Type	Label	Description
Statement
Theorem	reusn 2901	A way to express restricted existential uniqueness of a wff: its restricted class abstraction is a singleton.
|- (E!x e. A ph <-> E.y{x e. A | ph} = {y})
Theorem	reusni 2902	Restricted existential uniqueness determined by a singleton.
|- B e. V   =>   |- ({x e. A | ph} = {B} -> E!x e. A ph)
Theorem	rabsnt 2903	Truth implied by equality of a restricted class abstraction and a singleton.
|- B e. V   &   |- (x = B -> (ph <-> ps))   =>   |- ({x e. A | ph} = {B} -> ps)
Theorem	reuunisn 2904	A restricted class abstraction with a unique member can be expressed as a singleton.
|- (E!x e. A ph -> {x e. A | ph} = {U.{x e. A | ph}})
Theorem	alxfr 2905	Transfer universal quantification from a variable x to another variable y contained in expression A.
|- (x = A -> (ph <-> ps))   =>   |- ((A.y A e. B /\ A.xE.y x = A) -> (A.xph <-> A.yps))
Theorem	ralxfrd 2906	Transfer universal quantification from a variable x to another variable y contained in expression A.
|- ((ph /\ y e. B) -> A e. B)   &   |- ((ph /\ x e. B) -> E.y e. B x = A)   &   |- ((ph /\ x = A) -> (ps <-> ch))   =>   |- (ph -> (A.x e. B ps <-> A.y e. B ch))
Theorem	rexxfrd 2907	Transfer universal quantification from a variable x to another variable y contained in expression A. (Contributed by FL, 10-Apr-2007.)
|- ((ph /\ y e. B) -> A e. B)   &   |- ((ph /\ x e. B) -> E.y e. B x = A)   &   |- ((ph /\ x = A) -> (ps <-> ch))   =>   |- (ph -> (E.x e. B ps <-> E.y e. B ch))
Theorem	ralxfr 2908	Transfer universal quantification from a variable x to another variable y contained in expression A.
|- (y e. B -> A e. B)   &   |- (x e. B -> E.y e. B x = A)   &   |- (x = A -> (ph <-> ps))   =>   |- (A.x e. B ph <-> A.y e. B ps)
Theorem	ralxfrALT 2909	Transfer universal quantification from a variable x to another variable y contained in expression A.
|- (y e. B -> A e. B)   &   |- (x e. B -> E.y e. B x = A)   &   |- (x = A -> (ph <-> ps))   =>   |- (A.x e. B ph <-> A.y e. B ps)
Theorem	rexxfr 2910	Transfer existence from a variable x to another variable y contained in expression A.
|- (y e. B -> A e. B)   &   |- (x e. B -> E.y e. B x = A)   &   |- (x = A -> (ph <-> ps))   =>   |- (E.x e. B ph <-> E.y e. B ps)
Theorem	rabxfr 2911	Abstraction class membership after substituting an expression A (containing y) for x in the class expression ph.
|- (z e. B -> A.y z e. B)   &   |- (z e. C -> A.y z e. C)   &   |- (y e. D -> A e. D)   &   |- (x = A -> (ph <-> ps))   &   |- (y = B -> A = C)   =>   |- (B e. D -> (C e. {x e. D | ph} <-> B e. {y e. D | ps}))
Theorem	reuxfr2 2912	Transfer existential uniqueness from a variable x to another variable y contained in expression A.
|- (y e. B -> A e. B)   &   |- (x e. B -> E*y(y e. B /\ x = A))   =>   |- (E!x e. B E.y e. B (x = A /\ ph) <-> E!y e. B ph)
Theorem	reuxfr 2913	Transfer existential uniqueness from a variable x to another variable y contained in expression A. Use reuhyp 2914 to eliminate the second hypothesis.
|- (y e. B -> A e. B)   &   |- (x e. B -> E!y e. B x = A)   &   |- (x = A -> (ph <-> ps))   =>   |- (E!x e. B ph <-> E!y e. B ps)
Theorem	reuhyp 2914	A theorem useful for eliminating the restricted existential uniqueness hypotheses in reuxfr 2913.
|- (x e. C -> B e. C)   &   |- ((x e. C /\ y e. C) -> (x = A <-> y = B))   =>   |- (x e. C -> E!y e. C x = A)
Theorem	reuunixfr 2915	Change the variable x in the expression for "the unique A such that ph" to another variable y contained in expression B. Use reuhyp 2914 to eliminate the last hypothesis.
|- (z e. C -> A.y z e. C)   &   |- (y e. A -> B e. A)   &   |- (U.{y e. A | ps} e. A -> C e. A)   &   |- (x = B -> (ph <-> ps))   &   |- (y = U.{y e. A | ps} -> B = C)   &   |- (x e. A -> E!y e. A x = B)   =>   |- (E!x e. A ph -> U.{x e. A | ph} = C)
Theorem	uniexb 2916	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 2917	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 2918	The union of the universe is the universe. Exercise 4.12(c) of [Mendelson] p. 235.
|- U.V = V
Theorem	eldifpw 2919	Membership in a power class difference.
|- C e. V   =>   |- ((A e. P~B /\ -. C (_ B) -> (A u. C) e. (P~(B u. C) \ P~B))
Theorem	elpwun 2920	Membership in the power class of a union.
|- C e. V   =>   |- (A e. P~(B u. C) <-> (A \ C) e. P~B)
Theorem	elpwunsn 2921	Membership in an extension of a power class.
|- (A e. (P~(B u. {C}) \ P~B) -> C e. A)
Theorem	op1stb 2922	Extract the first member of an ordered pair. Theorem 73 of [Suppes] p. 42. (See op2ndb 3460 to extract the second member, op1sta 3457 for an alternate version, and op1st 4094 for the preferred version.)
|- A e. V   =>   |- |^||^|<.A, B>. = A
Theorem	iunpw 2923	The power class of an intersection in terms of indexed intersection. Part of Exercise 24(b) of [Enderton] p. 33.
|- A e. V   =>   |- (E.x e. A x = U.A <-> P~U.A = U_x e. A P~x)
Founded and well-ordering relations
Syntax	wfr 2924	Extend wff notation to include the founded predicate. Read: 'R is a founded relation on A.'
wff R Fr A
Syntax	wwe 2925	Extend wff notation to include the well-ordering predicate. Read: 'R well-orders A.'
wff R We A
Definition	df-fr 2926	Define a founded relation. For alternate definitions, see dffr2 2928 and dffr3 3440.
|- (R Fr A <-> A.x((x (_ A /\ x =/= (/)) -> E.y e. x A.z e. x -. zRy))
Theorem	fri 2927	Property of founded relation (one direction of definition).
|- (((B e. C /\ R Fr A) /\ (B (_ A /\ B =/= (/))) -> E.x e. B A.y e. B -. yRx)
Theorem	dffr2 2928	Alternate definition of founded relation. Similar to Definition 6.21 of [TakeutiZaring] p. 30.
|- (R Fr A <-> A.x((x (_ A /\ x =/= (/)) -> E.y e. x (x i^i {z | zRy}) = (/)))
Theorem	frc 2929	Property of founded relation (one direction of definition using class variables).
|- B e. V   =>   |- ((R Fr A /\ B (_ A /\ B =/= (/)) -> E.x e. B (B i^i {y | yRx}) = (/))
Theorem	frss 2930	Subset theorem for the founded predicate. Exercise 1 of [TakeutiZaring] p. 31.
|- (A (_ B -> (R Fr B -> R Fr A))
Theorem	freq1 2931	Equality theorem for the founded predicate.
|- (R = S -> (R Fr A <-> S Fr A))
Theorem	freq2 2932	Equality theorem for the founded predicate.
|- (A = B -> (R Fr A <-> R Fr B))
Theorem	frirr 2933	A founded relation is irreflexive. Special case of Proposition 6.23 of [TakeutiZaring] p. 30.
|- ((R Fr A /\ x e. A) -> -. xRx)
Theorem	fr2nr 2934	A founded relation has no 2-cycle loops. Special case of Proposition 6.23 of [TakeutiZaring] p. 30.
|- ((R Fr A /\ (x e. A /\ y e. A)) -> -. (xRy /\ yRx))
Theorem	fr3nr 2935	A founded relation has no 3-cycle loops. Special case of Proposition 6.23 of [TakeutiZaring] p. 30.
|- ((R Fr A /\ (x e. A /\ y e. A /\ z e. A)) -> -. (xRy /\ yRz /\ zRx))
Theorem	fr0 2936	Any relation is founded on the empty set.
|- R Fr (/)
Theorem	efrirr 2937	Irreflexivitiy of the epsilon relation: a class founded by epsilon is not a member of itself.
|- (E Fr A -> -. A e. A)
Theorem	efrn2lp 2938	A set founded by epsilon contains no 2-cycle loops.
|- ((E Fr A /\ (x e. A /\ y e. A)) -> -. (x e. y /\ y e. x))
Theorem	epne3 2939	A set founded by epsilon contains no 3-cycle loops.
|- ((E Fr A /\ (x e. A /\ y e. A /\ z e. A)) -> -. (x e. y /\ y e. z /\ z e. x))
Theorem	tz7.2 2940	Similar to Theorem 7.2 of [TakeutiZaring] p. 35, of except that the Axiom of Regularity is not required due to antecedent E Fr A.
|- ((Tr A /\ E Fr A /\ B e. A) -> (B (_ A /\ B =/= A))
Theorem	dfepfr 2941	An alternate way of saying that the epsilon relation is founded.
|- (E Fr A <-> A.x((x (_ A /\ x =/= (/)) -> E.y e. x (x i^i y) = (/)))
Theorem	epfrc 2942	A subset of an epsilon-founded class has a minimal element.
|- B e. V   =>   |- ((E Fr A /\ B (_ A /\ B =/= (/)) -> E.x e. B (B i^i x) = (/))
Definition	df-we 2943	Define a well-ordering. For an alternate definition see dfwe2 2944.
|- (R We A <-> (R Fr A /\ R Or A))
Theorem	dfwe2 2944	Alternate definition of well-ordering. Definition 6.24(2) of [TakeutiZaring] p. 30.
|- (R We A <-> (R Fr A /\ A.x e. A A.y e. A (xRy \/ x = y \/ yRx)))
Theorem	wess 2945	Subset theorem for the well-ordering predicate. Exercise 4 of [TakeutiZaring] p. 31.
|- (A (_ B -> (R We B -> R We A))
Theorem	weeq1 2946	Equality theorem for the well-ordering predicate.
|- (R = S -> (R We A <-> S We A))
Theorem	weeq2 2947	Equality theorem for the well-ordering predicate.
|- (A = B -> (R We A <-> R We B))
Theorem	wefr 2948	A well-ordering is founded.
|- (R We A -> R Fr A)
Theorem	weso 2949	A well-ordering is a strict ordering.
|- (R We A -> R Or A)
Theorem	wecmpep 2950	The elements of an epsilon well-ordering are comparable.
|-