P. 42 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 4101-4200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	equncomi 4101	Inference form of equncom 4100. equncomi 4101 was automatically derived from equncomiVD 45313 using the tools program translate_without_overwriting.cmd and minimizing. (Contributed by Alan Sare, 18-Feb-2012.)
⊢ 𝐴 = (𝐵 ∪ 𝐶)    ⇒   ⊢ 𝐴 = (𝐶 ∪ 𝐵)
Theorem	uneq1 4102	Equality theorem for the union of two classes. (Contributed by NM, 15-Jul-1993.)
⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))
Theorem	uneq2 4103	Equality theorem for the union of two classes. (Contributed by NM, 5-Aug-1993.)
⊢ (𝐴 = 𝐵 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵))
Theorem	uneq12 4104	Equality theorem for the union of two classes. (Contributed by NM, 29-Mar-1998.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷))
Theorem	uneq1i 4105	Inference adding union to the right in a class equality. (Contributed by NM, 30-Aug-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶)
Theorem	uneq2i 4106	Inference adding union to the left in a class equality. (Contributed by NM, 30-Aug-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵)
Theorem	uneq12i 4107	Equality inference for the union of two classes. (Contributed by NM, 12-Aug-2004.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷)
Theorem	uneq1d 4108	Deduction adding union to the right in a class equality. (Contributed by NM, 29-Mar-1998.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))
Theorem	uneq2d 4109	Deduction adding union to the left in a class equality. (Contributed by NM, 29-Mar-1998.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵))
Theorem	uneq12d 4110	Equality deduction for the union of two classes. (Contributed by NM, 29-Sep-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷))
Theorem	nfun 4111	Bound-variable hypothesis builder for the union of classes. (Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro, 14-Oct-2016.) Avoid ax-10 2147, ax-11 2163, ax-12 2185. (Revised by SN, 14-May-2025.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝐴 ∪ 𝐵)
Theorem	nfunOLD 4112	Obsolete version of nfun 4111 as of 14-May-2025. (Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro, 14-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝐴 ∪ 𝐵)
Theorem	unass 4113	Associative law for union of classes. Exercise 8 of [TakeutiZaring] p. 17. (Contributed by NM, 3-May-1994.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ((𝐴 ∪ 𝐵) ∪ 𝐶) = (𝐴 ∪ (𝐵 ∪ 𝐶))
Theorem	un12 4114	A rearrangement of union. (Contributed by NM, 12-Aug-2004.)
⊢ (𝐴 ∪ (𝐵 ∪ 𝐶)) = (𝐵 ∪ (𝐴 ∪ 𝐶))
Theorem	un23 4115	A rearrangement of union. (Contributed by NM, 12-Aug-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ((𝐴 ∪ 𝐵) ∪ 𝐶) = ((𝐴 ∪ 𝐶) ∪ 𝐵)
Theorem	un4 4116	A rearrangement of the union of 4 classes. (Contributed by NM, 12-Aug-2004.)
⊢ ((𝐴 ∪ 𝐵) ∪ (𝐶 ∪ 𝐷)) = ((𝐴 ∪ 𝐶) ∪ (𝐵 ∪ 𝐷))
Theorem	unundi 4117	Union distributes over itself. (Contributed by NM, 17-Aug-2004.)
⊢ (𝐴 ∪ (𝐵 ∪ 𝐶)) = ((𝐴 ∪ 𝐵) ∪ (𝐴 ∪ 𝐶))
Theorem	unundir 4118	Union distributes over itself. (Contributed by NM, 17-Aug-2004.)
⊢ ((𝐴 ∪ 𝐵) ∪ 𝐶) = ((𝐴 ∪ 𝐶) ∪ (𝐵 ∪ 𝐶))
Theorem	ssun1 4119	Subclass relationship for union of classes. Theorem 25 of [Suppes] p. 27. (Contributed by NM, 5-Aug-1993.)
⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
Theorem	ssun2 4120	Subclass relationship for union of classes. (Contributed by NM, 30-Aug-1993.)
⊢ 𝐴 ⊆ (𝐵 ∪ 𝐴)
Theorem	ssun3 4121	Subclass law for union of classes. (Contributed by NM, 5-Aug-1993.)
⊢ (𝐴 ⊆ 𝐵 → 𝐴 ⊆ (𝐵 ∪ 𝐶))
Theorem	ssun4 4122	Subclass law for union of classes. (Contributed by NM, 14-Aug-1994.)
⊢ (𝐴 ⊆ 𝐵 → 𝐴 ⊆ (𝐶 ∪ 𝐵))
Theorem	elun1 4123	Membership law for union of classes. (Contributed by NM, 5-Aug-1993.)
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ (𝐵 ∪ 𝐶))
Theorem	elun2 4124	Membership law for union of classes. (Contributed by NM, 30-Aug-1993.)
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ (𝐶 ∪ 𝐵))
Theorem	elunant 4125	A statement is true for every element of the union of a pair of classes if and only if it is true for every element of the first class and for every element of the second class. (Contributed by BTernaryTau, 27-Sep-2023.)
⊢ ((𝐶 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ((𝐶 ∈ 𝐴 → 𝜑) ∧ (𝐶 ∈ 𝐵 → 𝜑)))
Theorem	unss1 4126	Subclass law for union of classes. (Contributed by NM, 14-Oct-1999.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐶))
Theorem	ssequn1 4127	A relationship between subclass and union. Theorem 26 of [Suppes] p. 27. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
Theorem	unss2 4128	Subclass law for union of classes. Exercise 7 of [TakeutiZaring] p. 18. (Contributed by NM, 14-Oct-1999.)
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∪ 𝐴) ⊆ (𝐶 ∪ 𝐵))
Theorem	unss12 4129	Subclass law for union of classes. (Contributed by NM, 2-Jun-2004.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐷))
Theorem	ssequn2 4130	A relationship between subclass and union. (Contributed by NM, 13-Jun-1994.)
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵)
Theorem	unss 4131	The union of two subclasses is a subclass. Theorem 27 of [Suppes] p. 27 and its converse. (Contributed by NM, 11-Jun-2004.)
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶)
Theorem	unssi 4132	An inference showing the union of two subclasses is a subclass. (Contributed by Raph Levien, 10-Dec-2002.)
⊢ 𝐴 ⊆ 𝐶    &   ⊢ 𝐵 ⊆ 𝐶    ⇒   ⊢ (𝐴 ∪ 𝐵) ⊆ 𝐶
Theorem	unssd 4133	A deduction showing the union of two subclasses is a subclass. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 → 𝐴 ⊆ 𝐶)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶)
Theorem	unssad 4134	If (𝐴 ∪ 𝐵) is contained in 𝐶, so is 𝐴. One-way deduction form of unss 4131. Partial converse of unssd 4133. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	unssbd 4135	If (𝐴 ∪ 𝐵) is contained in 𝐶, so is 𝐵. One-way deduction form of unss 4131. Partial converse of unssd 4133. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶)    ⇒   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
Theorem	ssun 4136	A condition that implies inclusion in the union of two classes. (Contributed by NM, 23-Nov-2003.)
⊢ ((𝐴 ⊆ 𝐵 ∨ 𝐴 ⊆ 𝐶) → 𝐴 ⊆ (𝐵 ∪ 𝐶))
Theorem	rexun 4137	Restricted existential quantification over union. (Contributed by Jeff Madsen, 5-Jan-2011.)
⊢ (∃𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐵 𝜑))
Theorem	ralunb 4138	Restricted quantification over a union. (Contributed by Scott Fenton, 12-Apr-2011.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑))
Theorem	ralun 4139	Restricted quantification over union. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑) → ∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑)
2.1.13.3  The intersection of two classes
Theorem	elini 4140	Membership in an intersection of two classes. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ 𝐴 ∈ 𝐵    &   ⊢ 𝐴 ∈ 𝐶    ⇒   ⊢ 𝐴 ∈ (𝐵 ∩ 𝐶)
Theorem	elind 4141	Deduce membership in an intersection of two classes. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵))
Theorem	elinel1 4142	Membership in an intersection implies membership in the first set. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ 𝐵)
Theorem	elinel2 4143	Membership in an intersection implies membership in the second set. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ 𝐶)
Theorem	elin2 4144	Membership in a class defined as an intersection. (Contributed by Stefan O'Rear, 29-Mar-2015.)
⊢ 𝑋 = (𝐵 ∩ 𝐶)    ⇒   ⊢ (𝐴 ∈ 𝑋 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))
Theorem	elin1d 4145	Elementhood in the first set of an intersection - deduction version. (Contributed by Thierry Arnoux, 3-May-2020.)
⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵))    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝐴)
Theorem	elin2d 4146	Elementhood in the first set of an intersection - deduction version. (Contributed by Thierry Arnoux, 3-May-2020.)
⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵))    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝐵)
Theorem	elin3 4147	Membership in a class defined as a ternary intersection. (Contributed by Stefan O'Rear, 29-Mar-2015.)
⊢ 𝑋 = ((𝐵 ∩ 𝐶) ∩ 𝐷)    ⇒   ⊢ (𝐴 ∈ 𝑋 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶 ∧ 𝐴 ∈ 𝐷))
Theorem	nel1nelin 4148	Membership in an intersection implies membership in the first set. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (¬ 𝐴 ∈ 𝐵 → ¬ 𝐴 ∈ (𝐵 ∩ 𝐶))
Theorem	nel2nelin 4149	Membership in an intersection implies membership in the second set. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (¬ 𝐴 ∈ 𝐶 → ¬ 𝐴 ∈ (𝐵 ∩ 𝐶))
Theorem	incom 4150	Commutative law for intersection of classes. Exercise 7 of [TakeutiZaring] p. 17. (Contributed by NM, 21-Jun-1993.) (Proof shortened by SN, 12-Dec-2023.)
⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴)
Theorem	ineqcom 4151	Two ways of expressing that two classes have a given intersection. This is often used when that given intersection is the empty set, in which case the statement displays two ways of expressing that two classes are disjoint (when 𝐶 = ∅: ((𝐴 ∩ 𝐵) = ∅ ↔ (𝐵 ∩ 𝐴) = ∅)). (Contributed by Peter Mazsa, 22-Mar-2017.)
⊢ ((𝐴 ∩ 𝐵) = 𝐶 ↔ (𝐵 ∩ 𝐴) = 𝐶)
Theorem	ineqcomi 4152	Two ways of expressing that two classes have a given intersection. Inference form of ineqcom 4151. Disjointness inference when 𝐶 = ∅. (Contributed by Peter Mazsa, 26-Mar-2017.) (Proof shortened by SN, 20-Sep-2024.)
⊢ (𝐴 ∩ 𝐵) = 𝐶    ⇒   ⊢ (𝐵 ∩ 𝐴) = 𝐶
Theorem	ineqri 4153*	Inference from membership to intersection. (Contributed by NM, 21-Jun-1993.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐶)    ⇒   ⊢ (𝐴 ∩ 𝐵) = 𝐶
Theorem	ineq1 4154	Equality theorem for intersection of two classes. (Contributed by NM, 14-Dec-1993.) (Proof shortened by SN, 20-Sep-2023.)
⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))
Theorem	ineq2 4155	Equality theorem for intersection of two classes. (Contributed by NM, 26-Dec-1993.)
⊢ (𝐴 = 𝐵 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵))
Theorem	ineq12 4156	Equality theorem for intersection of two classes. (Contributed by NM, 8-May-1994.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷))
Theorem	ineq1i 4157	Equality inference for intersection of two classes. (Contributed by NM, 26-Dec-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)
Theorem	ineq2i 4158	Equality inference for intersection of two classes. (Contributed by NM, 26-Dec-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵)
Theorem	ineq12i 4159	Equality inference for intersection of two classes. (Contributed by NM, 24-Jun-2004.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)
Theorem	ineq1d 4160	Equality deduction for intersection of two classes. (Contributed by NM, 10-Apr-1994.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))
Theorem	ineq2d 4161	Equality deduction for intersection of two classes. (Contributed by NM, 10-Apr-1994.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵))
Theorem	ineq12d 4162	Equality deduction for intersection of two classes. (Contributed by NM, 24-Jun-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷))
Theorem	ineqan12d 4163	Equality deduction for intersection of two classes. (Contributed by NM, 7-Feb-2007.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜓 → 𝐶 = 𝐷)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷))
Theorem	sseqin2 4164	A relationship between subclass and intersection. Similar to Exercise 9 of [TakeutiZaring] p. 18. (Contributed by NM, 17-May-1994.)
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∩ 𝐴) = 𝐴)
Theorem	nfin 4165	Bound-variable hypothesis builder for the intersection of classes. (Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro, 14-Oct-2016.) Avoid ax-10 2147, ax-11 2163, ax-12 2185. (Revised by SN, 14-May-2025.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝐴 ∩ 𝐵)
Theorem	nfinOLD 4166	Obsolete version of nfin 4165 as of 14-May-2025. (Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro, 14-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝐴 ∩ 𝐵)
Theorem	rabbi2dva 4167*	Deduction from a wff to a restricted class abstraction. (Contributed by NM, 14-Jan-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐵 ↔ 𝜓))    ⇒   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝜓})
Theorem	inidm 4168	Idempotent law for intersection of classes. Theorem 15 of [Suppes] p. 26. (Contributed by NM, 5-Aug-1993.)
⊢ (𝐴 ∩ 𝐴) = 𝐴
Theorem	inass 4169	Associative law for intersection of classes. Exercise 9 of [TakeutiZaring] p. 17. (Contributed by NM, 3-May-1994.)
⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = (𝐴 ∩ (𝐵 ∩ 𝐶))
Theorem	in12 4170	A rearrangement of intersection. (Contributed by NM, 21-Apr-2001.)
⊢ (𝐴 ∩ (𝐵 ∩ 𝐶)) = (𝐵 ∩ (𝐴 ∩ 𝐶))
Theorem	in32 4171	A rearrangement of intersection. (Contributed by NM, 21-Apr-2001.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∩ 𝐵)
Theorem	in13 4172	A rearrangement of intersection. (Contributed by NM, 27-Aug-2012.)
⊢ (𝐴 ∩ (𝐵 ∩ 𝐶)) = (𝐶 ∩ (𝐵 ∩ 𝐴))
Theorem	in31 4173	A rearrangement of intersection. (Contributed by NM, 27-Aug-2012.)
⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = ((𝐶 ∩ 𝐵) ∩ 𝐴)
Theorem	inrot 4174	Rotate the intersection of 3 classes. (Contributed by NM, 27-Aug-2012.)
⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = ((𝐶 ∩ 𝐴) ∩ 𝐵)
Theorem	in4 4175	Rearrangement of intersection of 4 classes. (Contributed by NM, 21-Apr-2001.)
⊢ ((𝐴 ∩ 𝐵) ∩ (𝐶 ∩ 𝐷)) = ((𝐴 ∩ 𝐶) ∩ (𝐵 ∩ 𝐷))
Theorem	inindi 4176	Intersection distributes over itself. (Contributed by NM, 6-May-1994.)
⊢ (𝐴 ∩ (𝐵 ∩ 𝐶)) = ((𝐴 ∩ 𝐵) ∩ (𝐴 ∩ 𝐶))
Theorem	inindir 4177	Intersection distributes over itself. (Contributed by NM, 17-Aug-2004.)
⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∩ (𝐵 ∩ 𝐶))
Theorem	inss1 4178	The intersection of two classes is a subset of one of them. Part of Exercise 12 of [TakeutiZaring] p. 18. (Contributed by NM, 27-Apr-1994.)
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴
Theorem	inss2 4179	The intersection of two classes is a subset of one of them. Part of Exercise 12 of [TakeutiZaring] p. 18. (Contributed by NM, 27-Apr-1994.)
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵
Theorem	ssin 4180	Subclass of intersection. Theorem 2.8(vii) of [Monk1] p. 26. (Contributed by NM, 15-Jun-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶) ↔ 𝐴 ⊆ (𝐵 ∩ 𝐶))
Theorem	ssini 4181	An inference showing that a subclass of two classes is a subclass of their intersection. (Contributed by NM, 24-Nov-2003.)
⊢ 𝐴 ⊆ 𝐵    &   ⊢ 𝐴 ⊆ 𝐶    ⇒   ⊢ 𝐴 ⊆ (𝐵 ∩ 𝐶)
Theorem	ssind 4182	A deduction showing that a subclass of two classes is a subclass of their intersection. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ (𝐵 ∩ 𝐶))
Theorem	ssrin 4183	Add right intersection to subclass relation. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶))
Theorem	sslin 4184	Add left intersection to subclass relation. (Contributed by NM, 19-Oct-1999.)
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∩ 𝐴) ⊆ (𝐶 ∩ 𝐵))
Theorem	ssrind 4185	Add right intersection to subclass relation. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶))
Theorem	ss2in 4186	Intersection of subclasses. (Contributed by NM, 5-May-2000.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐷))
Theorem	ssinss1 4187	Intersection preserves subclass relationship. (Contributed by NM, 14-Sep-1999.)
⊢ (𝐴 ⊆ 𝐶 → (𝐴 ∩ 𝐵) ⊆ 𝐶)
Theorem	ssinss1d 4188	Intersection preserves subclass relationship. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → (𝐴 ∩ 𝐵) ⊆ 𝐶)
Theorem	inss 4189	Inclusion of an intersection of two classes. (Contributed by NM, 30-Oct-2014.)
⊢ ((𝐴 ⊆ 𝐶 ∨ 𝐵 ⊆ 𝐶) → (𝐴 ∩ 𝐵) ⊆ 𝐶)
Theorem	ralin 4190	Restricted universal quantification over intersection. (Contributed by Peter Mazsa, 8-Sep-2023.)
⊢ (∀𝑥 ∈ (𝐴 ∩ 𝐵)𝜑 ↔ ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝐵 → 𝜑))
Theorem	rexin 4191	Restricted existential quantification over intersection. (Contributed by Peter Mazsa, 17-Dec-2018.)
⊢ (∃𝑥 ∈ (𝐴 ∩ 𝐵)𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝑥 ∈ 𝐵 ∧ 𝜑))
Theorem	dfss7 4192*	Alternate definition of subclass relationship. (Contributed by AV, 1-Aug-2022.)
⊢ (𝐵 ⊆ 𝐴 ↔ {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵} = 𝐵)
2.1.13.4  The symmetric difference of two classes
Syntax	csymdif 4193	Declare the syntax for symmetric difference.
class (𝐴 △ 𝐵)
Definition	df-symdif 4194	Define the symmetric difference of two classes. Alternate definitions are dfsymdif2 4202, dfsymdif3 4247 and dfsymdif4 4200. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ (𝐴 △ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐴))
Theorem	symdifcom 4195	Symmetric difference commutes. (Contributed by Scott Fenton, 24-Apr-2012.)
⊢ (𝐴 △ 𝐵) = (𝐵 △ 𝐴)
Theorem	symdifeq1 4196	Equality theorem for symmetric difference. (Contributed by Scott Fenton, 24-Apr-2012.)
⊢ (𝐴 = 𝐵 → (𝐴 △ 𝐶) = (𝐵 △ 𝐶))
Theorem	symdifeq2 4197	Equality theorem for symmetric difference. (Contributed by Scott Fenton, 24-Apr-2012.)
⊢ (𝐴 = 𝐵 → (𝐶 △ 𝐴) = (𝐶 △ 𝐵))
Theorem	nfsymdif 4198	Hypothesis builder for symmetric difference. (Contributed by Scott Fenton, 19-Feb-2013.) (Revised by Mario Carneiro, 11-Dec-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝐴 △ 𝐵)
Theorem	elsymdif 4199	Membership in a symmetric difference. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ (𝐴 ∈ (𝐵 △ 𝐶) ↔ ¬ (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 𝐶))
Theorem	dfsymdif4 4200*	Alternate definition of the symmetric difference. (Contributed by NM, 17-Aug-2004.) (Revised by AV, 17-Aug-2022.)
⊢ (𝐴 △ 𝐵) = {𝑥 ∣ ¬ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)}