P. 31 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 3001-3100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rexss 3001*	Restricted existential quantification on a subset in terms of superset. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ (A ⊆ B → (∃x ∈ A φ ↔ ∃x ∈ B (x ∈ A ∧ φ)))
Theorem	ss2ab 3002	Class abstractions in a subclass relationship. (Contributed by NM, 3-Jul-1994.)
⊢ ({x ∣ φ} ⊆ {x ∣ ψ} ↔ ∀x(φ → ψ))
Theorem	abss 3003*	Class abstraction in a subclass relationship. (Contributed by NM, 16-Aug-2006.)
⊢ ({x ∣ φ} ⊆ A ↔ ∀x(φ → x ∈ A))
Theorem	ssab 3004*	Subclass of a class abstraction. (Contributed by NM, 16-Aug-2006.)
⊢ (A ⊆ {x ∣ φ} ↔ ∀x(x ∈ A → φ))
Theorem	ssabral 3005*	The relation for a subclass of a class abstraction is equivalent to restricted quantification. (Contributed by NM, 6-Sep-2006.)
⊢ (A ⊆ {x ∣ φ} ↔ ∀x ∈ A φ)
Theorem	ss2abi 3006	Inference of abstraction subclass from implication. (Contributed by NM, 31-Mar-1995.)
⊢ (φ → ψ)    ⇒   ⊢ {x ∣ φ} ⊆ {x ∣ ψ}
Theorem	ss2abdv 3007*	Deduction of abstraction subclass from implication. (Contributed by NM, 29-Jul-2011.)
⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → {x ∣ ψ} ⊆ {x ∣ χ})
Theorem	abssdv 3008*	Deduction of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006.)
⊢ (φ → (ψ → x ∈ A))    ⇒   ⊢ (φ → {x ∣ ψ} ⊆ A)
Theorem	abssi 3009*	Inference of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006.)
⊢ (φ → x ∈ A)    ⇒   ⊢ {x ∣ φ} ⊆ A
Theorem	ss2rab 3010	Restricted abstraction classes in a subclass relationship. (Contributed by NM, 30-May-1999.)
⊢ ({x ∈ A ∣ φ} ⊆ {x ∈ A ∣ ψ} ↔ ∀x ∈ A (φ → ψ))
Theorem	rabss 3011*	Restricted class abstraction in a subclass relationship. (Contributed by NM, 16-Aug-2006.)
⊢ ({x ∈ A ∣ φ} ⊆ B ↔ ∀x ∈ A (φ → x ∈ B))
Theorem	ssrab 3012*	Subclass of a restricted class abstraction. (Contributed by NM, 16-Aug-2006.)
⊢ (B ⊆ {x ∈ A ∣ φ} ↔ (B ⊆ A ∧ ∀x ∈ B φ))
Theorem	ssrabdv 3013*	Subclass of a restricted class abstraction (deduction rule). (Contributed by NM, 31-Aug-2006.)
⊢ (φ → B ⊆ A)    &   ⊢ ((φ ∧ x ∈ B) → ψ)    ⇒   ⊢ (φ → B ⊆ {x ∈ A ∣ ψ})
Theorem	rabssdv 3014*	Subclass of a restricted class abstraction (deduction rule). (Contributed by NM, 2-Feb-2015.)
⊢ ((φ ∧ x ∈ A ∧ ψ) → x ∈ B)    ⇒   ⊢ (φ → {x ∈ A ∣ ψ} ⊆ B)
Theorem	ss2rabdv 3015*	Deduction of restricted abstraction subclass from implication. (Contributed by NM, 30-May-2006.)
⊢ ((φ ∧ x ∈ A) → (ψ → χ))    ⇒   ⊢ (φ → {x ∈ A ∣ ψ} ⊆ {x ∈ A ∣ χ})
Theorem	ss2rabi 3016	Inference of restricted abstraction subclass from implication. (Contributed by NM, 14-Oct-1999.)
⊢ (x ∈ A → (φ → ψ))    ⇒   ⊢ {x ∈ A ∣ φ} ⊆ {x ∈ A ∣ ψ}
Theorem	rabss2 3017*	Subclass law for restricted abstraction. (Contributed by NM, 18-Dec-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (A ⊆ B → {x ∈ A ∣ φ} ⊆ {x ∈ B ∣ φ})
Theorem	ssab2 3018*	Subclass relation for the restriction of a class abstraction. (Contributed by NM, 31-Mar-1995.)
⊢ {x ∣ (x ∈ A ∧ φ)} ⊆ A
Theorem	ssrab2 3019*	Subclass relation for a restricted class. (Contributed by NM, 19-Mar-1997.)
⊢ {x ∈ A ∣ φ} ⊆ A
Theorem	ssrabeq 3020*	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.)
⊢ (𝑉 ⊆ {x ∈ 𝑉 ∣ φ} ↔ 𝑉 = {x ∈ 𝑉 ∣ φ})
Theorem	rabssab 3021	A restricted class is a subclass of the corresponding unrestricted class. (Contributed by Mario Carneiro, 23-Dec-2016.)
⊢ {x ∈ A ∣ φ} ⊆ {x ∣ φ}
Theorem	uniiunlem 3022*	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.)
⊢ (∀x ∈ A B ∈ 𝐷 → (∀x ∈ A B ∈ 𝐶 ↔ {y ∣ ∃x ∈ A y = B} ⊆ 𝐶))
Theorem	dfpss2 3023	Alternate definition of proper subclass. (Contributed by NM, 7-Feb-1996.)
⊢ (A ⊊ B ↔ (A ⊆ B ∧ ¬ A = B))
Theorem	dfpss3 3024	Alternate definition of proper subclass. (Contributed by NM, 7-Feb-1996.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (A ⊊ B ↔ (A ⊆ B ∧ ¬ B ⊆ A))
Theorem	psseq1 3025	Equality theorem for proper subclass. (Contributed by NM, 7-Feb-1996.)
⊢ (A = B → (A ⊊ 𝐶 ↔ B ⊊ 𝐶))
Theorem	psseq2 3026	Equality theorem for proper subclass. (Contributed by NM, 7-Feb-1996.)
⊢ (A = B → (𝐶 ⊊ A ↔ 𝐶 ⊊ B))
Theorem	psseq1i 3027	An equality inference for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.)
⊢ A = B    ⇒   ⊢ (A ⊊ 𝐶 ↔ B ⊊ 𝐶)
Theorem	psseq2i 3028	An equality inference for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.)
⊢ A = B    ⇒   ⊢ (𝐶 ⊊ A ↔ 𝐶 ⊊ B)
Theorem	psseq12i 3029	An equality inference for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.)
⊢ A = B    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (A ⊊ 𝐶 ↔ B ⊊ 𝐷)
Theorem	psseq1d 3030	An equality deduction for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (A ⊊ 𝐶 ↔ B ⊊ 𝐶))
Theorem	psseq2d 3031	An equality deduction for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (𝐶 ⊊ A ↔ 𝐶 ⊊ B))
Theorem	psseq12d 3032	An equality deduction for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.)
⊢ (φ → A = B)    &   ⊢ (φ → 𝐶 = 𝐷)    ⇒   ⊢ (φ → (A ⊊ 𝐶 ↔ B ⊊ 𝐷))
Theorem	pssss 3033	A proper subclass is a subclass. Theorem 10 of [Suppes] p. 23. (Contributed by NM, 7-Feb-1996.)
⊢ (A ⊊ B → A ⊆ B)
Theorem	pssne 3034	Two classes in a proper subclass relationship are not equal. (Contributed by NM, 16-Feb-2015.)
⊢ (A ⊊ B → A ≠ B)
Theorem	pssssd 3035	Deduce subclass from proper subclass. (Contributed by NM, 29-Feb-1996.)
⊢ (φ → A ⊊ B)    ⇒   ⊢ (φ → A ⊆ B)
Theorem	pssned 3036	Proper subclasses are unequal. Deduction form of pssne 3034. (Contributed by David Moews, 1-May-2017.)
⊢ (φ → A ⊊ B)    ⇒   ⊢ (φ → A ≠ B)
Theorem	sspssr 3037	Subclass in terms of proper subclass. (Contributed by Jim Kingdon, 16-Jul-2018.)
⊢ ((A ⊊ B ∨ A = B) → A ⊆ B)
Theorem	pssirr 3038	Proper subclass is irreflexive. Theorem 7 of [Suppes] p. 23. (Contributed by NM, 7-Feb-1996.)
⊢ ¬ A ⊊ A
Theorem	pssn2lp 3039	Proper subclass has no 2-cycle loops. Compare Theorem 8 of [Suppes] p. 23. (Contributed by NM, 7-Feb-1996.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ¬ (A ⊊ B ∧ B ⊊ A)
Theorem	sspsstrir 3040	Two ways of stating trichotomy with respect to inclusion. (Contributed by Jim Kingdon, 16-Jul-2018.)
⊢ ((A ⊊ B ∨ A = B ∨ B ⊊ A) → (A ⊆ B ∨ B ⊆ A))
Theorem	ssnpss 3041	Partial trichotomy law for subclasses. (Contributed by NM, 16-May-1996.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (A ⊆ B → ¬ B ⊊ A)
Theorem	sspssn 3042	Like pssn2lp 3039 but for subset and proper subset. (Contributed by Jim Kingdon, 17-Jul-2018.)
⊢ ¬ (A ⊆ B ∧ B ⊊ A)
Theorem	psstr 3043	Transitive law for proper subclass. Theorem 9 of [Suppes] p. 23. (Contributed by NM, 7-Feb-1996.)
⊢ ((A ⊊ B ∧ B ⊊ 𝐶) → A ⊊ 𝐶)
Theorem	sspsstr 3044	Transitive law for subclass and proper subclass. (Contributed by NM, 3-Apr-1996.)
⊢ ((A ⊆ B ∧ B ⊊ 𝐶) → A ⊊ 𝐶)
Theorem	psssstr 3045	Transitive law for subclass and proper subclass. (Contributed by NM, 3-Apr-1996.)
⊢ ((A ⊊ B ∧ B ⊆ 𝐶) → A ⊊ 𝐶)
Theorem	psstrd 3046	Proper subclass inclusion is transitive. Deduction form of psstr 3043. (Contributed by David Moews, 1-May-2017.)
⊢ (φ → A ⊊ B)    &   ⊢ (φ → B ⊊ 𝐶)    ⇒   ⊢ (φ → A ⊊ 𝐶)
Theorem	sspsstrd 3047	Transitivity involving subclass and proper subclass inclusion. Deduction form of sspsstr 3044. (Contributed by David Moews, 1-May-2017.)
⊢ (φ → A ⊆ B)    &   ⊢ (φ → B ⊊ 𝐶)    ⇒   ⊢ (φ → A ⊊ 𝐶)
Theorem	psssstrd 3048	Transitivity involving subclass and proper subclass inclusion. Deduction form of psssstr 3045. (Contributed by David Moews, 1-May-2017.)
⊢ (φ → A ⊊ B)    &   ⊢ (φ → B ⊆ 𝐶)    ⇒   ⊢ (φ → A ⊊ 𝐶)
2.1.13  The difference, union, and intersection of two classes
2.1.13.1  The difference of two classes
Theorem	difeq1 3049	Equality theorem for class difference. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (A = B → (A ∖ 𝐶) = (B ∖ 𝐶))
Theorem	difeq2 3050	Equality theorem for class difference. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (A = B → (𝐶 ∖ A) = (𝐶 ∖ B))
Theorem	difeq12 3051	Equality theorem for class difference. (Contributed by FL, 31-Aug-2009.)
⊢ ((A = B ∧ 𝐶 = 𝐷) → (A ∖ 𝐶) = (B ∖ 𝐷))
Theorem	difeq1i 3052	Inference adding difference to the right in a class equality. (Contributed by NM, 15-Nov-2002.)
⊢ A = B    ⇒   ⊢ (A ∖ 𝐶) = (B ∖ 𝐶)
Theorem	difeq2i 3053	Inference adding difference to the left in a class equality. (Contributed by NM, 15-Nov-2002.)
⊢ A = B    ⇒   ⊢ (𝐶 ∖ A) = (𝐶 ∖ B)
Theorem	difeq12i 3054	Equality inference for class difference. (Contributed by NM, 29-Aug-2004.)
⊢ A = B    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (A ∖ 𝐶) = (B ∖ 𝐷)
Theorem	difeq1d 3055	Deduction adding difference to the right in a class equality. (Contributed by NM, 15-Nov-2002.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (A ∖ 𝐶) = (B ∖ 𝐶))
Theorem	difeq2d 3056	Deduction adding difference to the left in a class equality. (Contributed by NM, 15-Nov-2002.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (𝐶 ∖ A) = (𝐶 ∖ B))
Theorem	difeq12d 3057	Equality deduction for class difference. (Contributed by FL, 29-May-2014.)
⊢ (φ → A = B)    &   ⊢ (φ → 𝐶 = 𝐷)    ⇒   ⊢ (φ → (A ∖ 𝐶) = (B ∖ 𝐷))
Theorem	difeqri 3058*	Inference from membership to difference. (Contributed by NM, 17-May-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ((x ∈ A ∧ ¬ x ∈ B) ↔ x ∈ 𝐶)    ⇒   ⊢ (A ∖ B) = 𝐶
Theorem	nfdif 3059	Bound-variable hypothesis builder for class difference. (Contributed by NM, 3-Dec-2003.) (Revised by Mario Carneiro, 13-Oct-2016.)
⊢ ℲxA    &   ⊢ ℲxB    ⇒   ⊢ Ⅎx(A ∖ B)
Theorem	eldifi 3060	Implication of membership in a class difference. (Contributed by NM, 29-Apr-1994.)
⊢ (A ∈ (B ∖ 𝐶) → A ∈ B)
Theorem	eldifn 3061	Implication of membership in a class difference. (Contributed by NM, 3-May-1994.)
⊢ (A ∈ (B ∖ 𝐶) → ¬ A ∈ 𝐶)
Theorem	elndif 3062	A set does not belong to a class excluding it. (Contributed by NM, 27-Jun-1994.)
⊢ (A ∈ B → ¬ A ∈ (𝐶 ∖ B))
Theorem	difdif 3063	Double class difference. Exercise 11 of [TakeutiZaring] p. 22. (Contributed by NM, 17-May-1998.)
⊢ (A ∖ (B ∖ A)) = A
Theorem	difss 3064	Subclass relationship for class difference. Exercise 14 of [TakeutiZaring] p. 22. (Contributed by NM, 29-Apr-1994.)
⊢ (A ∖ B) ⊆ A
Theorem	difssd 3065	A difference of two classes is contained in the minuend. Deduction form of difss 3064. (Contributed by David Moews, 1-May-2017.)
⊢ (φ → (A ∖ B) ⊆ A)
Theorem	difss2 3066	If a class is contained in a difference, it is contained in the minuend. (Contributed by David Moews, 1-May-2017.)
⊢ (A ⊆ (B ∖ 𝐶) → A ⊆ B)
Theorem	difss2d 3067	If a class is contained in a difference, it is contained in the minuend. Deduction form of difss2 3066. (Contributed by David Moews, 1-May-2017.)
⊢ (φ → A ⊆ (B ∖ 𝐶))    ⇒   ⊢ (φ → A ⊆ B)
Theorem	ssdifss 3068	Preservation of a subclass relationship by class difference. (Contributed by NM, 15-Feb-2007.)
⊢ (A ⊆ B → (A ∖ 𝐶) ⊆ B)
Theorem	ddifnel 3069*	Double complement under universal class. The hypothesis is one way of expressing the idea that membership in A is decidable. Exercise 4.10(s) of [Mendelson] p. 231, but with an additional hypothesis. For a version without a hypothesis, but which only states that A is a subset of V ∖ (V ∖ A), see ddifss 3169. (Contributed by Jim Kingdon, 21-Jul-2018.)
⊢ (¬ x ∈ (V ∖ A) → x ∈ A)    ⇒   ⊢ (V ∖ (V ∖ A)) = A
Theorem	ssconb 3070	Contraposition law for subsets. (Contributed by NM, 22-Mar-1998.)
⊢ ((A ⊆ 𝐶 ∧ B ⊆ 𝐶) → (A ⊆ (𝐶 ∖ B) ↔ B ⊆ (𝐶 ∖ A)))
Theorem	sscon 3071	Contraposition law for subsets. Exercise 15 of [TakeutiZaring] p. 22. (Contributed by NM, 22-Mar-1998.)
⊢ (A ⊆ B → (𝐶 ∖ B) ⊆ (𝐶 ∖ A))
Theorem	ssdif 3072	Difference law for subsets. (Contributed by NM, 28-May-1998.)
⊢ (A ⊆ B → (A ∖ 𝐶) ⊆ (B ∖ 𝐶))
Theorem	ssdifd 3073	If A is contained in B, then (A ∖ 𝐶) is contained in (B ∖ 𝐶). Deduction form of ssdif 3072. (Contributed by David Moews, 1-May-2017.)
⊢ (φ → A ⊆ B)    ⇒   ⊢ (φ → (A ∖ 𝐶) ⊆ (B ∖ 𝐶))
Theorem	sscond 3074	If A is contained in B, then (𝐶 ∖ B) is contained in (𝐶 ∖ A). Deduction form of sscon 3071. (Contributed by David Moews, 1-May-2017.)
⊢ (φ → A ⊆ B)    ⇒   ⊢ (φ → (𝐶 ∖ B) ⊆ (𝐶 ∖ A))
Theorem	ssdifssd 3075	If A is contained in B, then (A ∖ 𝐶) is also contained in B. Deduction form of ssdifss 3068. (Contributed by David Moews, 1-May-2017.)
⊢ (φ → A ⊆ B)    ⇒   ⊢ (φ → (A ∖ 𝐶) ⊆ B)
Theorem	ssdif2d 3076	If A is contained in B and 𝐶 is contained in 𝐷, then (A ∖ 𝐷) is contained in (B ∖ 𝐶). Deduction form. (Contributed by David Moews, 1-May-2017.)
⊢ (φ → A ⊆ B)    &   ⊢ (φ → 𝐶 ⊆ 𝐷)    ⇒   ⊢ (φ → (A ∖ 𝐷) ⊆ (B ∖ 𝐶))
Theorem	raldifb 3077	Restricted universal quantification on a class difference in terms of an implication. (Contributed by Alexander van der Vekens, 3-Jan-2018.)
⊢ (∀x ∈ A (x ∉ B → φ) ↔ ∀x ∈ (A ∖ B)φ)
2.1.13.2  The union of two classes
Theorem	elun 3078	Expansion of membership in class union. Theorem 12 of [Suppes] p. 25. (Contributed by NM, 7-Aug-1994.)
⊢ (A ∈ (B ∪ 𝐶) ↔ (A ∈ B ∨ A ∈ 𝐶))
Theorem	uneqri 3079*	Inference from membership to union. (Contributed by NM, 5-Aug-1993.)
⊢ ((x ∈ A ∨ x ∈ B) ↔ x ∈ 𝐶)    ⇒   ⊢ (A ∪ B) = 𝐶
Theorem	unidm 3080	Idempotent law for union of classes. Theorem 23 of [Suppes] p. 27. (Contributed by NM, 5-Aug-1993.)
⊢ (A ∪ A) = A
Theorem	uncom 3081	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.)
⊢ (A ∪ B) = (B ∪ A)
Theorem	equncom 3082	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.)
⊢ (A = (B ∪ 𝐶) ↔ A = (𝐶 ∪ B))
Theorem	equncomi 3083	Inference form of equncom 3082. (Contributed by Alan Sare, 18-Feb-2012.)
⊢ A = (B ∪ 𝐶)    ⇒   ⊢ A = (𝐶 ∪ B)
Theorem	uneq1 3084	Equality theorem for union of two classes. (Contributed by NM, 5-Aug-1993.)
⊢ (A = B → (A ∪ 𝐶) = (B ∪ 𝐶))
Theorem	uneq2 3085	Equality theorem for the union of two classes. (Contributed by NM, 5-Aug-1993.)
⊢ (A = B → (𝐶 ∪ A) = (𝐶 ∪ B))
Theorem	uneq12 3086	Equality theorem for union of two classes. (Contributed by NM, 29-Mar-1998.)
⊢ ((A = B ∧ 𝐶 = 𝐷) → (A ∪ 𝐶) = (B ∪ 𝐷))
Theorem	uneq1i 3087	Inference adding union to the right in a class equality. (Contributed by NM, 30-Aug-1993.)
⊢ A = B    ⇒   ⊢ (A ∪ 𝐶) = (B ∪ 𝐶)
Theorem	uneq2i 3088	Inference adding union to the left in a class equality. (Contributed by NM, 30-Aug-1993.)
⊢ A = B    ⇒   ⊢ (𝐶 ∪ A) = (𝐶 ∪ B)
Theorem	uneq12i 3089	Equality inference for union of two classes. (Contributed by NM, 12-Aug-2004.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)
⊢ A = B    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (A ∪ 𝐶) = (B ∪ 𝐷)
Theorem	uneq1d 3090	Deduction adding union to the right in a class equality. (Contributed by NM, 29-Mar-1998.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (A ∪ 𝐶) = (B ∪ 𝐶))
Theorem	uneq2d 3091	Deduction adding union to the left in a class equality. (Contributed by NM, 29-Mar-1998.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (𝐶 ∪ A) = (𝐶 ∪ B))
Theorem	uneq12d 3092	Equality deduction for union of two classes. (Contributed by NM, 29-Sep-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (φ → A = B)    &   ⊢ (φ → 𝐶 = 𝐷)    ⇒   ⊢ (φ → (A ∪ 𝐶) = (B ∪ 𝐷))
Theorem	nfun 3093	Bound-variable hypothesis builder for the union of classes. (Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro, 14-Oct-2016.)
⊢ ℲxA    &   ⊢ ℲxB    ⇒   ⊢ Ⅎx(A ∪ B)
Theorem	unass 3094	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.)
⊢ ((A ∪ B) ∪ 𝐶) = (A ∪ (B ∪ 𝐶))
Theorem	un12 3095	A rearrangement of union. (Contributed by NM, 12-Aug-2004.)
⊢ (A ∪ (B ∪ 𝐶)) = (B ∪ (A ∪ 𝐶))
Theorem	un23 3096	A rearrangement of union. (Contributed by NM, 12-Aug-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ((A ∪ B) ∪ 𝐶) = ((A ∪ 𝐶) ∪ B)
Theorem	un4 3097	A rearrangement of the union of 4 classes. (Contributed by NM, 12-Aug-2004.)
⊢ ((A ∪ B) ∪ (𝐶 ∪ 𝐷)) = ((A ∪ 𝐶) ∪ (B ∪ 𝐷))
Theorem	unundi 3098	Union distributes over itself. (Contributed by NM, 17-Aug-2004.)
⊢ (A ∪ (B ∪ 𝐶)) = ((A ∪ B) ∪ (A ∪ 𝐶))
Theorem	unundir 3099	Union distributes over itself. (Contributed by NM, 17-Aug-2004.)
⊢ ((A ∪ B) ∪ 𝐶) = ((A ∪ 𝐶) ∪ (B ∪ 𝐶))
Theorem	ssun1 3100	Subclass relationship for union of classes. Theorem 25 of [Suppes] p. 27. (Contributed by NM, 5-Aug-1993.)
⊢ A ⊆ (A ∪ B)