Home New Foundations ExplorerTheorem List (p. 40 of 64) < Previous  Next > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  NFE Home Page  >  Theorem List Contents       This page: Page List

Theorem List for New Foundations Explorer - 3901-4000   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremunieqi 3901 Inference of equality of two class unions. (Contributed by NM, 30-Aug-1993.)
A = B       A = B

Theoremunieqd 3902 Deduction of equality of two class unions. (Contributed by NM, 21-Apr-1995.)
(φA = B)       (φA = B)

Theoremeluniab 3903* Membership in union of a class abstraction. (Contributed by NM, 11-Aug-1994.) (Revised by Mario Carneiro, 14-Nov-2016.)
(A {x φ} ↔ x(A x φ))

Theoremelunirab 3904* Membership in union of a class abstraction. (Contributed by NM, 4-Oct-2006.)
(A {x B φ} ↔ x B (A x φ))

Theoremunipr 3905 The union of a pair is the union of its members. Proposition 5.7 of [TakeutiZaring] p. 16. (Contributed by NM, 23-Aug-1993.)
A V    &   B V       {A, B} = (AB)

Theoremuniprg 3906 The union of a pair is the union of its members. Proposition 5.7 of [TakeutiZaring] p. 16. (Contributed by NM, 25-Aug-2006.)
((A V B W) → {A, B} = (AB))

Theoremunisn 3907 A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53. (Contributed by NM, 30-Aug-1993.)
A V       {A} = A

Theoremunisng 3908 A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53. (Contributed by NM, 13-Aug-2002.)
(A V{A} = A)

Theoremdfnfc2 3909* An alternative statement of the effective freeness of a class A, when it is a set. (Contributed by Mario Carneiro, 14-Oct-2016.)
(x A V → (xAyx y = A))

Theoremuniun 3910 The class union of the union of two classes. Theorem 8.3 of [Quine] p. 53. (Contributed by NM, 20-Aug-1993.)
(AB) = (AB)

Theoremuniin 3911 The class union of the intersection of two classes. Exercise 4.12(n) of [Mendelson] p. 235. See uniinqs in set.mm for a condition where equality holds. (Contributed by NM, 4-Dec-2003.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
(AB) (AB)

Theoremuniss 3912 Subclass relationship for class union. Theorem 61 of [Suppes] p. 39. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
(A BA B)

Theoremssuni 3913 Subclass relationship for class union. (Contributed by NM, 24-May-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
((A B B C) → A C)

Theoremunissi 3914 Subclass relationship for subclass union. Inference form of uniss 3912. (Contributed by David Moews, 1-May-2017.)
A B       A B

Theoremunissd 3915 Subclass relationship for subclass union. Deduction form of uniss 3912. (Contributed by David Moews, 1-May-2017.)
(φA B)       (φA B)

Theoremuni0b 3916 The union of a set is empty iff the set is included in the singleton of the empty set. (Contributed by NM, 12-Sep-2004.)
(A = A {})

Theoremuni0c 3917* The union of a set is empty iff all of its members are empty. (Contributed by NM, 16-Aug-2006.)
(A = x A x = )

Theoremuni0 3918 The union of the empty set is the empty set. Theorem 8.7 of [Quine] p. 54. (Reproved without relying on ax-nul in set.mm by Eric Schmidt.) (Contributed by NM, 16-Sep-1993.) (Revised by Eric Schmidt, 4-Apr-2007.)
=

Theoremelssuni 3919 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. (Contributed by NM, 6-Jun-1994.)
(A BA B)

Theoremunissel 3920 Condition turning a subclass relationship for union into an equality. (Contributed by NM, 18-Jul-2006.)
((A B B A) → A = B)

Theoremunissb 3921* Relationship involving membership, subset, and union. Exercise 5 of [Enderton] p. 26 and its converse. (Contributed by NM, 20-Sep-2003.)
(A Bx A x B)

Theoremuniss2 3922* 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 4011 for a generalization to indexed unions. (Contributed by NM, 22-Mar-2004.)
(x A y B x yA B)

Theoremunidif 3923* If the difference A B contains the largest members of A, then the union of the difference is the union of A. (Contributed by NM, 22-Mar-2004.)
(x A y (A B)x y(A B) = A)

Theoremssunieq 3924* Relationship implying union. (Contributed by NM, 10-Nov-1999.)
((A B x B x A) → A = B)

Theoremunimax 3925* Any member of a class is the largest of those members that it includes. (Contributed by NM, 13-Aug-2002.)
(A B{x B x A} = A)

2.1.18  The intersection of a class

Syntaxcint 3926 Extend class notation to include the intersection of a class (read: 'intersect A').
class A

Definitiondf-int 3927* Define the intersection of a class. Definition 7.35 of [TakeutiZaring] p. 44. For example, {{ 1 , 3 }, { 1 , 8 }} = { 1 }. Compare this with the intersection of two classes, df-in 3213. (Contributed by NM, 18-Aug-1993.)
A = {x y(y Ax y)}

Theoremdfint2 3928* Alternate definition of class intersection. (Contributed by NM, 28-Jun-1998.)
A = {x y A x y}

Theoreminteq 3929 Equality law for intersection. (Contributed by NM, 13-Sep-1999.)
(A = BA = B)

Theoreminteqi 3930 Equality inference for class intersection. (Contributed by NM, 2-Sep-2003.)
A = B       A = B

Theoreminteqd 3931 Equality deduction for class intersection. (Contributed by NM, 2-Sep-2003.)
(φA = B)       (φA = B)

Theoremelint 3932* Membership in class intersection. (Contributed by NM, 21-May-1994.)
A V       (A Bx(x BA x))

Theoremelint2 3933* Membership in class intersection. (Contributed by NM, 14-Oct-1999.)
A V       (A Bx B A x)

Theoremelintg 3934* Membership in class intersection, with the sethood requirement expressed as an antecedent. (Contributed by NM, 20-Nov-2003.)
(A V → (A Bx B A x))

Theoremelinti 3935 Membership in class intersection. (Contributed by NM, 14-Oct-1999.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
(A B → (C BA C))

Theoremnfint 3936 Bound-variable hypothesis builder for intersection. (Contributed by NM, 2-Feb-1997.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
xA       xA

Theoremelintab 3937* Membership in the intersection of a class abstraction. (Contributed by NM, 30-Aug-1993.)
A V       (A {x φ} ↔ x(φA x))

Theoremelintrab 3938* Membership in the intersection of a class abstraction. (Contributed by NM, 17-Oct-1999.)
A V       (A {x B φ} ↔ x B (φA x))

Theoremelintrabg 3939* Membership in the intersection of a class abstraction. (Contributed by NM, 17-Feb-2007.)
(A V → (A {x B φ} ↔ x B (φA x)))

Theoremint0 3940 The intersection of the empty set is the universal class. Exercise 2 of [TakeutiZaring] p. 44. (Contributed by NM, 18-Aug-1993.)
= V

Theoremintss1 3941 An element of a class includes the intersection of the class. Exercise 4 of [TakeutiZaring] p. 44 (with correction), generalized to classes. (Contributed by NM, 18-Nov-1995.)
(A BB A)

Theoremssint 3942* Subclass of a class intersection. Theorem 5.11(viii) of [Monk1] p. 52 and its converse. (Contributed by NM, 14-Oct-1999.)
(A Bx B A x)

Theoremssintab 3943* Subclass of the intersection of a class abstraction. (Contributed by NM, 31-Jul-2006.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
(A {x φ} ↔ x(φA x))

Theoremssintub 3944* Subclass of the least upper bound. (Contributed by NM, 8-Aug-2000.)
A {x B A x}

Theoremssmin 3945* Subclass of the minimum value of class of supersets. (Contributed by NM, 10-Aug-2006.)
A {x (A x φ)}

Theoremintmin 3946* Any member of a class is the smallest of those members that include it. (Contributed by NM, 13-Aug-2002.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
(A B{x B A x} = A)

Theoremintss 3947 Intersection of subclasses. (Contributed by NM, 14-Oct-1999.)
(A BB A)

Theoremintssuni 3948 The intersection of a nonempty set is a subclass of its union. (Contributed by NM, 29-Jul-2006.)
(AA A)

Theoremssintrab 3949* Subclass of the intersection of a restricted class builder. (Contributed by NM, 30-Jan-2015.)
(A {x B φ} ↔ x B (φA x))

Theoremunissint 3950 If the union of a class is included in its intersection, the class is either the empty set or a singleton (uniintsn 3963). (Contributed by NM, 30-Oct-2010.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
(A A ↔ (A = A = A))

Theoremintssuni2 3951 Subclass relationship for intersection and union. (Contributed by NM, 29-Jul-2006.)
((A B A) → A B)

Theoremintminss 3952* Under subset ordering, the intersection of a restricted class abstraction is less than or equal to any of its members. (Contributed by NM, 7-Sep-2013.)
(x = A → (φψ))       ((A B ψ) → {x B φ} A)

Theoremintmin2 3953* Any set is the smallest of all sets that include it. (Contributed by NM, 20-Sep-2003.)
A V       {x A x} = A

Theoremintmin3 3954* Under subset ordering, the intersection of a class abstraction is less than or equal to any of its members. (Contributed by NM, 3-Jul-2005.)
(x = A → (φψ))    &   ψ       (A V{x φ} A)

Theoremintmin4 3955* Elimination of a conjunct in a class intersection. (Contributed by NM, 31-Jul-2006.)
(A {x φ} → {x (A x φ)} = {x φ})

Theoremintab 3956* The intersection of a special case of a class abstraction. y may be free in φ and A, which can be thought of a φ(y) and A(y). Typically, abrexex2 in set.mm or abexssex in set.mm can be used to satisfy the second hypothesis. (Contributed by NM, 28-Jul-2006.) (Proof shortened by Mario Carneiro, 14-Nov-2016.)
A V    &   {x y(φ x = A)} V       {x y(φA x)} = {x y(φ x = A)}

Theoremint0el 3957 The intersection of a class containing the empty set is empty. (Contributed by NM, 24-Apr-2004.)
( AA = )

Theoremintun 3958 The class intersection of the union of two classes. Theorem 78 of [Suppes] p. 42. (Contributed by NM, 22-Sep-2002.)
(AB) = (AB)

Theoremintpr 3959 The intersection of a pair is the intersection of its members. Theorem 71 of [Suppes] p. 42. (Contributed by NM, 14-Oct-1999.)
A V    &   B V       {A, B} = (AB)

Theoremintprg 3960 The intersection of a pair is the intersection of its members. Closed form of intpr 3959. Theorem 71 of [Suppes] p. 42. (Contributed by FL, 27-Apr-2008.)
((A V B W) → {A, B} = (AB))

Theoremintsng 3961 Intersection of a singleton. (Contributed by Stefan O'Rear, 22-Feb-2015.)
(A V{A} = A)

Theoremintsn 3962 The intersection of a singleton is its member. Theorem 70 of [Suppes] p. 41. (Contributed by NM, 29-Sep-2002.)
A V       {A} = A

Theoremuniintsn 3963* Two ways to express "A is a singleton." See also en1 in set.mm, en1b in set.mm, card1 in set.mm, and eusn 3796. (Contributed by NM, 2-Aug-2010.)
(A = Ax A = {x})

Theoremuniintab 3964 The union and the intersection of a class abstraction are equal exactly when there is a unique satisfying value of φ(x). (Contributed by Mario Carneiro, 24-Dec-2016.)
(∃!xφ{x φ} = {x φ})

Theoremintunsn 3965 Theorem joining a singleton to an intersection. (Contributed by NM, 29-Sep-2002.)
B V       (A ∪ {B}) = (AB)

Theoremrint0 3966 Relative intersection of an empty set. (Contributed by Stefan O'Rear, 3-Apr-2015.)
(X = → (AX) = A)

Theoremelrint 3967* Membership in a restricted intersection. (Contributed by Stefan O'Rear, 3-Apr-2015.)
(X (AB) ↔ (X A y B X y))

Theoremelrint2 3968* Membership in a restricted intersection. (Contributed by Stefan O'Rear, 3-Apr-2015.)
(X A → (X (AB) ↔ y B X y))

2.1.19  Indexed union and intersection

Syntaxciun 3969 Extend class notation to include indexed union. Note: Historically (prior to 21-Oct-2005), set.mm used the notation x AB, with the same union symbol as cuni 3891. While that syntax was unambiguous, it did not allow for LALR parsing of the syntax constructions in set.mm. The new syntax uses as distinguished symbol instead of and does allow LALR parsing. Thanks to Peter Backes for suggesting this change.
class x A B

Syntaxciin 3970 Extend class notation to include indexed intersection. Note: Historically (prior to 21-Oct-2005), set.mm used the notation x AB, with the same intersection symbol as cint 3926. Although that syntax was unambiguous, it did not allow for LALR parsing of the syntax constructions in set.mm. The new syntax uses a distinguished symbol instead of and does allow LALR parsing. Thanks to Peter Backes for suggesting this change.
class x A B

Definitiondf-iun 3971* Define indexed union. Definition indexed union in [Stoll] p. 45. In most applications, A is independent of x (although this is not required by the definition), and B depends on x i.e. can be read informally as B(x). We call x the index, A the index set, and B the indexed set. In most books, x A is written as a subscript or underneath a union symbol . We use a special union symbol to make it easier to distinguish from plain class union. In many theorems, you will see that x and A are in the same distinct variable group (meaning A cannot depend on x) and that B and x do not share a distinct variable group (meaning that can be thought of as B(x) i.e. can be substituted with a class expression containing x). An alternate definition tying indexed union to ordinary union is dfiun2 4001. Theorem uniiun 4019 provides a definition of ordinary union in terms of indexed union. Theorems fniunfv 5466 and funiunfv 5467 are useful when B is a function. (Contributed by NM, 27-Jun-1998.)
x A B = {y x A y B}

Definitiondf-iin 3972* Define indexed intersection. Definition of [Stoll] p. 45. See the remarks for its sibling operation of indexed union df-iun 3971. An alternate definition tying indexed intersection to ordinary intersection is dfiin2 4002. Theorem intiin 4020 provides a definition of ordinary intersection in terms of indexed intersection. (Contributed by NM, 27-Jun-1998.)
x A B = {y x A y B}

Theoremeliun 3973* Membership in indexed union. (Contributed by NM, 3-Sep-2003.)
(A x B Cx B A C)

Theoremeliin 3974* Membership in indexed intersection. (Contributed by NM, 3-Sep-2003.)
(A V → (A x B Cx B A C))

Theoremiuncom 3975* Commutation of indexed unions. (Contributed by NM, 18-Dec-2008.)
x A y B C = y B x A C

Theoremiuncom4 3976 Commutation of union with indexed union. (Contributed by Mario Carneiro, 18-Jan-2014.)
x A B = x A B

Theoremiunconst 3977* Indexed union of a constant class, i.e. where B does not depend on x. (Contributed by NM, 5-Sep-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
(Ax A B = B)

Theoremiinconst 3978* Indexed intersection of a constant class, i.e. where B does not depend on x. (Contributed by Mario Carneiro, 6-Feb-2015.)
(Ax A B = B)

Theoremiuniin 3979* Law combining indexed union with indexed intersection. Eq. 14 in [KuratowskiMostowski] p. 109. This theorem also appears as the last example at http://en.wikipedia.org/wiki/Union%5F%28set%5Ftheory%29. (Contributed by NM, 17-Aug-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
x A y B C y B x A C

Theoremiunss1 3980* Subclass theorem for indexed union. (Contributed by NM, 10-Dec-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
(A Bx A C x B C)

Theoremiinss1 3981* Subclass theorem for indexed union. (Contributed by NM, 24-Jan-2012.)
(A Bx B C x A C)

Theoremiuneq1 3982* Equality theorem for indexed union. (Contributed by NM, 27-Jun-1998.)
(A = Bx A C = x B C)

Theoremiineq1 3983* Equality theorem for restricted existential quantifier. (Contributed by NM, 27-Jun-1998.)
(A = Bx A C = x B C)

Theoremss2iun 3984 Subclass theorem for indexed union. (Contributed by NM, 26-Nov-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
(x A B Cx A B x A C)

Theoremiuneq2 3985 Equality theorem for indexed union. (Contributed by NM, 22-Oct-2003.)
(x A B = Cx A B = x A C)

Theoremiineq2 3986 Equality theorem for indexed intersection. (Contributed by NM, 22-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
(x A B = Cx A B = x A C)

Theoremiuneq2i 3987 Equality inference for indexed union. (Contributed by NM, 22-Oct-2003.)
(x AB = C)       x A B = x A C

Theoremiineq2i 3988 Equality inference for indexed intersection. (Contributed by NM, 22-Oct-2003.)
(x AB = C)       x A B = x A C

Theoremiineq2d 3989 Equality deduction for indexed intersection. (Contributed by NM, 7-Dec-2011.)
xφ    &   ((φ x A) → B = C)       (φx A B = x A C)

Theoremiuneq2dv 3990* Equality deduction for indexed union. (Contributed by NM, 3-Aug-2004.)
((φ x A) → B = C)       (φx A B = x A C)

Theoremiineq2dv 3991* Equality deduction for indexed intersection. (Contributed by NM, 3-Aug-2004.)
((φ x A) → B = C)       (φx A B = x A C)

Theoremiuneq1d 3992* Equality theorem for indexed union, deduction version. (Contributed by Drahflow, 22-Oct-2015.)
(φA = B)       (φx A C = x B C)

Theoremiuneq12d 3993* Equality deduction for indexed union, deduction version. (Contributed by Drahflow, 22-Oct-2015.)
(φA = B)    &   (φC = D)       (φx A C = x B D)

Theoremiuneq2d 3994* Equality deduction for indexed union. (Contributed by Drahflow, 22-Oct-2015.)
(φB = C)       (φx A B = x A C)

Theoremnfiun 3995 Bound-variable hypothesis builder for indexed union. (Contributed by Mario Carneiro, 25-Jan-2014.)
yA    &   yB       yx A B

Theoremnfiin 3996 Bound-variable hypothesis builder for indexed intersection. (Contributed by Mario Carneiro, 25-Jan-2014.)
yA    &   yB       yx A B

Theoremnfiu1 3997 Bound-variable hypothesis builder for indexed union. (Contributed by NM, 12-Oct-2003.)
xx A B

Theoremnfii1 3998 Bound-variable hypothesis builder for indexed intersection. (Contributed by NM, 15-Oct-2003.)
xx A B

Theoremdfiun2g 3999* Alternate definition of indexed union when B is a set. Definition 15(a) of [Suppes] p. 44. (Contributed by NM, 23-Mar-2006.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
(x A B Cx A B = {y x A y = B})

Theoremdfiin2g 4000* Alternate definition of indexed intersection when B is a set. (Contributed by Jeff Hankins, 27-Aug-2009.)
(x A B Cx A B = {y x A y = B})

Page List
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-6337
 Copyright terms: Public domain < Previous  Next >