mmtheorems26 - 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 - 2501-2600 - Page 26 of 123

Type	Label	Description
Statement
Theorem	dftp2 2501	Alternate definition of unordered triple of classes. Special case of Definition 5.3 of [TakeutiZaring] p. 16.
|- {A, B, C} = {x | (x = A \/ x = B \/ x = C)}
Theorem	disjsn 2502	Intersection with the singleton of a non-member is disjoint.
|- ((A i^i {B}) = (/) <-> -. B e. A)
Theorem	disjsn2 2503	Intersection of distinct singletons is disjoint.
|- (A =/= B -> ({A} i^i {B}) = (/))
Theorem	snprc 2504	The singleton of a proper class (one that doesn't exist) is the empty set. Theorem 7.2 of [Quine] p. 48.
|- (-. A e. V <-> {A} = (/))
Theorem	r19.12sn 2505	Special case of r19.12 1786 where its converse holds.
|- A e. V   =>   |- (E.x e. {A}A.y e. B ph <-> A.y e. B E.x e. {A}ph)
Theorem	rabsn 2506	Condition where a restricted class abstraction is a singleton.
|- (B e. A -> {x e. A | x = B} = {B})
Theorem	eusn 2507	Another way to express existential uniqueness of a wff: its class abstraction is a singleton.
|- (E!xph <-> E.x{x | ph} = {x})
Theorem	prcom 2508	Commutative law for unordered pairs.
|- {A, B} = {B, A}
Theorem	preq1 2509	An equality theorem for unordered pairs.
|- (A = B -> {A, C} = {B, C})
Theorem	preq2 2510	An equality theorem for unordered pairs.
|- (A = B -> {C, A} = {C, B})
Theorem	prid1g 2511	An unordered pair contains its first member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by Stefan Allan, 8-Nov-2008.)
|- (A e. C -> A e. {A, B})
Theorem	prid2g 2512	An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by Stefan Allan, 8-Nov-2008.)
|- (B e. C -> B e. {A, B})
Theorem	prid1 2513	An unordered pair contains its first member. Part of Theorem 7.6 of [Quine] p. 49.
|- A e. V   =>   |- A e. {A, B}
Theorem	prid2 2514	An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49.
|- B e. V   =>   |- B e. {A, B}
Theorem	prprc1 2515	A proper class vanishes in an unordered pair.
|- (-. A e. V -> {A, B} = {B})
Theorem	prprc2 2516	A proper class vanishes in an unordered pair.
|- (-. B e. V -> {A, B} = {A})
Theorem	prprc 2517	An unordered pair containing two proper classes is the empty set.
|- ((-. A e. V /\ -. B e. V) -> {A, B} = (/))
Theorem	tpi1 2518	One of the three elements of an unordered triple.
|- A e. V   =>   |- A e. {A, B, C}
Theorem	tpi2 2519	One of the three elements of an unordered triple.
|- B e. V   =>   |- B e. {A, B, C}
Theorem	tpi3 2520	One of the three elements of an unordered triple.
|- C e. V   =>   |- C e. {A, B, C}
Theorem	snnzg 2521	The singleton of a set is not empty.
|- (A e. B -> {A} =/= (/))
Theorem	snnz 2522	The singleton of a set is not empty.
|- A e. V   =>   |- {A} =/= (/)
Theorem	prnz 2523	A pair containing a set is not empty.
|- A e. V   =>   |- {A, B} =/= (/)
Theorem	tpnz 2524	A triplet containing a set is not empty.
|- A e. V   =>   |- {A, B, C} =/= (/)
Theorem	snss 2525	The singleton of an element of a class is a subset of the class. Theorem 7.4 of [Quine] p. 49.
|- A e. V   =>   |- (A e. B <-> {A} (_ B)
Theorem	eldifsn 2526	Membership in a set with an element removed.
|- (A e. (B \ {C}) <-> (A e. B /\ A =/= C))
Theorem	snssg 2527	The singleton of an element of a class is a subset of the class. Theorem 7.4 of [Quine] p. 49.
|- (A e. C -> (A e. B <-> {A} (_ B))
Theorem	difsn 2528	An element not in a set can be removed without affecting the set.
|- (-. A e. B -> (B \ {A}) = B)
Theorem	difprsn 2529	Removal of a singleton from an unordered pair.
|- ({A, B} \ {A}) (_ {B}
Theorem	snssi 2530	The singleton of an element of a class is a subset of the class.
|- (A e. B -> {A} (_ B)
Theorem	difsnid 2531	If we remove a single element from a class then put it back in, we end up with the original class.
|- (B e. A -> ((A \ {B}) u. {B}) = A)
Theorem	pw0 2532	Compute the power set of the empty set. Theorem 89 of [Suppes] p. 47. (The proof was shortened by Eric Schmidt, 4-Apr-2007.)
|- P~(/) = {(/)}
Theorem	pwpw0 2533	Compute the power set of the power set of the empty set. (See pw0 2532 for the power set of the empty set.) Theorem 90 of [Suppes] p. 48. Although this theorem is a special case of pwsn 2565, we have chosen to show a direct elementary proof.
|- P~{(/)} = {(/), {(/)}}
Theorem	snsspr1 2534	A singleton is a subset of an unordered pair containing its member.
|- {A} (_ {A, B}
Theorem	snsspr2 2535	A singleton is a subset of an unordered pair containing its member.
|- {B} (_ {A, B}
Theorem	prss 2536	A pair of elements of a class is a subset of the class. Theorem 7.5 of [Quine] p. 49.
|- A e. V   &   |- B e. V   =>   |- ((A e. C /\ B e. C) <-> {A, B} (_ C)
Theorem	prssg 2537	A pair of elements of a class is a subset of the class. Theorem 7.5 of [Quine] p. 49.
|- ((A e. R /\ B e. S) -> ((A e. C /\ B e. C) <-> {A, B} (_ C))
Theorem	sssn 2538	The subsets of a singleton.
|- (A (_ {B} <-> (A = (/) \/ A = {B}))
Theorem	eqsn 2539	Two ways to express that a nonempty set equals a singleton.
|- (A =/= (/) -> (A = {B} <-> A.x e. A x = B))
Theorem	sspr 2540	The subsets of a pair.
|- (A (_ {B, C} <-> ((A = (/) \/ A = {B}) \/ (A = {C} \/ A = {B, C})))
Theorem	tpss 2541	A triplet of elements of a class is a subset of the class.
|- A e. V   &   |- B e. V   &   |- C e. V   =>   |- ((A e. D /\ B e. D /\ C e. D) <-> {A, B, C} (_ D)
Theorem	sneqr 2542	If the singletons of two sets are equal, the two sets are equal. Part of Exercise 4 of [TakeutiZaring] p. 15.
|- A e. V   =>   |- ({A} = {B} -> A = B)
Theorem	snsssn 2543	If a singleton is a subset of another, their members are equal.
|- A e. V   =>   |- ({A} (_ {B} -> A = B)
Theorem	snsspw 2544	The singleton of a class is a subset of its power class.
|- {A} (_ P~A
Theorem	prsspw 2545	An unordered pair belongs to the power class of a class iff each member belongs to the class.
|- A e. V   &   |- B e. V   =>   |- ({A, B} (_ P~C <-> (A (_ C /\ B (_ C))
Theorem	preqr1 2546	Reverse equality lemma for unordered pairs. If two unordered pairs have the same second element, the first elements are equal.
|- A e. V   &   |- B e. V   =>   |- ({A, C} = {B, C} -> A = B)
Theorem	preqr2 2547	Reverse equality lemma for unordered pairs. If two unordered pairs have the same first element, the second elements are equal.
|- A e. V   &   |- B e. V   =>   |- ({C, A} = {C, B} -> A = B)
Theorem	preq12b 2548	Equality relationship for two unordered pairs.
|- A e. V   &   |- B e. V   &   |- C e. V   &   |- D e. V   =>   |- ({A, B} = {C, D} <-> ((A = C /\ B = D) \/ (A = D /\ B = C)))
Theorem	prel12 2549	Equality of two unordered pairs.
|- A e. V   &   |- B e. V   &   |- C e. V   &   |- D e. V   =>   |- (-. A = B -> ({A, B} = {C, D} <-> (A e. {C, D} /\ B e. {C, D})))
Theorem	opthpr 2550	A way to represent ordered pairs using unordered pairs with distinct members.
|- A e. V   &   |- B e. V   &   |- C e. V   &   |- D e. V   =>   |- (A =/= D -> ({A, B} = {C, D} <-> (A = C /\ B = D)))
Theorem	preqsn 2551	Equivalence for a pair equal to a singleton.
|- A e. V   &   |- B e. V   &   |- C e. V   =>   |- ({A, B} = {C} <-> (A = B /\ B = C))
Theorem	opeq1 2552	Equality theorem for ordered pairs.
|- (A = B -> <.A, C>. = <.B, C>.)
Theorem	opeq2 2553	Equality theorem for ordered pairs.
|- (A = B -> <.C, A>. = <.C, B>.)
Theorem	opeq12 2554	Equality theorem for ordered pairs.
|- ((A = C /\ B = D) -> <.A, B>. = <.C, D>.)
Theorem	opeq1i 2555	Equality inference for ordered pairs.
|- A = B   =>   |- <.A, C>. = <.B, C>.
Theorem	opeq2i 2556	Equality inference for ordered pairs.
|- A = B   =>   |- <.C, A>. = <.C, B>.
Theorem	opeq12i 2557	Equality inference for ordered pairs. (The proof was shortened by Eric Schmidt, 4-Apr-2007.)
|- A = B   &   |- C = D   =>   |- <.A, C>. = <.B, D>.
Theorem	opeq1d 2558	Equality deduction for ordered pairs.
|- (ph -> A = B)   =>   |- (ph -> <.A, C>. = <.B, C>.)
Theorem	opeq2d 2559	Equality deduction for ordered pairs.
|- (ph -> A = B)   =>   |- (ph -> <.C, A>. = <.C, B>.)
Theorem	opeq12d 2560	Equality deduction for ordered pairs.
|- (ph -> A = B)   &   |- (ph -> C = D)   =>   |- (ph -> <.A, C>. = <.B, D>.)
Theorem	hbop 2561	Bound-variable hypothesis builder for ordered pairs.
|- (y e. A -> A.x y e. A)   &   |- (y e. B -> A.x y e. B)   =>   |- (y e. <.A, B>. -> A.x y e. <.A, B>.)
Theorem	hbopd 2562	Deduction version of bound-variable hypothesis builder hbop 2561.
|- (ph -> A.xph)   &   |- (ph -> (y e. A -> A.x y e. A))   &   |- (ph -> (y e. B -> A.x y e. B))   =>   |- (ph -> (y e. <.A, B>. -> A.x y e. <.A, B>.))
Theorem	opprc1 2563	Expansion of an ordered pair when the first member is a proper class. See also opprc1b 2872, opprc2 2564, opprc3 2873.
|- (-. A e. V -> <.A, B>. = {(/), {B}})
Theorem	opprc2 2564	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	pwsn 2565	The power set of a singleton.
|- P~{A} = {(/), {A}}
Theorem	pwsnALT 2566	The power set of a singleton (direct proof).
|- P~{A} = {(/), {A}}
Theorem	pwpr 2567	The power set of an unordered pair.
|- P~{A, B} = ({(/), {A}} u. {{B}, {A, B}})
Theorem	pwv 2568	The power class of the universe is the universe. Exercise 4.12(d) of [Mendelson] p. 235.
|- P~V = V
The union of a class
Syntax	cuni 2569	Extend class notation to include the union of a class (read: 'union A ')
class U.A
Definition	df-uni 2570	Define the union of a class i.e. the collection of all members of the members of the class. Definition 5.5 of [TakeutiZaring] p. 16.
|- U.A = {x | E.y(x e. y /\ y e. A)}
Theorem	dfuni2 2571	Alternate definition of class union.
|- U.A = {x | E.y e. A x e. y}
Theorem	eluni 2572	Membership in class union.
|- (A e. U.B <-> E.x(A e. x /\ x e. B))
Theorem	eluni2 2573	Membership in class union. Restricted quantifier version.
|- (A e. U.B <-> E.x e. B A e. x)
Theorem	elunii 2574	Membership in class union.
|- ((A e. B /\ B e. C) -> A e. U.C)
Theorem	hbuni 2575	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	unieq 2576	Equality theorem for class union. Exercise 15 of [TakeutiZaring] p. 18.
|- (A = B -> U.A = U.B)
Theorem	unieqi 2577	Inference of equality of two class unions.
|- A = B   =>   |- U.A = U.B
Theorem	unieqd 2578	Deduction of equality of two class unions.
|- (ph -> A = B)   =>   |- (ph -> U.A = U.B)
Theorem	eluniab 2579	Membership in union of a class abstraction.
|- (A e. U.{x | ph} <-> E.x(A e. x /\ ph))
Theorem	elunirab 2580	Membership in union of a class abstraction.
|- (A e. U.{x e. B | ph} <-> E.x e. B (A e. x /\ ph))
Theorem	unipr 2581	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	uniprg 2582	The union of a pair is the union of its members. Proposition 5.7 of [TakeutiZaring] p. 16.
|- ((A e. C /\ B e. D) -> U.{A, B} = (A u. B))
Theorem	unisn 2583	A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53.
|- A e. V   =>   |- U.{A} = A
Theorem	reucl 2584	Closure law for "the unique element in A such that ph."
|- (E!x e. A ph -> U.{x e. A | ph} e. A)
Theorem	unisng 2585	A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53.
|- (A e. B -> U.{A} = A)
Theorem	uniun 2586	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 2587	The class union of the intersection of two classes. Exercise 4.12(n) of [Mendelson] p. 235. See uninqs 10730 for a condition where equality holds.
|- U.(A i^i B) (_ (U.A i^i U.B)
Theorem	uniss 2588	Subclass relationship for class union. Theorem 61 of [Suppes] p. 39.
|- (A (_ B -> U.A (_ U.B)
Theorem	ssuni 2589	Subclass relationship for class union.
|- ((A (_ B /\ B e. C) -> A (_ U.C)
Theorem	uni0b 2590	The union of a set is empty iff the set is included in the singleton of the empty set.
|- (U.A = (/) <-> A (_ {(/)})
Theorem	uni0c 2591	The union of a set is empty iff all of its members are empty.
|- (U.A = (/) <-> A.x e. A x = (/))
Theorem	uni0 2592	The union of the empty set is the empty set. Theorem 8.7 of [Quine] p. 54. (Reproved without relying on ax-nul 2784 by Eric Schmidt, 4-Apr-2007.)
|- U.(/) = (/)
Theorem	elssuni 2593	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	unissel 2594	Condition turning a subclass relationship for union into an equality.
|- ((U.A (_ B /\ B e. A) -> U.A = B)
Theorem	unissb 2595	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 2596	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 2663 for a generalization to indexed unions.
|- (A.x e. A E.y e. B x (_ y -> U.A (_ U.B)
Theorem	unidif 2597	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	ssunieq 2598	Relationship implying union.
|- ((A e. B /\ A.x e. B x (_ A) -> A = U.B)
Theorem	unimax 2599	Any member of a class is the largest of those members that it includes.
|- (A e. B -> U.{x e. B | x (_ A} = A)
The intersection of a class
Syntax	cint 2600	Extend class notation to include the intersection of a class (read: 'intersect A ').
class |^|A