![]() |
Metamath
Proof Explorer Theorem List (p. 51 of 479) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-iin 5001* | Define indexed intersection. Definition of [Stoll] p. 45. See the remarks for its sibling operation of indexed union df-iun 5000. An alternate definition tying indexed intersection to ordinary intersection is dfiin2 5038. Theorem intiin 5063 provides a definition of ordinary intersection in terms of indexed intersection. (Contributed by NM, 27-Jun-1998.) |
β’ β© π₯ β π΄ π΅ = {π¦ β£ βπ₯ β π΄ π¦ β π΅} | ||
Theorem | eliun 5002* | Membership in indexed union. (Contributed by NM, 3-Sep-2003.) |
β’ (π΄ β βͺ π₯ β π΅ πΆ β βπ₯ β π΅ π΄ β πΆ) | ||
Theorem | eliin 5003* | Membership in indexed intersection. (Contributed by NM, 3-Sep-2003.) |
β’ (π΄ β π β (π΄ β β© π₯ β π΅ πΆ β βπ₯ β π΅ π΄ β πΆ)) | ||
Theorem | eliuni 5004* | Membership in an indexed union, one way. (Contributed by JJ, 27-Jul-2021.) |
β’ (π₯ = π΄ β π΅ = πΆ) β β’ ((π΄ β π· β§ πΈ β πΆ) β πΈ β βͺ π₯ β π· π΅) | ||
Theorem | iuncom 5005* | Commutation of indexed unions. (Contributed by NM, 18-Dec-2008.) |
β’ βͺ π₯ β π΄ βͺ π¦ β π΅ πΆ = βͺ π¦ β π΅ βͺ π₯ β π΄ πΆ | ||
Theorem | iuncom4 5006 | Commutation of union with indexed union. (Contributed by Mario Carneiro, 18-Jan-2014.) |
β’ βͺ π₯ β π΄ βͺ π΅ = βͺ βͺ π₯ β π΄ π΅ | ||
Theorem | iunconst 5007* | Indexed union of a constant class, i.e. where π΅ does not depend on π₯. (Contributed by NM, 5-Sep-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
β’ (π΄ β β β βͺ π₯ β π΄ π΅ = π΅) | ||
Theorem | iinconst 5008* | Indexed intersection of a constant class, i.e. where π΅ does not depend on π₯. (Contributed by Mario Carneiro, 6-Feb-2015.) |
β’ (π΄ β β β β© π₯ β π΄ π΅ = π΅) | ||
Theorem | iuneqconst 5009* | Indexed union of identical classes. (Contributed by AV, 5-Mar-2024.) |
β’ (π₯ = π β π΅ = πΆ) β β’ ((π β π΄ β§ βπ₯ β π΄ π΅ = πΆ) β βͺ π₯ β π΄ π΅ = πΆ) | ||
Theorem | iuniin 5010* | 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.) |
β’ βͺ π₯ β π΄ β© π¦ β π΅ πΆ β β© π¦ β π΅ βͺ π₯ β π΄ πΆ | ||
Theorem | iinssiun 5011* | An indexed intersection is a subset of the corresponding indexed union. (Contributed by Thierry Arnoux, 31-Dec-2021.) |
β’ (π΄ β β β β© π₯ β π΄ π΅ β βͺ π₯ β π΄ π΅) | ||
Theorem | iunss1 5012* | Subclass theorem for indexed union. (Contributed by NM, 10-Dec-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
β’ (π΄ β π΅ β βͺ π₯ β π΄ πΆ β βͺ π₯ β π΅ πΆ) | ||
Theorem | iinss1 5013* | Subclass theorem for indexed intersection. (Contributed by NM, 24-Jan-2012.) |
β’ (π΄ β π΅ β β© π₯ β π΅ πΆ β β© π₯ β π΄ πΆ) | ||
Theorem | iuneq1 5014* | Equality theorem for indexed union. (Contributed by NM, 27-Jun-1998.) |
β’ (π΄ = π΅ β βͺ π₯ β π΄ πΆ = βͺ π₯ β π΅ πΆ) | ||
Theorem | iineq1 5015* | Equality theorem for indexed intersection. (Contributed by NM, 27-Jun-1998.) |
β’ (π΄ = π΅ β β© π₯ β π΄ πΆ = β© π₯ β π΅ πΆ) | ||
Theorem | ss2iun 5016 | Subclass theorem for indexed union. (Contributed by NM, 26-Nov-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
β’ (βπ₯ β π΄ π΅ β πΆ β βͺ π₯ β π΄ π΅ β βͺ π₯ β π΄ πΆ) | ||
Theorem | iuneq2 5017 | Equality theorem for indexed union. (Contributed by NM, 22-Oct-2003.) |
β’ (βπ₯ β π΄ π΅ = πΆ β βͺ π₯ β π΄ π΅ = βͺ π₯ β π΄ πΆ) | ||
Theorem | iineq2 5018 | Equality theorem for indexed intersection. (Contributed by NM, 22-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
β’ (βπ₯ β π΄ π΅ = πΆ β β© π₯ β π΄ π΅ = β© π₯ β π΄ πΆ) | ||
Theorem | iuneq2i 5019 | Equality inference for indexed union. (Contributed by NM, 22-Oct-2003.) |
β’ (π₯ β π΄ β π΅ = πΆ) β β’ βͺ π₯ β π΄ π΅ = βͺ π₯ β π΄ πΆ | ||
Theorem | iineq2i 5020 | Equality inference for indexed intersection. (Contributed by NM, 22-Oct-2003.) |
β’ (π₯ β π΄ β π΅ = πΆ) β β’ β© π₯ β π΄ π΅ = β© π₯ β π΄ πΆ | ||
Theorem | iineq2d 5021 | Equality deduction for indexed intersection. (Contributed by NM, 7-Dec-2011.) |
β’ β²π₯π & β’ ((π β§ π₯ β π΄) β π΅ = πΆ) β β’ (π β β© π₯ β π΄ π΅ = β© π₯ β π΄ πΆ) | ||
Theorem | iuneq2dv 5022* | Equality deduction for indexed union. (Contributed by NM, 3-Aug-2004.) |
β’ ((π β§ π₯ β π΄) β π΅ = πΆ) β β’ (π β βͺ π₯ β π΄ π΅ = βͺ π₯ β π΄ πΆ) | ||
Theorem | iineq2dv 5023* | Equality deduction for indexed intersection. (Contributed by NM, 3-Aug-2004.) |
β’ ((π β§ π₯ β π΄) β π΅ = πΆ) β β’ (π β β© π₯ β π΄ π΅ = β© π₯ β π΄ πΆ) | ||
Theorem | iuneq12df 5024 | Equality deduction for indexed union, deduction version. (Contributed by Thierry Arnoux, 31-Dec-2016.) |
β’ β²π₯π & β’ β²π₯π΄ & β’ β²π₯π΅ & β’ (π β π΄ = π΅) & β’ (π β πΆ = π·) β β’ (π β βͺ π₯ β π΄ πΆ = βͺ π₯ β π΅ π·) | ||
Theorem | iuneq1d 5025* | Equality theorem for indexed union, deduction version. (Contributed by Drahflow, 22-Oct-2015.) |
β’ (π β π΄ = π΅) β β’ (π β βͺ π₯ β π΄ πΆ = βͺ π₯ β π΅ πΆ) | ||
Theorem | iuneq12d 5026* | Equality deduction for indexed union, deduction version. (Contributed by Drahflow, 22-Oct-2015.) |
β’ (π β π΄ = π΅) & β’ (π β πΆ = π·) β β’ (π β βͺ π₯ β π΄ πΆ = βͺ π₯ β π΅ π·) | ||
Theorem | iuneq2d 5027* | Equality deduction for indexed union. (Contributed by Drahflow, 22-Oct-2015.) |
β’ (π β π΅ = πΆ) β β’ (π β βͺ π₯ β π΄ π΅ = βͺ π₯ β π΄ πΆ) | ||
Theorem | nfiun 5028* | Bound-variable hypothesis builder for indexed union. (Contributed by Mario Carneiro, 25-Jan-2014.) Add disjoint variable condition to avoid ax-13 2372. See nfiung 5030 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024.) |
β’ β²π¦π΄ & β’ β²π¦π΅ β β’ β²π¦βͺ π₯ β π΄ π΅ | ||
Theorem | nfiin 5029* | Bound-variable hypothesis builder for indexed intersection. (Contributed by Mario Carneiro, 25-Jan-2014.) Add disjoint variable condition to avoid ax-13 2372. See nfiing 5031 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024.) |
β’ β²π¦π΄ & β’ β²π¦π΅ β β’ β²π¦β© π₯ β π΄ π΅ | ||
Theorem | nfiung 5030 | Bound-variable hypothesis builder for indexed union. Usage of this theorem is discouraged because it depends on ax-13 2372. See nfiun 5028 for a version with more disjoint variable conditions, but not requiring ax-13 2372. (Contributed by Mario Carneiro, 25-Jan-2014.) (New usage is discouraged.) |
β’ β²π¦π΄ & β’ β²π¦π΅ β β’ β²π¦βͺ π₯ β π΄ π΅ | ||
Theorem | nfiing 5031 | Bound-variable hypothesis builder for indexed intersection. Usage of this theorem is discouraged because it depends on ax-13 2372. See nfiin 5029 for a version with more disjoint variable conditions, but not requiring ax-13 2372. (Contributed by Mario Carneiro, 25-Jan-2014.) (New usage is discouraged.) |
β’ β²π¦π΄ & β’ β²π¦π΅ β β’ β²π¦β© π₯ β π΄ π΅ | ||
Theorem | nfiu1 5032 | Bound-variable hypothesis builder for indexed union. (Contributed by NM, 12-Oct-2003.) |
β’ β²π₯βͺ π₯ β π΄ π΅ | ||
Theorem | nfii1 5033 | Bound-variable hypothesis builder for indexed intersection. (Contributed by NM, 15-Oct-2003.) |
β’ β²π₯β© π₯ β π΄ π΅ | ||
Theorem | dfiun2g 5034* | Alternate definition of indexed union when π΅ is a set. Definition 15(a) of [Suppes] p. 44. (Contributed by NM, 23-Mar-2006.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) (Proof shortened by Rohan Ridenour, 11-Aug-2023.) Avoid ax-10 2138, ax-12 2172. (Revised by SN, 11-Dec-2024.) |
β’ (βπ₯ β π΄ π΅ β πΆ β βͺ π₯ β π΄ π΅ = βͺ {π¦ β£ βπ₯ β π΄ π¦ = π΅}) | ||
Theorem | dfiun2gOLD 5035* | Obsolete version of dfiun2g 5034 as of 11-Dec-2024. (Contributed by NM, 23-Mar-2006.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) (Proof shortened by Rohan Ridenour, 11-Aug-2023.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ (βπ₯ β π΄ π΅ β πΆ β βͺ π₯ β π΄ π΅ = βͺ {π¦ β£ βπ₯ β π΄ π¦ = π΅}) | ||
Theorem | dfiin2g 5036* | Alternate definition of indexed intersection when π΅ is a set. (Contributed by Jeff Hankins, 27-Aug-2009.) |
β’ (βπ₯ β π΄ π΅ β πΆ β β© π₯ β π΄ π΅ = β© {π¦ β£ βπ₯ β π΄ π¦ = π΅}) | ||
Theorem | dfiun2 5037* | Alternate definition of indexed union when π΅ is a set. Definition 15(a) of [Suppes] p. 44. (Contributed by NM, 27-Jun-1998.) (Revised by David Abernethy, 19-Jun-2012.) |
β’ π΅ β V β β’ βͺ π₯ β π΄ π΅ = βͺ {π¦ β£ βπ₯ β π΄ π¦ = π΅} | ||
Theorem | dfiin2 5038* | Alternate definition of indexed intersection when π΅ is a set. Definition 15(b) of [Suppes] p. 44. (Contributed by NM, 28-Jun-1998.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
β’ π΅ β V β β’ β© π₯ β π΄ π΅ = β© {π¦ β£ βπ₯ β π΄ π¦ = π΅} | ||
Theorem | dfiunv2 5039* | Define double indexed union. (Contributed by FL, 6-Nov-2013.) |
β’ βͺ π₯ β π΄ βͺ π¦ β π΅ πΆ = {π§ β£ βπ₯ β π΄ βπ¦ β π΅ π§ β πΆ} | ||
Theorem | cbviun 5040* | Rule used to change the bound variables in an indexed union, with the substitution specified implicitly by the hypothesis. (Contributed by NM, 26-Mar-2006.) (Revised by Andrew Salmon, 25-Jul-2011.) Add disjoint variable condition to avoid ax-13 2372. See cbviung 5042 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024.) |
β’ β²π¦π΅ & β’ β²π₯πΆ & β’ (π₯ = π¦ β π΅ = πΆ) β β’ βͺ π₯ β π΄ π΅ = βͺ π¦ β π΄ πΆ | ||
Theorem | cbviin 5041* | Change bound variables in an indexed intersection. (Contributed by Jeff Hankins, 26-Aug-2009.) (Revised by Mario Carneiro, 14-Oct-2016.) Add disjoint variable condition to avoid ax-13 2372. See cbviing 5043 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024.) |
β’ β²π¦π΅ & β’ β²π₯πΆ & β’ (π₯ = π¦ β π΅ = πΆ) β β’ β© π₯ β π΄ π΅ = β© π¦ β π΄ πΆ | ||
Theorem | cbviung 5042* | Rule used to change the bound variables in an indexed union, with the substitution specified implicitly by the hypothesis. Usage of this theorem is discouraged because it depends on ax-13 2372. See cbviun 5040 for a version with more disjoint variable conditions, but not requiring ax-13 2372. (Contributed by NM, 26-Mar-2006.) (Revised by Andrew Salmon, 25-Jul-2011.) (New usage is discouraged.) |
β’ β²π¦π΅ & β’ β²π₯πΆ & β’ (π₯ = π¦ β π΅ = πΆ) β β’ βͺ π₯ β π΄ π΅ = βͺ π¦ β π΄ πΆ | ||
Theorem | cbviing 5043* | Change bound variables in an indexed intersection. Usage of this theorem is discouraged because it depends on ax-13 2372. See cbviin 5041 for a version with more disjoint variable conditions, but not requiring ax-13 2372. (Contributed by Jeff Hankins, 26-Aug-2009.) (Revised by Mario Carneiro, 14-Oct-2016.) (New usage is discouraged.) |
β’ β²π¦π΅ & β’ β²π₯πΆ & β’ (π₯ = π¦ β π΅ = πΆ) β β’ β© π₯ β π΄ π΅ = β© π¦ β π΄ πΆ | ||
Theorem | cbviunv 5044* | Rule used to change the bound variables in an indexed union, with the substitution specified implicitly by the hypothesis. (Contributed by NM, 15-Sep-2003.) Add disjoint variable condition to avoid ax-13 2372. See cbviunvg 5046 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024.) |
β’ (π₯ = π¦ β π΅ = πΆ) β β’ βͺ π₯ β π΄ π΅ = βͺ π¦ β π΄ πΆ | ||
Theorem | cbviinv 5045* | Change bound variables in an indexed intersection. (Contributed by Jeff Hankins, 26-Aug-2009.) Add disjoint variable condition to avoid ax-13 2372. See cbviinvg 5047 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024.) |
β’ (π₯ = π¦ β π΅ = πΆ) β β’ β© π₯ β π΄ π΅ = β© π¦ β π΄ πΆ | ||
Theorem | cbviunvg 5046* | Rule used to change the bound variables in an indexed union, with the substitution specified implicitly by the hypothesis. Usage of this theorem is discouraged because it depends on ax-13 2372. Usage of the weaker cbviunv 5044 is preferred. (Contributed by NM, 15-Sep-2003.) (New usage is discouraged.) |
β’ (π₯ = π¦ β π΅ = πΆ) β β’ βͺ π₯ β π΄ π΅ = βͺ π¦ β π΄ πΆ | ||
Theorem | cbviinvg 5047* | Change bound variables in an indexed intersection. Usage of this theorem is discouraged because it depends on ax-13 2372. Usage of the weaker cbviinv 5045 is preferred. (Contributed by Jeff Hankins, 26-Aug-2009.) (New usage is discouraged.) |
β’ (π₯ = π¦ β π΅ = πΆ) β β’ β© π₯ β π΄ π΅ = β© π¦ β π΄ πΆ | ||
Theorem | iunssf 5048 | Subset theorem for an indexed union. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ β²π₯πΆ β β’ (βͺ π₯ β π΄ π΅ β πΆ β βπ₯ β π΄ π΅ β πΆ) | ||
Theorem | iunss 5049* | Subset theorem for an indexed union. (Contributed by NM, 13-Sep-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
β’ (βͺ π₯ β π΄ π΅ β πΆ β βπ₯ β π΄ π΅ β πΆ) | ||
Theorem | ssiun 5050* | Subset implication for an indexed union. (Contributed by NM, 3-Sep-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
β’ (βπ₯ β π΄ πΆ β π΅ β πΆ β βͺ π₯ β π΄ π΅) | ||
Theorem | ssiun2 5051 | Identity law for subset of an indexed union. (Contributed by NM, 12-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
β’ (π₯ β π΄ β π΅ β βͺ π₯ β π΄ π΅) | ||
Theorem | ssiun2s 5052* | Subset relationship for an indexed union. (Contributed by NM, 26-Oct-2003.) |
β’ (π₯ = πΆ β π΅ = π·) β β’ (πΆ β π΄ β π· β βͺ π₯ β π΄ π΅) | ||
Theorem | iunss2 5053* | A subclass condition on the members of two indexed classes πΆ(π₯) and π·(π¦) that implies a subclass relation on their indexed unions. Generalization of Proposition 8.6 of [TakeutiZaring] p. 59. Compare uniss2 4946. (Contributed by NM, 9-Dec-2004.) |
β’ (βπ₯ β π΄ βπ¦ β π΅ πΆ β π· β βͺ π₯ β π΄ πΆ β βͺ π¦ β π΅ π·) | ||
Theorem | iunssd 5054* | Subset theorem for an indexed union. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ ((π β§ π₯ β π΄) β π΅ β πΆ) β β’ (π β βͺ π₯ β π΄ π΅ β πΆ) | ||
Theorem | iunab 5055* | The indexed union of a class abstraction. (Contributed by NM, 27-Dec-2004.) |
β’ βͺ π₯ β π΄ {π¦ β£ π} = {π¦ β£ βπ₯ β π΄ π} | ||
Theorem | iunrab 5056* | The indexed union of a restricted class abstraction. (Contributed by NM, 3-Jan-2004.) (Proof shortened by Mario Carneiro, 14-Nov-2016.) |
β’ βͺ π₯ β π΄ {π¦ β π΅ β£ π} = {π¦ β π΅ β£ βπ₯ β π΄ π} | ||
Theorem | iunxdif2 5057* | Indexed union with a class difference as its index. (Contributed by NM, 10-Dec-2004.) |
β’ (π₯ = π¦ β πΆ = π·) β β’ (βπ₯ β π΄ βπ¦ β (π΄ β π΅)πΆ β π· β βͺ π¦ β (π΄ β π΅)π· = βͺ π₯ β π΄ πΆ) | ||
Theorem | ssiinf 5058 | Subset theorem for an indexed intersection. (Contributed by FL, 15-Oct-2012.) (Proof shortened by Mario Carneiro, 14-Oct-2016.) |
β’ β²π₯πΆ β β’ (πΆ β β© π₯ β π΄ π΅ β βπ₯ β π΄ πΆ β π΅) | ||
Theorem | ssiin 5059* | Subset theorem for an indexed intersection. (Contributed by NM, 15-Oct-2003.) |
β’ (πΆ β β© π₯ β π΄ π΅ β βπ₯ β π΄ πΆ β π΅) | ||
Theorem | iinss 5060* | Subset implication for an indexed intersection. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
β’ (βπ₯ β π΄ π΅ β πΆ β β© π₯ β π΄ π΅ β πΆ) | ||
Theorem | iinss2 5061 | An indexed intersection is included in any of its members. (Contributed by FL, 15-Oct-2012.) |
β’ (π₯ β π΄ β β© π₯ β π΄ π΅ β π΅) | ||
Theorem | uniiun 5062* | Class union in terms of indexed union. Definition in [Stoll] p. 43. (Contributed by NM, 28-Jun-1998.) |
β’ βͺ π΄ = βͺ π₯ β π΄ π₯ | ||
Theorem | intiin 5063* | Class intersection in terms of indexed intersection. Definition in [Stoll] p. 44. (Contributed by NM, 28-Jun-1998.) |
β’ β© π΄ = β© π₯ β π΄ π₯ | ||
Theorem | iunid 5064* | An indexed union of singletons recovers the index set. (Contributed by NM, 6-Sep-2005.) (Proof shortened by SN, 15-Jan-2025.) |
β’ βͺ π₯ β π΄ {π₯} = π΄ | ||
Theorem | iunidOLD 5065* | Obsolete version of iunid 5064 as of 15-Jan-2025. (Contributed by NM, 6-Sep-2005.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ βͺ π₯ β π΄ {π₯} = π΄ | ||
Theorem | iun0 5066 | An indexed union of the empty set is empty. (Contributed by NM, 26-Mar-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
β’ βͺ π₯ β π΄ β = β | ||
Theorem | 0iun 5067 | An empty indexed union is empty. (Contributed by NM, 4-Dec-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
β’ βͺ π₯ β β π΄ = β | ||
Theorem | 0iin 5068 | An empty indexed intersection is the universal class. (Contributed by NM, 20-Oct-2005.) |
β’ β© π₯ β β π΄ = V | ||
Theorem | viin 5069* | Indexed intersection with a universal index class. When π΄ doesn't depend on π₯, this evaluates to π΄ by 19.3 2196 and abid2 2872. When π΄ = π₯, this evaluates to β by intiin 5063 and intv 5363. (Contributed by NM, 11-Sep-2008.) |
β’ β© π₯ β V π΄ = {π¦ β£ βπ₯ π¦ β π΄} | ||
Theorem | iunsn 5070* | Indexed union of a singleton. Compare dfiun2 5037 and rnmpt 5955. (Contributed by Steven Nguyen, 7-Jun-2023.) |
β’ βͺ π₯ β π΄ {π΅} = {π¦ β£ βπ₯ β π΄ π¦ = π΅} | ||
Theorem | iunn0 5071* | There is a nonempty class in an indexed collection π΅(π₯) iff the indexed union of them is nonempty. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
β’ (βπ₯ β π΄ π΅ β β β βͺ π₯ β π΄ π΅ β β ) | ||
Theorem | iinab 5072* | Indexed intersection of a class abstraction. (Contributed by NM, 6-Dec-2011.) |
β’ β© π₯ β π΄ {π¦ β£ π} = {π¦ β£ βπ₯ β π΄ π} | ||
Theorem | iinrab 5073* | Indexed intersection of a restricted class abstraction. (Contributed by NM, 6-Dec-2011.) |
β’ (π΄ β β β β© π₯ β π΄ {π¦ β π΅ β£ π} = {π¦ β π΅ β£ βπ₯ β π΄ π}) | ||
Theorem | iinrab2 5074* | Indexed intersection of a restricted class abstraction. (Contributed by NM, 6-Dec-2011.) |
β’ (β© π₯ β π΄ {π¦ β π΅ β£ π} β© π΅) = {π¦ β π΅ β£ βπ₯ β π΄ π} | ||
Theorem | iunin2 5075* | Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 5062 to recover Enderton's theorem. (Contributed by NM, 26-Mar-2004.) |
β’ βͺ π₯ β π΄ (π΅ β© πΆ) = (π΅ β© βͺ π₯ β π΄ πΆ) | ||
Theorem | iunin1 5076* | Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 5062 to recover Enderton's theorem. (Contributed by Mario Carneiro, 30-Aug-2015.) |
β’ βͺ π₯ β π΄ (πΆ β© π΅) = (βͺ π₯ β π΄ πΆ β© π΅) | ||
Theorem | iinun2 5077* | Indexed intersection of union. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use intiin 5063 to recover Enderton's theorem. (Contributed by NM, 19-Aug-2004.) |
β’ β© π₯ β π΄ (π΅ βͺ πΆ) = (π΅ βͺ β© π₯ β π΄ πΆ) | ||
Theorem | iundif2 5078* | Indexed union of class difference. Generalization of half of theorem "De Morgan's laws" in [Enderton] p. 31. Use intiin 5063 to recover Enderton's theorem. (Contributed by NM, 19-Aug-2004.) |
β’ βͺ π₯ β π΄ (π΅ β πΆ) = (π΅ β β© π₯ β π΄ πΆ) | ||
Theorem | iindif1 5079* | Indexed intersection of class difference with the subtrahend held constant. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
β’ (π΄ β β β β© π₯ β π΄ (π΅ β πΆ) = (β© π₯ β π΄ π΅ β πΆ)) | ||
Theorem | 2iunin 5080* | Rearrange indexed unions over intersection. (Contributed by NM, 18-Dec-2008.) |
β’ βͺ π₯ β π΄ βͺ π¦ β π΅ (πΆ β© π·) = (βͺ π₯ β π΄ πΆ β© βͺ π¦ β π΅ π·) | ||
Theorem | iindif2 5081* | Indexed intersection of class difference. Generalization of half of theorem "De Morgan's laws" in [Enderton] p. 31. Use uniiun 5062 to recover Enderton's theorem. (Contributed by NM, 5-Oct-2006.) |
β’ (π΄ β β β β© π₯ β π΄ (π΅ β πΆ) = (π΅ β βͺ π₯ β π΄ πΆ)) | ||
Theorem | iinin2 5082* | Indexed intersection of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use intiin 5063 to recover Enderton's theorem. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ (π΄ β β β β© π₯ β π΄ (π΅ β© πΆ) = (π΅ β© β© π₯ β π΄ πΆ)) | ||
Theorem | iinin1 5083* | Indexed intersection of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use intiin 5063 to recover Enderton's theorem. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ (π΄ β β β β© π₯ β π΄ (πΆ β© π΅) = (β© π₯ β π΄ πΆ β© π΅)) | ||
Theorem | iinvdif 5084* | The indexed intersection of a complement. (Contributed by GΓ©rard Lang, 5-Aug-2018.) |
β’ β© π₯ β π΄ (V β π΅) = (V β βͺ π₯ β π΄ π΅) | ||
Theorem | elriin 5085* | Elementhood in a relative intersection. (Contributed by Mario Carneiro, 30-Dec-2016.) |
β’ (π΅ β (π΄ β© β© π₯ β π π) β (π΅ β π΄ β§ βπ₯ β π π΅ β π)) | ||
Theorem | riin0 5086* | Relative intersection of an empty family. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
β’ (π = β β (π΄ β© β© π₯ β π π) = π΄) | ||
Theorem | riinn0 5087* | Relative intersection of a nonempty family. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
β’ ((βπ₯ β π π β π΄ β§ π β β ) β (π΄ β© β© π₯ β π π) = β© π₯ β π π) | ||
Theorem | riinrab 5088* | Relative intersection of a relative abstraction. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
β’ (π΄ β© β© π₯ β π {π¦ β π΄ β£ π}) = {π¦ β π΄ β£ βπ₯ β π π} | ||
Theorem | symdif0 5089 | Symmetric difference with the empty class. The empty class is the identity element for symmetric difference. (Contributed by Scott Fenton, 24-Apr-2012.) |
β’ (π΄ β³ β ) = π΄ | ||
Theorem | symdifv 5090 | The symmetric difference with the universal class is the complement. (Contributed by Scott Fenton, 24-Apr-2012.) |
β’ (π΄ β³ V) = (V β π΄) | ||
Theorem | symdifid 5091 | The symmetric difference of a class with itself is the empty class. (Contributed by Scott Fenton, 25-Apr-2012.) |
β’ (π΄ β³ π΄) = β | ||
Theorem | iinxsng 5092* | A singleton index picks out an instance of an indexed intersection's argument. (Contributed by NM, 15-Jan-2012.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) |
β’ (π₯ = π΄ β π΅ = πΆ) β β’ (π΄ β π β β© π₯ β {π΄}π΅ = πΆ) | ||
Theorem | iinxprg 5093* | Indexed intersection with an unordered pair index. (Contributed by NM, 25-Jan-2012.) |
β’ (π₯ = π΄ β πΆ = π·) & β’ (π₯ = π΅ β πΆ = πΈ) β β’ ((π΄ β π β§ π΅ β π) β β© π₯ β {π΄, π΅}πΆ = (π· β© πΈ)) | ||
Theorem | iunxsng 5094* | A singleton index picks out an instance of an indexed union's argument. (Contributed by Mario Carneiro, 25-Jun-2016.) |
β’ (π₯ = π΄ β π΅ = πΆ) β β’ (π΄ β π β βͺ π₯ β {π΄}π΅ = πΆ) | ||
Theorem | iunxsn 5095* | A singleton index picks out an instance of an indexed union's argument. (Contributed by NM, 26-Mar-2004.) (Proof shortened by Mario Carneiro, 25-Jun-2016.) |
β’ π΄ β V & β’ (π₯ = π΄ β π΅ = πΆ) β β’ βͺ π₯ β {π΄}π΅ = πΆ | ||
Theorem | iunxsngf 5096* | A singleton index picks out an instance of an indexed union's argument. (Contributed by Mario Carneiro, 25-Jun-2016.) (Revised by Thierry Arnoux, 2-May-2020.) Avoid ax-13 2372. (Revised by Gino Giotto, 19-May-2023.) |
β’ β²π₯πΆ & β’ (π₯ = π΄ β π΅ = πΆ) β β’ (π΄ β π β βͺ π₯ β {π΄}π΅ = πΆ) | ||
Theorem | iunun 5097 | Separate a union in an indexed union. (Contributed by NM, 27-Dec-2004.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) |
β’ βͺ π₯ β π΄ (π΅ βͺ πΆ) = (βͺ π₯ β π΄ π΅ βͺ βͺ π₯ β π΄ πΆ) | ||
Theorem | iunxun 5098 | Separate a union in the index of an indexed union. (Contributed by NM, 26-Mar-2004.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) |
β’ βͺ π₯ β (π΄ βͺ π΅)πΆ = (βͺ π₯ β π΄ πΆ βͺ βͺ π₯ β π΅ πΆ) | ||
Theorem | iunxdif3 5099* | An indexed union where some terms are the empty set. See iunxdif2 5057. (Contributed by Thierry Arnoux, 4-May-2020.) |
β’ β²π₯πΈ β β’ (βπ₯ β πΈ π΅ = β β βͺ π₯ β (π΄ β πΈ)π΅ = βͺ π₯ β π΄ π΅) | ||
Theorem | iunxprg 5100* | A pair index picks out two instances of an indexed union's argument. (Contributed by Alexander van der Vekens, 2-Feb-2018.) |
β’ (π₯ = π΄ β πΆ = π·) & β’ (π₯ = π΅ β πΆ = πΈ) β β’ ((π΄ β π β§ π΅ β π) β βͺ π₯ β {π΄, π΅}πΆ = (π· βͺ πΈ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |