![]() |
Metamath
Proof Explorer Theorem List (p. 51 of 482) | < 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-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | iinconst 5001* | Indexed intersection of a constant class, i.e. where 𝐵 does not depend on 𝑥. (Contributed by Mario Carneiro, 6-Feb-2015.) |
⊢ (𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 𝐵 = 𝐵) | ||
Theorem | iuneqconst 5002* | Indexed union of identical classes. (Contributed by AV, 5-Mar-2024.) |
⊢ (𝑥 = 𝑋 → 𝐵 = 𝐶) ⇒ ⊢ ((𝑋 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶) → ∪ 𝑥 ∈ 𝐴 𝐵 = 𝐶) | ||
Theorem | iuniin 5003* | 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 5004* | An indexed intersection is a subset of the corresponding indexed union. (Contributed by Thierry Arnoux, 31-Dec-2021.) |
⊢ (𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) | ||
Theorem | iunss1 5005* | Subclass theorem for indexed union. (Contributed by NM, 10-Dec-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ (𝐴 ⊆ 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑥 ∈ 𝐵 𝐶) | ||
Theorem | iinss1 5006* | Subclass theorem for indexed intersection. (Contributed by NM, 24-Jan-2012.) |
⊢ (𝐴 ⊆ 𝐵 → ∩ 𝑥 ∈ 𝐵 𝐶 ⊆ ∩ 𝑥 ∈ 𝐴 𝐶) | ||
Theorem | iuneq1 5007* | Equality theorem for indexed union. (Contributed by NM, 27-Jun-1998.) |
⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶) | ||
Theorem | iineq1 5008* | Equality theorem for indexed intersection. (Contributed by NM, 27-Jun-1998.) |
⊢ (𝐴 = 𝐵 → ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐶) | ||
Theorem | ss2iun 5009 | Subclass theorem for indexed union. (Contributed by NM, 26-Nov-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐶) | ||
Theorem | iuneq2 5010 | Equality theorem for indexed union. (Contributed by NM, 22-Oct-2003.) |
⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶) | ||
Theorem | iineq2 5011 | Equality theorem for indexed intersection. (Contributed by NM, 22-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑥 ∈ 𝐴 𝐶) | ||
Theorem | iuneq2i 5012 | Equality inference for indexed union. (Contributed by NM, 22-Oct-2003.) |
⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶 | ||
Theorem | iineq2i 5013 | Equality inference for indexed intersection. (Contributed by NM, 22-Oct-2003.) |
⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑥 ∈ 𝐴 𝐶 | ||
Theorem | iineq2d 5014 | Equality deduction for indexed intersection. (Contributed by NM, 7-Dec-2011.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑥 ∈ 𝐴 𝐶) | ||
Theorem | iuneq2dv 5015* | Equality deduction for indexed union. (Contributed by NM, 3-Aug-2004.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶) | ||
Theorem | iineq2dv 5016* | Equality deduction for indexed intersection. (Contributed by NM, 3-Aug-2004.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑥 ∈ 𝐴 𝐶) | ||
Theorem | iuneq12df 5017 | Equality deduction for indexed union, deduction version. (Contributed by Thierry Arnoux, 31-Dec-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷) | ||
Theorem | iuneq1d 5018* | Equality theorem for indexed union, deduction version. (Contributed by Drahflow, 22-Oct-2015.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶) | ||
Theorem | iuneq12d 5019* | Equality deduction for indexed union, deduction version. (Contributed by Drahflow, 22-Oct-2015.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷) | ||
Theorem | iuneq2d 5020* | Equality deduction for indexed union. (Contributed by Drahflow, 22-Oct-2015.) |
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶) | ||
Theorem | nfiun 5021* | Bound-variable hypothesis builder for indexed union. (Contributed by Mario Carneiro, 25-Jan-2014.) Add disjoint variable condition to avoid ax-13 2366. See nfiung 5023 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝐵 ⇒ ⊢ Ⅎ𝑦∪ 𝑥 ∈ 𝐴 𝐵 | ||
Theorem | nfiin 5022* | Bound-variable hypothesis builder for indexed intersection. (Contributed by Mario Carneiro, 25-Jan-2014.) Add disjoint variable condition to avoid ax-13 2366. See nfiing 5024 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝐵 ⇒ ⊢ Ⅎ𝑦∩ 𝑥 ∈ 𝐴 𝐵 | ||
Theorem | nfiung 5023 | Bound-variable hypothesis builder for indexed union. Usage of this theorem is discouraged because it depends on ax-13 2366. See nfiun 5021 for a version with more disjoint variable conditions, but not requiring ax-13 2366. (Contributed by Mario Carneiro, 25-Jan-2014.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝐵 ⇒ ⊢ Ⅎ𝑦∪ 𝑥 ∈ 𝐴 𝐵 | ||
Theorem | nfiing 5024 | Bound-variable hypothesis builder for indexed intersection. Usage of this theorem is discouraged because it depends on ax-13 2366. See nfiin 5022 for a version with more disjoint variable conditions, but not requiring ax-13 2366. (Contributed by Mario Carneiro, 25-Jan-2014.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝐵 ⇒ ⊢ Ⅎ𝑦∩ 𝑥 ∈ 𝐴 𝐵 | ||
Theorem | nfiu1 5025 | Bound-variable hypothesis builder for indexed union. (Contributed by NM, 12-Oct-2003.) |
⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵 | ||
Theorem | nfii1 5026 | Bound-variable hypothesis builder for indexed intersection. (Contributed by NM, 15-Oct-2003.) |
⊢ Ⅎ𝑥∩ 𝑥 ∈ 𝐴 𝐵 | ||
Theorem | dfiun2g 5027* | 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 2130, ax-12 2164. (Revised by SN, 11-Dec-2024.) |
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) | ||
Theorem | dfiun2gOLD 5028* | Obsolete version of dfiun2g 5027 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 5029* | Alternate definition of indexed intersection when 𝐵 is a set. (Contributed by Jeff Hankins, 27-Aug-2009.) |
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) | ||
Theorem | dfiun2 5030* | 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 5031* | 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 5032* | Define double indexed union. (Contributed by FL, 6-Nov-2013.) |
⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 ∈ 𝐶} | ||
Theorem | cbviun 5033* | 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 2366. See cbviung 5035 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024.) |
⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶 | ||
Theorem | cbviin 5034* | 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 2366. See cbviing 5036 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024.) |
⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑦 ∈ 𝐴 𝐶 | ||
Theorem | cbviung 5035* | 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 2366. See cbviun 5033 for a version with more disjoint variable conditions, but not requiring ax-13 2366. (Contributed by NM, 26-Mar-2006.) (Revised by Andrew Salmon, 25-Jul-2011.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶 | ||
Theorem | cbviing 5036* | Change bound variables in an indexed intersection. Usage of this theorem is discouraged because it depends on ax-13 2366. See cbviin 5034 for a version with more disjoint variable conditions, but not requiring ax-13 2366. (Contributed by Jeff Hankins, 26-Aug-2009.) (Revised by Mario Carneiro, 14-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑦 ∈ 𝐴 𝐶 | ||
Theorem | cbviunv 5037* | 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 2366. See cbviunvg 5039 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024.) |
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶 | ||
Theorem | cbviinv 5038* | Change bound variables in an indexed intersection. (Contributed by Jeff Hankins, 26-Aug-2009.) Add disjoint variable condition to avoid ax-13 2366. See cbviinvg 5040 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024.) |
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑦 ∈ 𝐴 𝐶 | ||
Theorem | cbviunvg 5039* | 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 2366. Usage of the weaker cbviunv 5037 is preferred. (Contributed by NM, 15-Sep-2003.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶 | ||
Theorem | cbviinvg 5040* | Change bound variables in an indexed intersection. Usage of this theorem is discouraged because it depends on ax-13 2366. Usage of the weaker cbviinv 5038 is preferred. (Contributed by Jeff Hankins, 26-Aug-2009.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑦 ∈ 𝐴 𝐶 | ||
Theorem | iunssf 5041 | Subset theorem for an indexed union. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ Ⅎ𝑥𝐶 ⇒ ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶) | ||
Theorem | iunss 5042* | Subset theorem for an indexed union. (Contributed by NM, 13-Sep-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶) | ||
Theorem | ssiun 5043* | Subset implication for an indexed union. (Contributed by NM, 3-Sep-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ (∃𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵 → 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) | ||
Theorem | ssiun2 5044 | Identity law for subset of an indexed union. (Contributed by NM, 12-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) | ||
Theorem | ssiun2s 5045* | Subset relationship for an indexed union. (Contributed by NM, 26-Oct-2003.) |
⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷) ⇒ ⊢ (𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) | ||
Theorem | iunss2 5046* | 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 4939. (Contributed by NM, 9-Dec-2004.) |
⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐶 ⊆ 𝐷 → ∪ 𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑦 ∈ 𝐵 𝐷) | ||
Theorem | iunssd 5047* | Subset theorem for an indexed union. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶) | ||
Theorem | iunab 5048* | The indexed union of a class abstraction. (Contributed by NM, 27-Dec-2004.) |
⊢ ∪ 𝑥 ∈ 𝐴 {𝑦 ∣ 𝜑} = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} | ||
Theorem | iunrab 5049* | The indexed union of a restricted class abstraction. (Contributed by NM, 3-Jan-2004.) (Proof shortened by Mario Carneiro, 14-Nov-2016.) |
⊢ ∪ 𝑥 ∈ 𝐴 {𝑦 ∈ 𝐵 ∣ 𝜑} = {𝑦 ∈ 𝐵 ∣ ∃𝑥 ∈ 𝐴 𝜑} | ||
Theorem | iunxdif2 5050* | Indexed union with a class difference as its index. (Contributed by NM, 10-Dec-2004.) |
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ (𝐴 ∖ 𝐵)𝐶 ⊆ 𝐷 → ∪ 𝑦 ∈ (𝐴 ∖ 𝐵)𝐷 = ∪ 𝑥 ∈ 𝐴 𝐶) | ||
Theorem | ssiinf 5051 | Subset theorem for an indexed intersection. (Contributed by FL, 15-Oct-2012.) (Proof shortened by Mario Carneiro, 14-Oct-2016.) |
⊢ Ⅎ𝑥𝐶 ⇒ ⊢ (𝐶 ⊆ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵) | ||
Theorem | ssiin 5052* | Subset theorem for an indexed intersection. (Contributed by NM, 15-Oct-2003.) |
⊢ (𝐶 ⊆ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵) | ||
Theorem | iinss 5053* | Subset implication for an indexed intersection. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ (∃𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶) | ||
Theorem | iinss2 5054 | An indexed intersection is included in any of its members. (Contributed by FL, 15-Oct-2012.) |
⊢ (𝑥 ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐵) | ||
Theorem | uniiun 5055* | Class union in terms of indexed union. Definition in [Stoll] p. 43. (Contributed by NM, 28-Jun-1998.) |
⊢ ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝑥 | ||
Theorem | intiin 5056* | Class intersection in terms of indexed intersection. Definition in [Stoll] p. 44. (Contributed by NM, 28-Jun-1998.) |
⊢ ∩ 𝐴 = ∩ 𝑥 ∈ 𝐴 𝑥 | ||
Theorem | iunid 5057* | An indexed union of singletons recovers the index set. (Contributed by NM, 6-Sep-2005.) (Proof shortened by SN, 15-Jan-2025.) |
⊢ ∪ 𝑥 ∈ 𝐴 {𝑥} = 𝐴 | ||
Theorem | iunidOLD 5058* | Obsolete version of iunid 5057 as of 15-Jan-2025. (Contributed by NM, 6-Sep-2005.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ∪ 𝑥 ∈ 𝐴 {𝑥} = 𝐴 | ||
Theorem | iun0 5059 | 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 5060 | An empty indexed union is empty. (Contributed by NM, 4-Dec-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ ∪ 𝑥 ∈ ∅ 𝐴 = ∅ | ||
Theorem | 0iin 5061 | An empty indexed intersection is the universal class. (Contributed by NM, 20-Oct-2005.) |
⊢ ∩ 𝑥 ∈ ∅ 𝐴 = V | ||
Theorem | viin 5062* | Indexed intersection with a universal index class. When 𝐴 doesn't depend on 𝑥, this evaluates to 𝐴 by 19.3 2188 and abid2 2866. When 𝐴 = 𝑥, this evaluates to ∅ by intiin 5056 and intv 5358. (Contributed by NM, 11-Sep-2008.) |
⊢ ∩ 𝑥 ∈ V 𝐴 = {𝑦 ∣ ∀𝑥 𝑦 ∈ 𝐴} | ||
Theorem | iunsn 5063* | Indexed union of a singleton. Compare dfiun2 5030 and rnmpt 5951. (Contributed by Steven Nguyen, 7-Jun-2023.) |
⊢ ∪ 𝑥 ∈ 𝐴 {𝐵} = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} | ||
Theorem | iunn0 5064* | 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 5065* | Indexed intersection of a class abstraction. (Contributed by NM, 6-Dec-2011.) |
⊢ ∩ 𝑥 ∈ 𝐴 {𝑦 ∣ 𝜑} = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝜑} | ||
Theorem | iinrab 5066* | Indexed intersection of a restricted class abstraction. (Contributed by NM, 6-Dec-2011.) |
⊢ (𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 {𝑦 ∈ 𝐵 ∣ 𝜑} = {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐴 𝜑}) | ||
Theorem | iinrab2 5067* | Indexed intersection of a restricted class abstraction. (Contributed by NM, 6-Dec-2011.) |
⊢ (∩ 𝑥 ∈ 𝐴 {𝑦 ∈ 𝐵 ∣ 𝜑} ∩ 𝐵) = {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐴 𝜑} | ||
Theorem | iunin2 5068* | Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 5055 to recover Enderton's theorem. (Contributed by NM, 26-Mar-2004.) |
⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = (𝐵 ∩ ∪ 𝑥 ∈ 𝐴 𝐶) | ||
Theorem | iunin1 5069* | Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 5055 to recover Enderton's theorem. (Contributed by Mario Carneiro, 30-Aug-2015.) |
⊢ ∪ 𝑥 ∈ 𝐴 (𝐶 ∩ 𝐵) = (∪ 𝑥 ∈ 𝐴 𝐶 ∩ 𝐵) | ||
Theorem | iinun2 5070* | Indexed intersection of union. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use intiin 5056 to recover Enderton's theorem. (Contributed by NM, 19-Aug-2004.) |
⊢ ∩ 𝑥 ∈ 𝐴 (𝐵 ∪ 𝐶) = (𝐵 ∪ ∩ 𝑥 ∈ 𝐴 𝐶) | ||
Theorem | iundif2 5071* | Indexed union of class difference. Generalization of half of theorem "De Morgan's laws" in [Enderton] p. 31. Use intiin 5056 to recover Enderton's theorem. (Contributed by NM, 19-Aug-2004.) |
⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∖ 𝐶) = (𝐵 ∖ ∩ 𝑥 ∈ 𝐴 𝐶) | ||
Theorem | iindif1 5072* | Indexed intersection of class difference with the subtrahend held constant. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
⊢ (𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 (𝐵 ∖ 𝐶) = (∩ 𝑥 ∈ 𝐴 𝐵 ∖ 𝐶)) | ||
Theorem | 2iunin 5073* | Rearrange indexed unions over intersection. (Contributed by NM, 18-Dec-2008.) |
⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 (𝐶 ∩ 𝐷) = (∪ 𝑥 ∈ 𝐴 𝐶 ∩ ∪ 𝑦 ∈ 𝐵 𝐷) | ||
Theorem | iindif2 5074* | Indexed intersection of class difference. Generalization of half of theorem "De Morgan's laws" in [Enderton] p. 31. Use uniiun 5055 to recover Enderton's theorem. (Contributed by NM, 5-Oct-2006.) |
⊢ (𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 (𝐵 ∖ 𝐶) = (𝐵 ∖ ∪ 𝑥 ∈ 𝐴 𝐶)) | ||
Theorem | iinin2 5075* | Indexed intersection of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use intiin 5056 to recover Enderton's theorem. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ (𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = (𝐵 ∩ ∩ 𝑥 ∈ 𝐴 𝐶)) | ||
Theorem | iinin1 5076* | Indexed intersection of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use intiin 5056 to recover Enderton's theorem. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ (𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 (𝐶 ∩ 𝐵) = (∩ 𝑥 ∈ 𝐴 𝐶 ∩ 𝐵)) | ||
Theorem | iinvdif 5077* | The indexed intersection of a complement. (Contributed by Gérard Lang, 5-Aug-2018.) |
⊢ ∩ 𝑥 ∈ 𝐴 (V ∖ 𝐵) = (V ∖ ∪ 𝑥 ∈ 𝐴 𝐵) | ||
Theorem | elriin 5078* | Elementhood in a relative intersection. (Contributed by Mario Carneiro, 30-Dec-2016.) |
⊢ (𝐵 ∈ (𝐴 ∩ ∩ 𝑥 ∈ 𝑋 𝑆) ↔ (𝐵 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝑋 𝐵 ∈ 𝑆)) | ||
Theorem | riin0 5079* | Relative intersection of an empty family. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
⊢ (𝑋 = ∅ → (𝐴 ∩ ∩ 𝑥 ∈ 𝑋 𝑆) = 𝐴) | ||
Theorem | riinn0 5080* | Relative intersection of a nonempty family. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
⊢ ((∀𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴 ∧ 𝑋 ≠ ∅) → (𝐴 ∩ ∩ 𝑥 ∈ 𝑋 𝑆) = ∩ 𝑥 ∈ 𝑋 𝑆) | ||
Theorem | riinrab 5081* | Relative intersection of a relative abstraction. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
⊢ (𝐴 ∩ ∩ 𝑥 ∈ 𝑋 {𝑦 ∈ 𝐴 ∣ 𝜑}) = {𝑦 ∈ 𝐴 ∣ ∀𝑥 ∈ 𝑋 𝜑} | ||
Theorem | symdif0 5082 | 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 5083 | The symmetric difference with the universal class is the complement. (Contributed by Scott Fenton, 24-Apr-2012.) |
⊢ (𝐴 △ V) = (V ∖ 𝐴) | ||
Theorem | symdifid 5084 | The symmetric difference of a class with itself is the empty class. (Contributed by Scott Fenton, 25-Apr-2012.) |
⊢ (𝐴 △ 𝐴) = ∅ | ||
Theorem | iinxsng 5085* | 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 5086* | Indexed intersection with an unordered pair index. (Contributed by NM, 25-Jan-2012.) |
⊢ (𝑥 = 𝐴 → 𝐶 = 𝐷) & ⊢ (𝑥 = 𝐵 → 𝐶 = 𝐸) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∩ 𝑥 ∈ {𝐴, 𝐵}𝐶 = (𝐷 ∩ 𝐸)) | ||
Theorem | iunxsng 5087* | A singleton index picks out an instance of an indexed union's argument. (Contributed by Mario Carneiro, 25-Jun-2016.) |
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝐴 ∈ 𝑉 → ∪ 𝑥 ∈ {𝐴}𝐵 = 𝐶) | ||
Theorem | iunxsn 5088* | 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 5089* | 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 2366. (Revised by Gino Giotto, 19-May-2023.) |
⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝐴 ∈ 𝑉 → ∪ 𝑥 ∈ {𝐴}𝐵 = 𝐶) | ||
Theorem | iunun 5090 | Separate a union in an indexed union. (Contributed by NM, 27-Dec-2004.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) |
⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∪ 𝐶) = (∪ 𝑥 ∈ 𝐴 𝐵 ∪ ∪ 𝑥 ∈ 𝐴 𝐶) | ||
Theorem | iunxun 5091 | 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 5092* | An indexed union where some terms are the empty set. See iunxdif2 5050. (Contributed by Thierry Arnoux, 4-May-2020.) |
⊢ Ⅎ𝑥𝐸 ⇒ ⊢ (∀𝑥 ∈ 𝐸 𝐵 = ∅ → ∪ 𝑥 ∈ (𝐴 ∖ 𝐸)𝐵 = ∪ 𝑥 ∈ 𝐴 𝐵) | ||
Theorem | iunxprg 5093* | A pair index picks out two instances of an indexed union's argument. (Contributed by Alexander van der Vekens, 2-Feb-2018.) |
⊢ (𝑥 = 𝐴 → 𝐶 = 𝐷) & ⊢ (𝑥 = 𝐵 → 𝐶 = 𝐸) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∪ 𝑥 ∈ {𝐴, 𝐵}𝐶 = (𝐷 ∪ 𝐸)) | ||
Theorem | iunxiun 5094* | Separate an indexed union in the index of an indexed union. (Contributed by Mario Carneiro, 5-Dec-2016.) |
⊢ ∪ 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 = ∪ 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 | ||
Theorem | iinuni 5095* | A relationship involving union and indexed intersection. Exercise 23 of [Enderton] p. 33. (Contributed by NM, 25-Nov-2003.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) |
⊢ (𝐴 ∪ ∩ 𝐵) = ∩ 𝑥 ∈ 𝐵 (𝐴 ∪ 𝑥) | ||
Theorem | iununi 5096* | A relationship involving union and indexed union. Exercise 25 of [Enderton] p. 33. (Contributed by NM, 25-Nov-2003.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) |
⊢ ((𝐵 = ∅ → 𝐴 = ∅) ↔ (𝐴 ∪ ∪ 𝐵) = ∪ 𝑥 ∈ 𝐵 (𝐴 ∪ 𝑥)) | ||
Theorem | sspwuni 5097 | Subclass relationship for power class and union. (Contributed by NM, 18-Jul-2006.) |
⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 ⊆ 𝐵) | ||
Theorem | pwssb 5098* | Two ways to express a collection of subclasses. (Contributed by NM, 19-Jul-2006.) |
⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵) | ||
Theorem | elpwpw 5099 | Characterization of the elements of a double power class: they are exactly the sets whose union is included in that class. (Contributed by BJ, 29-Apr-2021.) |
⊢ (𝐴 ∈ 𝒫 𝒫 𝐵 ↔ (𝐴 ∈ V ∧ ∪ 𝐴 ⊆ 𝐵)) | ||
Theorem | pwpwab 5100* | The double power class written as a class abstraction: the class of sets whose union is included in the given class. (Contributed by BJ, 29-Apr-2021.) |
⊢ 𝒫 𝒫 𝐴 = {𝑥 ∣ ∪ 𝑥 ⊆ 𝐴} |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |