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	ssab2 3001*	Subclass relation for the restriction of a class abstraction. (Contributed by NM, 31-Mar-1995.)
⊢ {x ∣ (x ∈ A ∧ φ)} ⊆ A
Theorem	ssrab2 3002*	Subclass relation for a restricted class. (Contributed by NM, 19-Mar-1997.)
⊢ {x ∈ A ∣ φ} ⊆ A
Theorem	ssrabeq 3003*	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 3004	A restricted class is a subclass of the corresponding unrestricted class. (Contributed by Mario Carneiro, 23-Dec-2016.)
⊢ {x ∈ A ∣ φ} ⊆ {x ∣ φ}
Theorem	uniiunlem 3005*	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 3006	Alternate definition of proper subclass. (Contributed by NM, 7-Feb-1996.)
⊢ (A ⊊ B ↔ (A ⊆ B ∧ ¬ A = B))
Theorem	dfpss3 3007	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 3008	Equality theorem for proper subclass. (Contributed by NM, 7-Feb-1996.)
⊢ (A = B → (A ⊊ 𝐶 ↔ B ⊊ 𝐶))
Theorem	psseq2 3009	Equality theorem for proper subclass. (Contributed by NM, 7-Feb-1996.)
⊢ (A = B → (𝐶 ⊊ A ↔ 𝐶 ⊊ B))
Theorem	psseq1i 3010	An equality inference for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.)
⊢ A = B    ⇒   ⊢ (A ⊊ 𝐶 ↔ B ⊊ 𝐶)
Theorem	psseq2i 3011	An equality inference for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.)
⊢ A = B    ⇒   ⊢ (𝐶 ⊊ A ↔ 𝐶 ⊊ B)
Theorem	psseq12i 3012	An equality inference for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.)
⊢ A = B    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (A ⊊ 𝐶 ↔ B ⊊ 𝐷)
Theorem	psseq1d 3013	An equality deduction for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (A ⊊ 𝐶 ↔ B ⊊ 𝐶))
Theorem	psseq2d 3014	An equality deduction for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (𝐶 ⊊ A ↔ 𝐶 ⊊ B))
Theorem	psseq12d 3015	An equality deduction for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.)
⊢ (φ → A = B)    &   ⊢ (φ → 𝐶 = 𝐷)    ⇒   ⊢ (φ → (A ⊊ 𝐶 ↔ B ⊊ 𝐷))
Theorem	pssss 3016	A proper subclass is a subclass. Theorem 10 of [Suppes] p. 23. (Contributed by NM, 7-Feb-1996.)
⊢ (A ⊊ B → A ⊆ B)
Theorem	pssne 3017	Two classes in a proper subclass relationship are not equal. (Contributed by NM, 16-Feb-2015.)
⊢ (A ⊊ B → A ≠ B)
Theorem	pssssd 3018	Deduce subclass from proper subclass. (Contributed by NM, 29-Feb-1996.)
⊢ (φ → A ⊊ B)    ⇒   ⊢ (φ → A ⊆ B)
Theorem	pssned 3019	Proper subclasses are unequal. Deduction form of pssne 3017. (Contributed by David Moews, 1-May-2017.)
⊢ (φ → A ⊊ B)    ⇒   ⊢ (φ → A ≠ B)
Theorem	sspssr 3020	Subclass in terms of proper subclass. (Contributed by Jim Kingdon, 16-Jul-2018.)
⊢ ((A ⊊ B ∨ A = B) → A ⊆ B)
Theorem	pssirr 3021	Proper subclass is irreflexive. Theorem 7 of [Suppes] p. 23. (Contributed by NM, 7-Feb-1996.)
⊢ ¬ A ⊊ A
Theorem	pssn2lp 3022	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 3023	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 3024	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 3025	Like pssn2lp 3022 but for subset and proper subset. (Contributed by Jim Kingdon, 17-Jul-2018.)
⊢ ¬ (A ⊆ B ∧ B ⊊ A)
Theorem	psstr 3026	Transitive law for proper subclass. Theorem 9 of [Suppes] p. 23. (Contributed by NM, 7-Feb-1996.)
⊢ ((A ⊊ B ∧ B ⊊ 𝐶) → A ⊊ 𝐶)
Theorem	sspsstr 3027	Transitive law for subclass and proper subclass. (Contributed by NM, 3-Apr-1996.)
⊢ ((A ⊆ B ∧ B ⊊ 𝐶) → A ⊊ 𝐶)
Theorem	psssstr 3028	Transitive law for subclass and proper subclass. (Contributed by NM, 3-Apr-1996.)
⊢ ((A ⊊ B ∧ B ⊆ 𝐶) → A ⊊ 𝐶)
Theorem	psstrd 3029	Proper subclass inclusion is transitive. Deduction form of psstr 3026. (Contributed by David Moews, 1-May-2017.)
⊢ (φ → A ⊊ B)    &   ⊢ (φ → B ⊊ 𝐶)    ⇒   ⊢ (φ → A ⊊ 𝐶)
Theorem	sspsstrd 3030	Transitivity involving subclass and proper subclass inclusion. Deduction form of sspsstr 3027. (Contributed by David Moews, 1-May-2017.)
⊢ (φ → A ⊆ B)    &   ⊢ (φ → B ⊊ 𝐶)    ⇒   ⊢ (φ → A ⊊ 𝐶)
Theorem	psssstrd 3031	Transitivity involving subclass and proper subclass inclusion. Deduction form of psssstr 3028. (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 3032	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 3033	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 3034	Equality theorem for class difference. (Contributed by FL, 31-Aug-2009.)
⊢ ((A = B ∧ 𝐶 = 𝐷) → (A ∖ 𝐶) = (B ∖ 𝐷))
Theorem	difeq1i 3035	Inference adding difference to the right in a class equality. (Contributed by NM, 15-Nov-2002.)
⊢ A = B    ⇒   ⊢ (A ∖ 𝐶) = (B ∖ 𝐶)
Theorem	difeq2i 3036	Inference adding difference to the left in a class equality. (Contributed by NM, 15-Nov-2002.)
⊢ A = B    ⇒   ⊢ (𝐶 ∖ A) = (𝐶 ∖ B)
Theorem	difeq12i 3037	Equality inference for class difference. (Contributed by NM, 29-Aug-2004.)
⊢ A = B    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (A ∖ 𝐶) = (B ∖ 𝐷)
Theorem	difeq1d 3038	Deduction adding difference to the right in a class equality. (Contributed by NM, 15-Nov-2002.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (A ∖ 𝐶) = (B ∖ 𝐶))
Theorem	difeq2d 3039	Deduction adding difference to the left in a class equality. (Contributed by NM, 15-Nov-2002.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (𝐶 ∖ A) = (𝐶 ∖ B))
Theorem	difeq12d 3040	Equality deduction for class difference. (Contributed by FL, 29-May-2014.)
⊢ (φ → A = B)    &   ⊢ (φ → 𝐶 = 𝐷)    ⇒   ⊢ (φ → (A ∖ 𝐶) = (B ∖ 𝐷))
Theorem	difeqri 3041*	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 3042	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 3043	Implication of membership in a class difference. (Contributed by NM, 29-Apr-1994.)
⊢ (A ∈ (B ∖ 𝐶) → A ∈ B)
Theorem	eldifn 3044	Implication of membership in a class difference. (Contributed by NM, 3-May-1994.)
⊢ (A ∈ (B ∖ 𝐶) → ¬ A ∈ 𝐶)
Theorem	elndif 3045	A set does not belong to a class excluding it. (Contributed by NM, 27-Jun-1994.)
⊢ (A ∈ B → ¬ A ∈ (𝐶 ∖ B))
Theorem	difdif 3046	Double class difference. Exercise 11 of [TakeutiZaring] p. 22. (Contributed by NM, 17-May-1998.)
⊢ (A ∖ (B ∖ A)) = A
Theorem	difss 3047	Subclass relationship for class difference. Exercise 14 of [TakeutiZaring] p. 22. (Contributed by NM, 29-Apr-1994.)
⊢ (A ∖ B) ⊆ A
Theorem	difssd 3048	A difference of two classes is contained in the minuend. Deduction form of difss 3047. (Contributed by David Moews, 1-May-2017.)
⊢ (φ → (A ∖ B) ⊆ A)
Theorem	difss2 3049	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 3050	If a class is contained in a difference, it is contained in the minuend. Deduction form of difss2 3049. (Contributed by David Moews, 1-May-2017.)
⊢ (φ → A ⊆ (B ∖ 𝐶))    ⇒   ⊢ (φ → A ⊆ B)
Theorem	ssdifss 3051	Preservation of a subclass relationship by class difference. (Contributed by NM, 15-Feb-2007.)
⊢ (A ⊆ B → (A ∖ 𝐶) ⊆ B)
Theorem	ddifnel 3052*	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 3152. (Contributed by Jim Kingdon, 21-Jul-2018.)
⊢ (¬ x ∈ (V ∖ A) → x ∈ A)    ⇒   ⊢ (V ∖ (V ∖ A)) = A
Theorem	ssconb 3053	Contraposition law for subsets. (Contributed by NM, 22-Mar-1998.)
⊢ ((A ⊆ 𝐶 ∧ B ⊆ 𝐶) → (A ⊆ (𝐶 ∖ B) ↔ B ⊆ (𝐶 ∖ A)))
Theorem	sscon 3054	Contraposition law for subsets. Exercise 15 of [TakeutiZaring] p. 22. (Contributed by NM, 22-Mar-1998.)
⊢ (A ⊆ B → (𝐶 ∖ B) ⊆ (𝐶 ∖ A))
Theorem	ssdif 3055	Difference law for subsets. (Contributed by NM, 28-May-1998.)
⊢ (A ⊆ B → (A ∖ 𝐶) ⊆ (B ∖ 𝐶))
Theorem	ssdifd 3056	If A is contained in B, then (A ∖ 𝐶) is contained in (B ∖ 𝐶). Deduction form of ssdif 3055. (Contributed by David Moews, 1-May-2017.)
⊢ (φ → A ⊆ B)    ⇒   ⊢ (φ → (A ∖ 𝐶) ⊆ (B ∖ 𝐶))
Theorem	sscond 3057	If A is contained in B, then (𝐶 ∖ B) is contained in (𝐶 ∖ A). Deduction form of sscon 3054. (Contributed by David Moews, 1-May-2017.)
⊢ (φ → A ⊆ B)    ⇒   ⊢ (φ → (𝐶 ∖ B) ⊆ (𝐶 ∖ A))
Theorem	ssdifssd 3058	If A is contained in B, then (A ∖ 𝐶) is also contained in B. Deduction form of ssdifss 3051. (Contributed by David Moews, 1-May-2017.)
⊢ (φ → A ⊆ B)    ⇒   ⊢ (φ → (A ∖ 𝐶) ⊆ B)
Theorem	ssdif2d 3059	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 3060	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 3061	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 3062*	Inference from membership to union. (Contributed by NM, 5-Aug-1993.)
⊢ ((x ∈ A ∨ x ∈ B) ↔ x ∈ 𝐶)    ⇒   ⊢ (A ∪ B) = 𝐶
Theorem	unidm 3063	Idempotent law for union of classes. Theorem 23 of [Suppes] p. 27. (Contributed by NM, 5-Aug-1993.)
⊢ (A ∪ A) = A
Theorem	uncom 3064	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 3065	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 3066	Inference form of equncom 3065. (Contributed by Alan Sare, 18-Feb-2012.)
⊢ A = (B ∪ 𝐶)    ⇒   ⊢ A = (𝐶 ∪ B)
Theorem	uneq1 3067	Equality theorem for union of two classes. (Contributed by NM, 5-Aug-1993.)
⊢ (A = B → (A ∪ 𝐶) = (B ∪ 𝐶))
Theorem	uneq2 3068	Equality theorem for the union of two classes. (Contributed by NM, 5-Aug-1993.)
⊢ (A = B → (𝐶 ∪ A) = (𝐶 ∪ B))
Theorem	uneq12 3069	Equality theorem for union of two classes. (Contributed by NM, 29-Mar-1998.)
⊢ ((A = B ∧ 𝐶 = 𝐷) → (A ∪ 𝐶) = (B ∪ 𝐷))
Theorem	uneq1i 3070	Inference adding union to the right in a class equality. (Contributed by NM, 30-Aug-1993.)
⊢ A = B    ⇒   ⊢ (A ∪ 𝐶) = (B ∪ 𝐶)
Theorem	uneq2i 3071	Inference adding union to the left in a class equality. (Contributed by NM, 30-Aug-1993.)
⊢ A = B    ⇒   ⊢ (𝐶 ∪ A) = (𝐶 ∪ B)
Theorem	uneq12i 3072	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 3073	Deduction adding union to the right in a class equality. (Contributed by NM, 29-Mar-1998.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (A ∪ 𝐶) = (B ∪ 𝐶))
Theorem	uneq2d 3074	Deduction adding union to the left in a class equality. (Contributed by NM, 29-Mar-1998.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (𝐶 ∪ A) = (𝐶 ∪ B))
Theorem	uneq12d 3075	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 3076	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 3077	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 3078	A rearrangement of union. (Contributed by NM, 12-Aug-2004.)
⊢ (A ∪ (B ∪ 𝐶)) = (B ∪ (A ∪ 𝐶))
Theorem	un23 3079	A rearrangement of union. (Contributed by NM, 12-Aug-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ((A ∪ B) ∪ 𝐶) = ((A ∪ 𝐶) ∪ B)
Theorem	un4 3080	A rearrangement of the union of 4 classes. (Contributed by NM, 12-Aug-2004.)
⊢ ((A ∪ B) ∪ (𝐶 ∪ 𝐷)) = ((A ∪ 𝐶) ∪ (B ∪ 𝐷))
Theorem	unundi 3081	Union distributes over itself. (Contributed by NM, 17-Aug-2004.)
⊢ (A ∪ (B ∪ 𝐶)) = ((A ∪ B) ∪ (A ∪ 𝐶))
Theorem	unundir 3082	Union distributes over itself. (Contributed by NM, 17-Aug-2004.)
⊢ ((A ∪ B) ∪ 𝐶) = ((A ∪ 𝐶) ∪ (B ∪ 𝐶))
Theorem	ssun1 3083	Subclass relationship for union of classes. Theorem 25 of [Suppes] p. 27. (Contributed by NM, 5-Aug-1993.)
⊢ A ⊆ (A ∪ B)
Theorem	ssun2 3084	Subclass relationship for union of classes. (Contributed by NM, 30-Aug-1993.)
⊢ A ⊆ (B ∪ A)
Theorem	ssun3 3085	Subclass law for union of classes. (Contributed by NM, 5-Aug-1993.)
⊢ (A ⊆ B → A ⊆ (B ∪ 𝐶))
Theorem	ssun4 3086	Subclass law for union of classes. (Contributed by NM, 14-Aug-1994.)
⊢ (A ⊆ B → A ⊆ (𝐶 ∪ B))
Theorem	elun1 3087	Membership law for union of classes. (Contributed by NM, 5-Aug-1993.)
⊢ (A ∈ B → A ∈ (B ∪ 𝐶))
Theorem	elun2 3088	Membership law for union of classes. (Contributed by NM, 30-Aug-1993.)
⊢ (A ∈ B → A ∈ (𝐶 ∪ B))
Theorem	unss1 3089	Subclass law for union of classes. (Contributed by NM, 14-Oct-1999.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (A ⊆ B → (A ∪ 𝐶) ⊆ (B ∪ 𝐶))
Theorem	ssequn1 3090	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.)
⊢ (A ⊆ B ↔ (A ∪ B) = B)
Theorem	unss2 3091	Subclass law for union of classes. Exercise 7 of [TakeutiZaring] p. 18. (Contributed by NM, 14-Oct-1999.)
⊢ (A ⊆ B → (𝐶 ∪ A) ⊆ (𝐶 ∪ B))
Theorem	unss12 3092	Subclass law for union of classes. (Contributed by NM, 2-Jun-2004.)
⊢ ((A ⊆ B ∧ 𝐶 ⊆ 𝐷) → (A ∪ 𝐶) ⊆ (B ∪ 𝐷))
Theorem	ssequn2 3093	A relationship between subclass and union. (Contributed by NM, 13-Jun-1994.)
⊢ (A ⊆ B ↔ (B ∪ A) = B)
Theorem	unss 3094	The union of two subclasses is a subclass. Theorem 27 of [Suppes] p. 27 and its converse. (Contributed by NM, 11-Jun-2004.)
⊢ ((A ⊆ 𝐶 ∧ B ⊆ 𝐶) ↔ (A ∪ B) ⊆ 𝐶)
Theorem	unssi 3095	An inference showing the union of two subclasses is a subclass. (Contributed by Raph Levien, 10-Dec-2002.)
⊢ A ⊆ 𝐶    &   ⊢ B ⊆ 𝐶    ⇒   ⊢ (A ∪ B) ⊆ 𝐶
Theorem	unssd 3096	A deduction showing the union of two subclasses is a subclass. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (φ → A ⊆ 𝐶)    &   ⊢ (φ → B ⊆ 𝐶)    ⇒   ⊢ (φ → (A ∪ B) ⊆ 𝐶)
Theorem	unssad 3097	If (A ∪ B) is contained in 𝐶, so is A. One-way deduction form of unss 3094. Partial converse of unssd 3096. (Contributed by David Moews, 1-May-2017.)
⊢ (φ → (A ∪ B) ⊆ 𝐶)    ⇒   ⊢ (φ → A ⊆ 𝐶)
Theorem	unssbd 3098	If (A ∪ B) is contained in 𝐶, so is B. One-way deduction form of unss 3094. Partial converse of unssd 3096. (Contributed by David Moews, 1-May-2017.)
⊢ (φ → (A ∪ B) ⊆ 𝐶)    ⇒   ⊢ (φ → B ⊆ 𝐶)
Theorem	ssun 3099	A condition that implies inclusion in the union of two classes. (Contributed by NM, 23-Nov-2003.)
⊢ ((A ⊆ B ∨ A ⊆ 𝐶) → A ⊆ (B ∪ 𝐶))
Theorem	rexun 3100	Restricted existential quantification over union. (Contributed by Jeff Madsen, 5-Jan-2011.)
⊢ (∃x ∈ (A ∪ B)φ ↔ (∃x ∈ A φ ∨ ∃x ∈ B φ))