HomeHome Intuitionistic Logic Explorer
Theorem List (p. 39 of 154)
< Previous  Next >
Bad symbols? Try the
GIF version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 3801-3900   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremopeq12d 3801 Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐶 = 𝐷)       (𝜑 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐷⟩)
 
Theoremoteq1 3802 Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015.)
(𝐴 = 𝐵 → ⟨𝐴, 𝐶, 𝐷⟩ = ⟨𝐵, 𝐶, 𝐷⟩)
 
Theoremoteq2 3803 Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015.)
(𝐴 = 𝐵 → ⟨𝐶, 𝐴, 𝐷⟩ = ⟨𝐶, 𝐵, 𝐷⟩)
 
Theoremoteq3 3804 Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015.)
(𝐴 = 𝐵 → ⟨𝐶, 𝐷, 𝐴⟩ = ⟨𝐶, 𝐷, 𝐵⟩)
 
Theoremoteq1d 3805 Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.)
(𝜑𝐴 = 𝐵)       (𝜑 → ⟨𝐴, 𝐶, 𝐷⟩ = ⟨𝐵, 𝐶, 𝐷⟩)
 
Theoremoteq2d 3806 Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.)
(𝜑𝐴 = 𝐵)       (𝜑 → ⟨𝐶, 𝐴, 𝐷⟩ = ⟨𝐶, 𝐵, 𝐷⟩)
 
Theoremoteq3d 3807 Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.)
(𝜑𝐴 = 𝐵)       (𝜑 → ⟨𝐶, 𝐷, 𝐴⟩ = ⟨𝐶, 𝐷, 𝐵⟩)
 
Theoremoteq123d 3808 Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐶 = 𝐷)    &   (𝜑𝐸 = 𝐹)       (𝜑 → ⟨𝐴, 𝐶, 𝐸⟩ = ⟨𝐵, 𝐷, 𝐹⟩)
 
Theoremnfop 3809 Bound-variable hypothesis builder for ordered pairs. (Contributed by NM, 14-Nov-1995.)
𝑥𝐴    &   𝑥𝐵       𝑥𝐴, 𝐵
 
Theoremnfopd 3810 Deduction version of bound-variable hypothesis builder nfop 3809. This shows how the deduction version of a not-free theorem such as nfop 3809 can be created from the corresponding not-free inference theorem. (Contributed by NM, 4-Feb-2008.)
(𝜑𝑥𝐴)    &   (𝜑𝑥𝐵)       (𝜑𝑥𝐴, 𝐵⟩)
 
Theoremopid 3811 The ordered pair 𝐴, 𝐴 in Kuratowski's representation. (Contributed by FL, 28-Dec-2011.)
𝐴 ∈ V       𝐴, 𝐴⟩ = {{𝐴}}
 
Theoremralunsn 3812* Restricted quantification over the union of a set and a singleton, using implicit substitution. (Contributed by Paul Chapman, 17-Nov-2012.) (Revised by Mario Carneiro, 23-Apr-2015.)
(𝑥 = 𝐵 → (𝜑𝜓))       (𝐵𝐶 → (∀𝑥 ∈ (𝐴 ∪ {𝐵})𝜑 ↔ (∀𝑥𝐴 𝜑𝜓)))
 
Theorem2ralunsn 3813* Double restricted quantification over the union of a set and a singleton, using implicit substitution. (Contributed by Paul Chapman, 17-Nov-2012.)
(𝑥 = 𝐵 → (𝜑𝜒))    &   (𝑦 = 𝐵 → (𝜑𝜓))    &   (𝑥 = 𝐵 → (𝜓𝜃))       (𝐵𝐶 → (∀𝑥 ∈ (𝐴 ∪ {𝐵})∀𝑦 ∈ (𝐴 ∪ {𝐵})𝜑 ↔ ((∀𝑥𝐴𝑦𝐴 𝜑 ∧ ∀𝑥𝐴 𝜓) ∧ (∀𝑦𝐴 𝜒𝜃))))
 
Theoremopprc 3814 Expansion of an ordered pair when either member is a proper class. (Contributed by Mario Carneiro, 26-Apr-2015.)
(¬ (𝐴 ∈ V ∧ 𝐵 ∈ V) → ⟨𝐴, 𝐵⟩ = ∅)
 
Theoremopprc1 3815 Expansion of an ordered pair when the first member is a proper class. See also opprc 3814. (Contributed by NM, 10-Apr-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
𝐴 ∈ V → ⟨𝐴, 𝐵⟩ = ∅)
 
Theoremopprc2 3816 Expansion of an ordered pair when the second member is a proper class. See also opprc 3814. (Contributed by NM, 15-Nov-1994.) (Revised by Mario Carneiro, 26-Apr-2015.)
𝐵 ∈ V → ⟨𝐴, 𝐵⟩ = ∅)
 
Theoremoprcl 3817 If an ordered pair has an element, then its arguments are sets. (Contributed by Mario Carneiro, 26-Apr-2015.)
(𝐶 ∈ ⟨𝐴, 𝐵⟩ → (𝐴 ∈ V ∧ 𝐵 ∈ V))
 
Theorempwsnss 3818 The power set of a singleton. (Contributed by Jim Kingdon, 12-Aug-2018.)
{∅, {𝐴}} ⊆ 𝒫 {𝐴}
 
Theorempwpw0ss 3819 Compute the power set of the power set of the empty set. (See pw0 3754 for the power set of the empty set.) Theorem 90 of [Suppes] p. 48 (but with subset in place of equality). (Contributed by Jim Kingdon, 12-Aug-2018.)
{∅, {∅}} ⊆ 𝒫 {∅}
 
Theorempwprss 3820 The power set of an unordered pair. (Contributed by Jim Kingdon, 13-Aug-2018.)
({∅, {𝐴}} ∪ {{𝐵}, {𝐴, 𝐵}}) ⊆ 𝒫 {𝐴, 𝐵}
 
Theorempwtpss 3821 The power set of an unordered triple. (Contributed by Jim Kingdon, 13-Aug-2018.)
(({∅, {𝐴}} ∪ {{𝐵}, {𝐴, 𝐵}}) ∪ ({{𝐶}, {𝐴, 𝐶}} ∪ {{𝐵, 𝐶}, {𝐴, 𝐵, 𝐶}})) ⊆ 𝒫 {𝐴, 𝐵, 𝐶}
 
Theorempwpwpw0ss 3822 Compute the power set of the power set of the power set of the empty set. (See also pw0 3754 and pwpw0ss 3819.) (Contributed by Jim Kingdon, 13-Aug-2018.)
({∅, {∅}} ∪ {{{∅}}, {∅, {∅}}}) ⊆ 𝒫 {∅, {∅}}
 
Theorempwv 3823 The power class of the universe is the universe. Exercise 4.12(d) of [Mendelson] p. 235. (Contributed by NM, 14-Sep-2003.)
𝒫 V = V
 
2.1.18  The union of a class
 
Syntaxcuni 3824 Extend class notation to include the union of a class. Read: "union (of) 𝐴".
class 𝐴
 
Definitiondf-uni 3825* 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. For example, {{1, 3}, {1, 8}} = {1, 3, 8}. This is similar to the union of two classes df-un 3148. (Contributed by NM, 23-Aug-1993.)
𝐴 = {𝑥 ∣ ∃𝑦(𝑥𝑦𝑦𝐴)}
 
Theoremdfuni2 3826* Alternate definition of class union. (Contributed by NM, 28-Jun-1998.)
𝐴 = {𝑥 ∣ ∃𝑦𝐴 𝑥𝑦}
 
Theoremeluni 3827* Membership in class union. (Contributed by NM, 22-May-1994.)
(𝐴 𝐵 ↔ ∃𝑥(𝐴𝑥𝑥𝐵))
 
Theoremeluni2 3828* Membership in class union. Restricted quantifier version. (Contributed by NM, 31-Aug-1999.)
(𝐴 𝐵 ↔ ∃𝑥𝐵 𝐴𝑥)
 
Theoremelunii 3829 Membership in class union. (Contributed by NM, 24-Mar-1995.)
((𝐴𝐵𝐵𝐶) → 𝐴 𝐶)
 
Theoremnfuni 3830 Bound-variable hypothesis builder for union. (Contributed by NM, 30-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
𝑥𝐴       𝑥 𝐴
 
Theoremnfunid 3831 Deduction version of nfuni 3830. (Contributed by NM, 18-Feb-2013.)
(𝜑𝑥𝐴)       (𝜑𝑥 𝐴)
 
Theoremcsbunig 3832 Distribute proper substitution through the union of a class. (Contributed by Alan Sare, 10-Nov-2012.)
(𝐴𝑉𝐴 / 𝑥 𝐵 = 𝐴 / 𝑥𝐵)
 
Theoremunieq 3833 Equality theorem for class union. Exercise 15 of [TakeutiZaring] p. 18. (Contributed by NM, 10-Aug-1993.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
(𝐴 = 𝐵 𝐴 = 𝐵)
 
Theoremunieqi 3834 Inference of equality of two class unions. (Contributed by NM, 30-Aug-1993.)
𝐴 = 𝐵        𝐴 = 𝐵
 
Theoremunieqd 3835 Deduction of equality of two class unions. (Contributed by NM, 21-Apr-1995.)
(𝜑𝐴 = 𝐵)       (𝜑 𝐴 = 𝐵)
 
Theoremeluniab 3836* Membership in union of a class abstraction. (Contributed by NM, 11-Aug-1994.) (Revised by Mario Carneiro, 14-Nov-2016.)
(𝐴 {𝑥𝜑} ↔ ∃𝑥(𝐴𝑥𝜑))
 
Theoremelunirab 3837* Membership in union of a class abstraction. (Contributed by NM, 4-Oct-2006.)
(𝐴 {𝑥𝐵𝜑} ↔ ∃𝑥𝐵 (𝐴𝑥𝜑))
 
Theoremunipr 3838 The union of a pair is the union of its members. Proposition 5.7 of [TakeutiZaring] p. 16. (Contributed by NM, 23-Aug-1993.)
𝐴 ∈ V    &   𝐵 ∈ V        {𝐴, 𝐵} = (𝐴𝐵)
 
Theoremuniprg 3839 The union of a pair is the union of its members. Proposition 5.7 of [TakeutiZaring] p. 16. (Contributed by NM, 25-Aug-2006.)
((𝐴𝑉𝐵𝑊) → {𝐴, 𝐵} = (𝐴𝐵))
 
Theoremunisn 3840 A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53. (Contributed by NM, 30-Aug-1993.)
𝐴 ∈ V        {𝐴} = 𝐴
 
Theoremunisng 3841 A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53. (Contributed by NM, 13-Aug-2002.)
(𝐴𝑉 {𝐴} = 𝐴)
 
Theoremdfnfc2 3842* An alternate statement of the effective freeness of a class 𝐴, when it is a set. (Contributed by Mario Carneiro, 14-Oct-2016.)
(∀𝑥 𝐴𝑉 → (𝑥𝐴 ↔ ∀𝑦𝑥 𝑦 = 𝐴))
 
Theoremuniun 3843 The class union of the union of two classes. Theorem 8.3 of [Quine] p. 53. (Contributed by NM, 20-Aug-1993.)
(𝐴𝐵) = ( 𝐴 𝐵)
 
Theoremuniin 3844 The class union of the intersection of two classes. Exercise 4.12(n) of [Mendelson] p. 235. (Contributed by NM, 4-Dec-2003.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
(𝐴𝐵) ⊆ ( 𝐴 𝐵)
 
Theoremuniss 3845 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.)
(𝐴𝐵 𝐴 𝐵)
 
Theoremssuni 3846 Subclass relationship for class union. (Contributed by NM, 24-May-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
((𝐴𝐵𝐵𝐶) → 𝐴 𝐶)
 
Theoremunissi 3847 Subclass relationship for subclass union. Inference form of uniss 3845. (Contributed by David Moews, 1-May-2017.)
𝐴𝐵        𝐴 𝐵
 
Theoremunissd 3848 Subclass relationship for subclass union. Deduction form of uniss 3845. (Contributed by David Moews, 1-May-2017.)
(𝜑𝐴𝐵)       (𝜑 𝐴 𝐵)
 
Theoremuni0b 3849 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.)
( 𝐴 = ∅ ↔ 𝐴 ⊆ {∅})
 
Theoremuni0c 3850* The union of a set is empty iff all of its members are empty. (Contributed by NM, 16-Aug-2006.)
( 𝐴 = ∅ ↔ ∀𝑥𝐴 𝑥 = ∅)
 
Theoremuni0 3851 The union of the empty set is the empty set. Theorem 8.7 of [Quine] p. 54. (Reproved without relying on ax-nul by Eric Schmidt.) (Contributed by NM, 16-Sep-1993.) (Revised by Eric Schmidt, 4-Apr-2007.)
∅ = ∅
 
Theoremelssuni 3852 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.)
(𝐴𝐵𝐴 𝐵)
 
Theoremunissel 3853 Condition turning a subclass relationship for union into an equality. (Contributed by NM, 18-Jul-2006.)
(( 𝐴𝐵𝐵𝐴) → 𝐴 = 𝐵)
 
Theoremunissb 3854* Relationship involving membership, subset, and union. Exercise 5 of [Enderton] p. 26 and its converse. (Contributed by NM, 20-Sep-2003.)
( 𝐴𝐵 ↔ ∀𝑥𝐴 𝑥𝐵)
 
Theoremuniss2 3855* A subclass condition on the members of two classes that implies a subclass relation on their unions. Proposition 8.6 of [TakeutiZaring] p. 59. (Contributed by NM, 22-Mar-2004.)
(∀𝑥𝐴𝑦𝐵 𝑥𝑦 𝐴 𝐵)
 
Theoremunidif 3856* If the difference 𝐴𝐵 contains the largest members of 𝐴, then the union of the difference is the union of 𝐴. (Contributed by NM, 22-Mar-2004.)
(∀𝑥𝐴𝑦 ∈ (𝐴𝐵)𝑥𝑦 (𝐴𝐵) = 𝐴)
 
Theoremssunieq 3857* Relationship implying union. (Contributed by NM, 10-Nov-1999.)
((𝐴𝐵 ∧ ∀𝑥𝐵 𝑥𝐴) → 𝐴 = 𝐵)
 
Theoremunimax 3858* Any member of a class is the largest of those members that it includes. (Contributed by NM, 13-Aug-2002.)
(𝐴𝐵 {𝑥𝐵𝑥𝐴} = 𝐴)
 
2.1.19  The intersection of a class
 
Syntaxcint 3859 Extend class notation to include the intersection of a class. Read: "intersection (of) 𝐴".
class 𝐴
 
Definitiondf-int 3860* 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 3150. (Contributed by NM, 18-Aug-1993.)
𝐴 = {𝑥 ∣ ∀𝑦(𝑦𝐴𝑥𝑦)}
 
Theoremdfint2 3861* Alternate definition of class intersection. (Contributed by NM, 28-Jun-1998.)
𝐴 = {𝑥 ∣ ∀𝑦𝐴 𝑥𝑦}
 
Theoreminteq 3862 Equality law for intersection. (Contributed by NM, 13-Sep-1999.)
(𝐴 = 𝐵 𝐴 = 𝐵)
 
Theoreminteqi 3863 Equality inference for class intersection. (Contributed by NM, 2-Sep-2003.)
𝐴 = 𝐵        𝐴 = 𝐵
 
Theoreminteqd 3864 Equality deduction for class intersection. (Contributed by NM, 2-Sep-2003.)
(𝜑𝐴 = 𝐵)       (𝜑 𝐴 = 𝐵)
 
Theoremelint 3865* Membership in class intersection. (Contributed by NM, 21-May-1994.)
𝐴 ∈ V       (𝐴 𝐵 ↔ ∀𝑥(𝑥𝐵𝐴𝑥))
 
Theoremelint2 3866* Membership in class intersection. (Contributed by NM, 14-Oct-1999.)
𝐴 ∈ V       (𝐴 𝐵 ↔ ∀𝑥𝐵 𝐴𝑥)
 
Theoremelintg 3867* Membership in class intersection, with the sethood requirement expressed as an antecedent. (Contributed by NM, 20-Nov-2003.)
(𝐴𝑉 → (𝐴 𝐵 ↔ ∀𝑥𝐵 𝐴𝑥))
 
Theoremelinti 3868 Membership in class intersection. (Contributed by NM, 14-Oct-1999.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
(𝐴 𝐵 → (𝐶𝐵𝐴𝐶))
 
Theoremnfint 3869 Bound-variable hypothesis builder for intersection. (Contributed by NM, 2-Feb-1997.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
𝑥𝐴       𝑥 𝐴
 
Theoremelintab 3870* Membership in the intersection of a class abstraction. (Contributed by NM, 30-Aug-1993.)
𝐴 ∈ V       (𝐴 {𝑥𝜑} ↔ ∀𝑥(𝜑𝐴𝑥))
 
Theoremelintrab 3871* Membership in the intersection of a class abstraction. (Contributed by NM, 17-Oct-1999.)
𝐴 ∈ V       (𝐴 {𝑥𝐵𝜑} ↔ ∀𝑥𝐵 (𝜑𝐴𝑥))
 
Theoremelintrabg 3872* Membership in the intersection of a class abstraction. (Contributed by NM, 17-Feb-2007.)
(𝐴𝑉 → (𝐴 {𝑥𝐵𝜑} ↔ ∀𝑥𝐵 (𝜑𝐴𝑥)))
 
Theoremint0 3873 The intersection of the empty set is the universal class. Exercise 2 of [TakeutiZaring] p. 44. (Contributed by NM, 18-Aug-1993.)
∅ = V
 
Theoremintss1 3874 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.)
(𝐴𝐵 𝐵𝐴)
 
Theoremssint 3875* Subclass of a class intersection. Theorem 5.11(viii) of [Monk1] p. 52 and its converse. (Contributed by NM, 14-Oct-1999.)
(𝐴 𝐵 ↔ ∀𝑥𝐵 𝐴𝑥)
 
Theoremssintab 3876* Subclass of the intersection of a class abstraction. (Contributed by NM, 31-Jul-2006.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
(𝐴 {𝑥𝜑} ↔ ∀𝑥(𝜑𝐴𝑥))
 
Theoremssintub 3877* Subclass of the least upper bound. (Contributed by NM, 8-Aug-2000.)
𝐴 {𝑥𝐵𝐴𝑥}
 
Theoremssmin 3878* Subclass of the minimum value of class of supersets. (Contributed by NM, 10-Aug-2006.)
𝐴 {𝑥 ∣ (𝐴𝑥𝜑)}
 
Theoremintmin 3879* 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.)
(𝐴𝐵 {𝑥𝐵𝐴𝑥} = 𝐴)
 
Theoremintss 3880 Intersection of subclasses. (Contributed by NM, 14-Oct-1999.)
(𝐴𝐵 𝐵 𝐴)
 
Theoremintssunim 3881* The intersection of an inhabited set is a subclass of its union. (Contributed by NM, 29-Jul-2006.)
(∃𝑥 𝑥𝐴 𝐴 𝐴)
 
Theoremssintrab 3882* Subclass of the intersection of a restricted class builder. (Contributed by NM, 30-Jan-2015.)
(𝐴 {𝑥𝐵𝜑} ↔ ∀𝑥𝐵 (𝜑𝐴𝑥))
 
Theoremintssuni2m 3883* Subclass relationship for intersection and union. (Contributed by Jim Kingdon, 14-Aug-2018.)
((𝐴𝐵 ∧ ∃𝑥 𝑥𝐴) → 𝐴 𝐵)
 
Theoremintminss 3884* 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.)
(𝑥 = 𝐴 → (𝜑𝜓))       ((𝐴𝐵𝜓) → {𝑥𝐵𝜑} ⊆ 𝐴)
 
Theoremintmin2 3885* Any set is the smallest of all sets that include it. (Contributed by NM, 20-Sep-2003.)
𝐴 ∈ V        {𝑥𝐴𝑥} = 𝐴
 
Theoremintmin3 3886* 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.)
(𝑥 = 𝐴 → (𝜑𝜓))    &   𝜓       (𝐴𝑉 {𝑥𝜑} ⊆ 𝐴)
 
Theoremintmin4 3887* Elimination of a conjunct in a class intersection. (Contributed by NM, 31-Jul-2006.)
(𝐴 {𝑥𝜑} → {𝑥 ∣ (𝐴𝑥𝜑)} = {𝑥𝜑})
 
Theoremintab 3888* The intersection of a special case of a class abstraction. 𝑦 may be free in 𝜑 and 𝐴, which can be thought of a 𝜑(𝑦) and 𝐴(𝑦). (Contributed by NM, 28-Jul-2006.) (Proof shortened by Mario Carneiro, 14-Nov-2016.)
𝐴 ∈ V    &   {𝑥 ∣ ∃𝑦(𝜑𝑥 = 𝐴)} ∈ V        {𝑥 ∣ ∀𝑦(𝜑𝐴𝑥)} = {𝑥 ∣ ∃𝑦(𝜑𝑥 = 𝐴)}
 
Theoremint0el 3889 The intersection of a class containing the empty set is empty. (Contributed by NM, 24-Apr-2004.)
(∅ ∈ 𝐴 𝐴 = ∅)
 
Theoremintun 3890 The class intersection of the union of two classes. Theorem 78 of [Suppes] p. 42. (Contributed by NM, 22-Sep-2002.)
(𝐴𝐵) = ( 𝐴 𝐵)
 
Theoremintpr 3891 The intersection of a pair is the intersection of its members. Theorem 71 of [Suppes] p. 42. (Contributed by NM, 14-Oct-1999.)
𝐴 ∈ V    &   𝐵 ∈ V        {𝐴, 𝐵} = (𝐴𝐵)
 
Theoremintprg 3892 The intersection of a pair is the intersection of its members. Closed form of intpr 3891. Theorem 71 of [Suppes] p. 42. (Contributed by FL, 27-Apr-2008.)
((𝐴𝑉𝐵𝑊) → {𝐴, 𝐵} = (𝐴𝐵))
 
Theoremintsng 3893 Intersection of a singleton. (Contributed by Stefan O'Rear, 22-Feb-2015.)
(𝐴𝑉 {𝐴} = 𝐴)
 
Theoremintsn 3894 The intersection of a singleton is its member. Theorem 70 of [Suppes] p. 41. (Contributed by NM, 29-Sep-2002.)
𝐴 ∈ V        {𝐴} = 𝐴
 
Theoremuniintsnr 3895* The union and intersection of a singleton are equal. See also eusn 3681. (Contributed by Jim Kingdon, 14-Aug-2018.)
(∃𝑥 𝐴 = {𝑥} → 𝐴 = 𝐴)
 
Theoremuniintabim 3896 The union and the intersection of a class abstraction are equal if there is a unique satisfying value of 𝜑(𝑥). (Contributed by Jim Kingdon, 14-Aug-2018.)
(∃!𝑥𝜑 {𝑥𝜑} = {𝑥𝜑})
 
Theoremintunsn 3897 Theorem joining a singleton to an intersection. (Contributed by NM, 29-Sep-2002.)
𝐵 ∈ V        (𝐴 ∪ {𝐵}) = ( 𝐴𝐵)
 
Theoremrint0 3898 Relative intersection of an empty set. (Contributed by Stefan O'Rear, 3-Apr-2015.)
(𝑋 = ∅ → (𝐴 𝑋) = 𝐴)
 
Theoremelrint 3899* Membership in a restricted intersection. (Contributed by Stefan O'Rear, 3-Apr-2015.)
(𝑋 ∈ (𝐴 𝐵) ↔ (𝑋𝐴 ∧ ∀𝑦𝐵 𝑋𝑦))
 
Theoremelrint2 3900* Membership in a restricted intersection. (Contributed by Stefan O'Rear, 3-Apr-2015.)
(𝑋𝐴 → (𝑋 ∈ (𝐴 𝐵) ↔ ∀𝑦𝐵 𝑋𝑦))
    < Previous  Next >

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-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-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15300 154 15301-15311
  Copyright terms: Public domain < Previous  Next >