P. 33 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 3201-3300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	eqimss 3201	Equality implies the subclass relation. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)
⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
Theorem	eqimss2 3202	Equality implies the subclass relation. (Contributed by NM, 23-Nov-2003.)
⊢ (𝐵 = 𝐴 → 𝐴 ⊆ 𝐵)
Theorem	eqimssi 3203	Infer subclass relationship from equality. (Contributed by NM, 6-Jan-2007.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ 𝐴 ⊆ 𝐵
Theorem	eqimss2i 3204	Infer subclass relationship from equality. (Contributed by NM, 7-Jan-2007.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ 𝐵 ⊆ 𝐴
Theorem	nssne1 3205	Two classes are different if they don't include the same class. (Contributed by NM, 23-Apr-2015.)
⊢ ((𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 ⊆ 𝐶) → 𝐵 ≠ 𝐶)
Theorem	nssne2 3206	Two classes are different if they are not subclasses of the same class. (Contributed by NM, 23-Apr-2015.)
⊢ ((𝐴 ⊆ 𝐶 ∧ ¬ 𝐵 ⊆ 𝐶) → 𝐴 ≠ 𝐵)
Theorem	nssr 3207*	Negation of subclass relationship. One direction of Exercise 13 of [TakeutiZaring] p. 18. (Contributed by Jim Kingdon, 15-Jul-2018.)
⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) → ¬ 𝐴 ⊆ 𝐵)
Theorem	nelss 3208	Demonstrate by witnesses that two classes lack a subclass relation. (Contributed by Stefan O'Rear, 5-Feb-2015.)
⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → ¬ 𝐵 ⊆ 𝐶)
Theorem	ssrexf 3209	Restricted existential quantification follows from a subclass relationship. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜑))
Theorem	ssrmof 3210	"At most one" existential quantification restricted to a subclass. (Contributed by Thierry Arnoux, 8-Oct-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 ⊆ 𝐵 → (∃*𝑥 ∈ 𝐵 𝜑 → ∃*𝑥 ∈ 𝐴 𝜑))
Theorem	ssralv 3211*	Quantification restricted to a subclass. (Contributed by NM, 11-Mar-2006.)
⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 𝜑))
Theorem	ssrexv 3212*	Existential quantification restricted to a subclass. (Contributed by NM, 11-Jan-2007.)
⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜑))
Theorem	ralss 3213*	Restricted universal quantification on a subset in terms of superset. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 (𝑥 ∈ 𝐴 → 𝜑)))
Theorem	rexss 3214*	Restricted existential quantification on a subset in terms of superset. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 (𝑥 ∈ 𝐴 ∧ 𝜑)))
Theorem	ss2ab 3215	Class abstractions in a subclass relationship. (Contributed by NM, 3-Jul-1994.)
⊢ ({𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓} ↔ ∀𝑥(𝜑 → 𝜓))
Theorem	abss 3216*	Class abstraction in a subclass relationship. (Contributed by NM, 16-Aug-2006.)
⊢ ({𝑥 ∣ 𝜑} ⊆ 𝐴 ↔ ∀𝑥(𝜑 → 𝑥 ∈ 𝐴))
Theorem	ssab 3217*	Subclass of a class abstraction. (Contributed by NM, 16-Aug-2006.)
⊢ (𝐴 ⊆ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
Theorem	ssabral 3218*	The relation for a subclass of a class abstraction is equivalent to restricted quantification. (Contributed by NM, 6-Sep-2006.)
⊢ (𝐴 ⊆ {𝑥 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐴 𝜑)
Theorem	ss2abi 3219	Inference of abstraction subclass from implication. (Contributed by NM, 31-Mar-1995.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓}
Theorem	ss2abdv 3220*	Deduction of abstraction subclass from implication. (Contributed by NM, 29-Jul-2011.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ {𝑥 ∣ 𝜒})
Theorem	abssdv 3221*	Deduction of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006.)
⊢ (𝜑 → (𝜓 → 𝑥 ∈ 𝐴))    ⇒   ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ 𝐴)
Theorem	abssi 3222*	Inference of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006.)
⊢ (𝜑 → 𝑥 ∈ 𝐴)    ⇒   ⊢ {𝑥 ∣ 𝜑} ⊆ 𝐴
Theorem	ss2rab 3223	Restricted abstraction classes in a subclass relationship. (Contributed by NM, 30-May-1999.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓} ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
Theorem	rabss 3224*	Restricted class abstraction in a subclass relationship. (Contributed by NM, 16-Aug-2006.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 ∈ 𝐵))
Theorem	ssrab 3225*	Subclass of a restricted class abstraction. (Contributed by NM, 16-Aug-2006.)
⊢ (𝐵 ⊆ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ (𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 𝜑))
Theorem	ssrabdv 3226*	Subclass of a restricted class abstraction (deduction form). (Contributed by NM, 31-Aug-2006.)
⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝜓)    ⇒   ⊢ (𝜑 → 𝐵 ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓})
Theorem	rabssdv 3227*	Subclass of a restricted class abstraction (deduction form). (Contributed by NM, 2-Feb-2015.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝜓) → 𝑥 ∈ 𝐵)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ 𝐵)
Theorem	ss2rabdv 3228*	Deduction of restricted abstraction subclass from implication. (Contributed by NM, 30-May-2006.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜒})
Theorem	ss2rabi 3229	Inference of restricted abstraction subclass from implication. (Contributed by NM, 14-Oct-1999.)
⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓}
Theorem	rabss2 3230*	Subclass law for restricted abstraction. (Contributed by NM, 18-Dec-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝐴 ⊆ 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐵 ∣ 𝜑})
Theorem	ssab2 3231*	Subclass relation for the restriction of a class abstraction. (Contributed by NM, 31-Mar-1995.)
⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ 𝐴
Theorem	ssrab2 3232*	Subclass relation for a restricted class. (Contributed by NM, 19-Mar-1997.)
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴
Theorem	ssrab3 3233*	Subclass relation for a restricted class abstraction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜑}    ⇒   ⊢ 𝐵 ⊆ 𝐴
Theorem	ssrabeq 3234*	If the restricting class of a restricted class abstraction is a subset of this restricted class abstraction, it is equal to this restricted class abstraction. (Contributed by Alexander van der Vekens, 31-Dec-2017.)
⊢ (𝑉 ⊆ {𝑥 ∈ 𝑉 ∣ 𝜑} ↔ 𝑉 = {𝑥 ∈ 𝑉 ∣ 𝜑})
Theorem	rabssab 3235	A restricted class is a subclass of the corresponding unrestricted class. (Contributed by Mario Carneiro, 23-Dec-2016.)
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜑}
Theorem	uniiunlem 3236*	A subset relationship useful for converting union to indexed union using dfiun2 or dfiun2g and intersection to indexed intersection using dfiin2 . (Contributed by NM, 5-Oct-2006.) (Proof shortened by Mario Carneiro, 26-Sep-2015.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐷 → (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ⊆ 𝐶))
2.1.13  The difference, union, and intersection of two classes
2.1.13.1  The difference of two classes
Theorem	dfdif3 3237*	Alternate definition of class difference. Definition of relative set complement in Section 2.3 of [Pierik], p. 10. (Contributed by BJ and Jim Kingdon, 16-Jun-2022.)
⊢ (𝐴 ∖ 𝐵) = {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐵 𝑥 ≠ 𝑦}
Theorem	difeq1 3238	Equality theorem for class difference. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝐴 = 𝐵 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶))
Theorem	difeq2 3239	Equality theorem for class difference. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝐴 = 𝐵 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵))
Theorem	difeq12 3240	Equality theorem for class difference. (Contributed by FL, 31-Aug-2009.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐷))
Theorem	difeq1i 3241	Inference adding difference to the right in a class equality. (Contributed by NM, 15-Nov-2002.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶)
Theorem	difeq2i 3242	Inference adding difference to the left in a class equality. (Contributed by NM, 15-Nov-2002.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵)
Theorem	difeq12i 3243	Equality inference for class difference. (Contributed by NM, 29-Aug-2004.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐷)
Theorem	difeq1d 3244	Deduction adding difference to the right in a class equality. (Contributed by NM, 15-Nov-2002.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶))
Theorem	difeq2d 3245	Deduction adding difference to the left in a class equality. (Contributed by NM, 15-Nov-2002.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵))
Theorem	difeq12d 3246	Equality deduction for class difference. (Contributed by FL, 29-May-2014.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐷))
Theorem	difeqri 3247*	Inference from membership to difference. (Contributed by NM, 17-May-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐶)    ⇒   ⊢ (𝐴 ∖ 𝐵) = 𝐶
Theorem	nfdif 3248	Bound-variable hypothesis builder for class difference. (Contributed by NM, 3-Dec-2003.) (Revised by Mario Carneiro, 13-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝐴 ∖ 𝐵)
Theorem	eldifi 3249	Implication of membership in a class difference. (Contributed by NM, 29-Apr-1994.)
⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ 𝐵)
Theorem	eldifn 3250	Implication of membership in a class difference. (Contributed by NM, 3-May-1994.)
⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → ¬ 𝐴 ∈ 𝐶)
Theorem	elndif 3251	A set does not belong to a class excluding it. (Contributed by NM, 27-Jun-1994.)
⊢ (𝐴 ∈ 𝐵 → ¬ 𝐴 ∈ (𝐶 ∖ 𝐵))
Theorem	difdif 3252	Double class difference. Exercise 11 of [TakeutiZaring] p. 22. (Contributed by NM, 17-May-1998.)
⊢ (𝐴 ∖ (𝐵 ∖ 𝐴)) = 𝐴
Theorem	difss 3253	Subclass relationship for class difference. Exercise 14 of [TakeutiZaring] p. 22. (Contributed by NM, 29-Apr-1994.)
⊢ (𝐴 ∖ 𝐵) ⊆ 𝐴
Theorem	difssd 3254	A difference of two classes is contained in the minuend. Deduction form of difss 3253. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → (𝐴 ∖ 𝐵) ⊆ 𝐴)
Theorem	difss2 3255	If a class is contained in a difference, it is contained in the minuend. (Contributed by David Moews, 1-May-2017.)
⊢ (𝐴 ⊆ (𝐵 ∖ 𝐶) → 𝐴 ⊆ 𝐵)
Theorem	difss2d 3256	If a class is contained in a difference, it is contained in the minuend. Deduction form of difss2 3255. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊆ (𝐵 ∖ 𝐶))    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
Theorem	ssdifss 3257	Preservation of a subclass relationship by class difference. (Contributed by NM, 15-Feb-2007.)
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ 𝐵)
Theorem	ddifnel 3258*	Double complement under universal class. The hypothesis corresponds to stability of membership in 𝐴, which is weaker than decidability (see dcstab 839). Actually, the conclusion is a characterization of stability of membership in a class (see ddifstab 3259) . Exercise 4.10(s) of [Mendelson] p. 231, but with an additional hypothesis. For a version without a hypothesis, but which only states that 𝐴 is a subset of V ∖ (V ∖ 𝐴), see ddifss 3365. (Contributed by Jim Kingdon, 21-Jul-2018.)
⊢ (¬ 𝑥 ∈ (V ∖ 𝐴) → 𝑥 ∈ 𝐴)    ⇒   ⊢ (V ∖ (V ∖ 𝐴)) = 𝐴
Theorem	ddifstab 3259*	A class is equal to its double complement if and only if it is stable (that is, membership in it is a stable property). (Contributed by BJ, 12-Dec-2021.)
⊢ ((V ∖ (V ∖ 𝐴)) = 𝐴 ↔ ∀𝑥STAB 𝑥 ∈ 𝐴)
Theorem	ssconb 3260	Contraposition law for subsets. (Contributed by NM, 22-Mar-1998.)
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → (𝐴 ⊆ (𝐶 ∖ 𝐵) ↔ 𝐵 ⊆ (𝐶 ∖ 𝐴)))
Theorem	sscon 3261	Contraposition law for subsets. Exercise 15 of [TakeutiZaring] p. 22. (Contributed by NM, 22-Mar-1998.)
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∖ 𝐵) ⊆ (𝐶 ∖ 𝐴))
Theorem	ssdif 3262	Difference law for subsets. (Contributed by NM, 28-May-1998.)
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶))
Theorem	ssdifd 3263	If 𝐴 is contained in 𝐵, then (𝐴 ∖ 𝐶) is contained in (𝐵 ∖ 𝐶). Deduction form of ssdif 3262. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶))
Theorem	sscond 3264	If 𝐴 is contained in 𝐵, then (𝐶 ∖ 𝐵) is contained in (𝐶 ∖ 𝐴). Deduction form of sscon 3261. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ∖ 𝐵) ⊆ (𝐶 ∖ 𝐴))
Theorem	ssdifssd 3265	If 𝐴 is contained in 𝐵, then (𝐴 ∖ 𝐶) is also contained in 𝐵. Deduction form of ssdifss 3257. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ∖ 𝐶) ⊆ 𝐵)
Theorem	ssdif2d 3266	If 𝐴 is contained in 𝐵 and 𝐶 is contained in 𝐷, then (𝐴 ∖ 𝐷) is contained in (𝐵 ∖ 𝐶). Deduction form. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ∖ 𝐷) ⊆ (𝐵 ∖ 𝐶))
Theorem	raldifb 3267	Restricted universal quantification on a class difference in terms of an implication. (Contributed by Alexander van der Vekens, 3-Jan-2018.)
⊢ (∀𝑥 ∈ 𝐴 (𝑥 ∉ 𝐵 → 𝜑) ↔ ∀𝑥 ∈ (𝐴 ∖ 𝐵)𝜑)
2.1.13.2  The union of two classes
Theorem	elun 3268	Expansion of membership in class union. Theorem 12 of [Suppes] p. 25. (Contributed by NM, 7-Aug-1994.)
⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))
Theorem	uneqri 3269*	Inference from membership to union. (Contributed by NM, 5-Aug-1993.)
⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐶)    ⇒   ⊢ (𝐴 ∪ 𝐵) = 𝐶
Theorem	unidm 3270	Idempotent law for union of classes. Theorem 23 of [Suppes] p. 27. (Contributed by NM, 5-Aug-1993.)
⊢ (𝐴 ∪ 𝐴) = 𝐴
Theorem	uncom 3271	Commutative law for union of classes. Exercise 6 of [TakeutiZaring] p. 17. (Contributed by NM, 25-Jun-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
Theorem	equncom 3272	If a class equals the union of two other classes, then it equals the union of those two classes commuted. (Contributed by Alan Sare, 18-Feb-2012.)
⊢ (𝐴 = (𝐵 ∪ 𝐶) ↔ 𝐴 = (𝐶 ∪ 𝐵))
Theorem	equncomi 3273	Inference form of equncom 3272. (Contributed by Alan Sare, 18-Feb-2012.)
⊢ 𝐴 = (𝐵 ∪ 𝐶)    ⇒   ⊢ 𝐴 = (𝐶 ∪ 𝐵)
Theorem	uneq1 3274	Equality theorem for union of two classes. (Contributed by NM, 5-Aug-1993.)
⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))
Theorem	uneq2 3275	Equality theorem for the union of two classes. (Contributed by NM, 5-Aug-1993.)
⊢ (𝐴 = 𝐵 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵))
Theorem	uneq12 3276	Equality theorem for union of two classes. (Contributed by NM, 29-Mar-1998.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷))
Theorem	uneq1i 3277	Inference adding union to the right in a class equality. (Contributed by NM, 30-Aug-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶)
Theorem	uneq2i 3278	Inference adding union to the left in a class equality. (Contributed by NM, 30-Aug-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵)
Theorem	uneq12i 3279	Equality inference for union of two classes. (Contributed by NM, 12-Aug-2004.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷)
Theorem	uneq1d 3280	Deduction adding union to the right in a class equality. (Contributed by NM, 29-Mar-1998.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))
Theorem	uneq2d 3281	Deduction adding union to the left in a class equality. (Contributed by NM, 29-Mar-1998.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵))
Theorem	uneq12d 3282	Equality deduction for union of two classes. (Contributed by NM, 29-Sep-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷))
Theorem	nfun 3283	Bound-variable hypothesis builder for the union of classes. (Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro, 14-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝐴 ∪ 𝐵)
Theorem	unass 3284	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 3285	A rearrangement of union. (Contributed by NM, 12-Aug-2004.)
⊢ (𝐴 ∪ (𝐵 ∪ 𝐶)) = (𝐵 ∪ (𝐴 ∪ 𝐶))
Theorem	un23 3286	A rearrangement of union. (Contributed by NM, 12-Aug-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ((𝐴 ∪ 𝐵) ∪ 𝐶) = ((𝐴 ∪ 𝐶) ∪ 𝐵)
Theorem	un4 3287	A rearrangement of the union of 4 classes. (Contributed by NM, 12-Aug-2004.)
⊢ ((𝐴 ∪ 𝐵) ∪ (𝐶 ∪ 𝐷)) = ((𝐴 ∪ 𝐶) ∪ (𝐵 ∪ 𝐷))
Theorem	unundi 3288	Union distributes over itself. (Contributed by NM, 17-Aug-2004.)
⊢ (𝐴 ∪ (𝐵 ∪ 𝐶)) = ((𝐴 ∪ 𝐵) ∪ (𝐴 ∪ 𝐶))
Theorem	unundir 3289	Union distributes over itself. (Contributed by NM, 17-Aug-2004.)
⊢ ((𝐴 ∪ 𝐵) ∪ 𝐶) = ((𝐴 ∪ 𝐶) ∪ (𝐵 ∪ 𝐶))
Theorem	ssun1 3290	Subclass relationship for union of classes. Theorem 25 of [Suppes] p. 27. (Contributed by NM, 5-Aug-1993.)
⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
Theorem	ssun2 3291	Subclass relationship for union of classes. (Contributed by NM, 30-Aug-1993.)
⊢ 𝐴 ⊆ (𝐵 ∪ 𝐴)
Theorem	ssun3 3292	Subclass law for union of classes. (Contributed by NM, 5-Aug-1993.)
⊢ (𝐴 ⊆ 𝐵 → 𝐴 ⊆ (𝐵 ∪ 𝐶))
Theorem	ssun4 3293	Subclass law for union of classes. (Contributed by NM, 14-Aug-1994.)
⊢ (𝐴 ⊆ 𝐵 → 𝐴 ⊆ (𝐶 ∪ 𝐵))
Theorem	elun1 3294	Membership law for union of classes. (Contributed by NM, 5-Aug-1993.)
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ (𝐵 ∪ 𝐶))
Theorem	elun2 3295	Membership law for union of classes. (Contributed by NM, 30-Aug-1993.)
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ (𝐶 ∪ 𝐵))
Theorem	unss1 3296	Subclass law for union of classes. (Contributed by NM, 14-Oct-1999.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐶))
Theorem	ssequn1 3297	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 3298	Subclass law for union of classes. Exercise 7 of [TakeutiZaring] p. 18. (Contributed by NM, 14-Oct-1999.)
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∪ 𝐴) ⊆ (𝐶 ∪ 𝐵))
Theorem	unss12 3299	Subclass law for union of classes. (Contributed by NM, 2-Jun-2004.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐷))
Theorem	ssequn2 3300	A relationship between subclass and union. (Contributed by NM, 13-Jun-1994.)
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵)