P. 43 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 4201-4300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sseq0 4201	A subclass of an empty class is empty. (Contributed by NM, 7-Mar-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅)
Theorem	ssn0 4202	A class with a nonempty subclass is nonempty. (Contributed by NM, 17-Feb-2007.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → 𝐵 ≠ ∅)
Theorem	0dif 4203	The difference between the empty set and a class. Part of Exercise 4.4 of [Stoll] p. 16. (Contributed by NM, 17-Aug-2004.)
⊢ (∅ ∖ 𝐴) = ∅
Theorem	abf 4204	A class builder with a false argument is empty. (Contributed by NM, 20-Jan-2012.)
⊢ ¬ 𝜑    ⇒   ⊢ {𝑥 ∣ 𝜑} = ∅
Theorem	eq0rdv 4205*	Deduction for equality to the empty set. (Contributed by NM, 11-Jul-2014.)
⊢ (𝜑 → ¬ 𝑥 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 = ∅)
Theorem	csbprc 4206	The proper substitution of a proper class for a set into a class results in the empty set. (Contributed by NM, 17-Aug-2018.) (Proof shortened by JJ, 27-Aug-2021.)
⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 = ∅)
Theorem	csb0 4207	The proper substitution of a class into the empty set is the empty set. (Contributed by NM, 18-Aug-2018.)
⊢ ⦋𝐴 / 𝑥⦌∅ = ∅
Theorem	sbcel12 4208	Distribute proper substitution through a membership relation. (Contributed by NM, 10-Nov-2005.) (Revised by NM, 18-Aug-2018.)
⊢ ([𝐴 / 𝑥]𝐵 ∈ 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 ∈ ⦋𝐴 / 𝑥⦌𝐶)
Theorem	sbceqg 4209	Distribute proper substitution through an equality relation. (Contributed by NM, 10-Nov-2005.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶))
Theorem	sbcnel12g 4210	Distribute proper substitution through negated membership. (Contributed by Andrew Salmon, 18-Jun-2011.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 ∉ 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 ∉ ⦋𝐴 / 𝑥⦌𝐶))
Theorem	sbcne12 4211	Distribute proper substitution through an inequality. (Contributed by Andrew Salmon, 18-Jun-2011.) (Revised by NM, 18-Aug-2018.)
⊢ ([𝐴 / 𝑥]𝐵 ≠ 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 ≠ ⦋𝐴 / 𝑥⦌𝐶)
Theorem	sbcel1g 4212*	Move proper substitution in and out of a membership relation. Note that the scope of [𝐴 / 𝑥] is the wff 𝐵 ∈ 𝐶, whereas the scope of ⦋𝐴 / 𝑥⦌ is the class 𝐵. (Contributed by NM, 10-Nov-2005.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 ∈ 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 ∈ 𝐶))
Theorem	sbceq1g 4213*	Move proper substitution to first argument of an equality. (Contributed by NM, 30-Nov-2005.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶))
Theorem	sbcel2 4214*	Move proper substitution in and out of a membership relation. (Contributed by NM, 14-Nov-2005.) (Revised by NM, 18-Aug-2018.)
⊢ ([𝐴 / 𝑥]𝐵 ∈ 𝐶 ↔ 𝐵 ∈ ⦋𝐴 / 𝑥⦌𝐶)
Theorem	sbceq2g 4215*	Move proper substitution to second argument of an equality. (Contributed by NM, 30-Nov-2005.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ 𝐵 = ⦋𝐴 / 𝑥⦌𝐶))
Theorem	csbeq2d 4216	Formula-building deduction for class substitution. (Contributed by NM, 22-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)
Theorem	csbeq2dv 4217*	Formula-building deduction for class substitution. (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)
Theorem	csbeq2i 4218	Formula-building inference for class substitution. (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
⊢ 𝐵 = 𝐶    ⇒   ⊢ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶
Theorem	csbcom 4219*	Commutative law for double substitution into a class. (Contributed by NM, 14-Nov-2005.) (Revised by NM, 18-Aug-2018.)
⊢ ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = ⦋𝐵 / 𝑦⦌⦋𝐴 / 𝑥⦌𝐶
Theorem	sbcnestgf 4220	Nest the composition of two substitutions. (Contributed by Mario Carneiro, 11-Nov-2016.)
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑦Ⅎ𝑥𝜑) → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦]𝜑))
Theorem	csbnestgf 4221	Nest the composition of two substitutions. (Contributed by NM, 23-Nov-2005.) (Proof shortened by Mario Carneiro, 10-Nov-2016.)
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑦Ⅎ𝑥𝐶) → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = ⦋⦋𝐴 / 𝑥⦌𝐵 / 𝑦⦌𝐶)
Theorem	sbcnestg 4222*	Nest the composition of two substitutions. (Contributed by NM, 27-Nov-2005.) (Proof shortened by Mario Carneiro, 11-Nov-2016.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦]𝜑))
Theorem	csbnestg 4223*	Nest the composition of two substitutions. (Contributed by NM, 23-Nov-2005.) (Proof shortened by Mario Carneiro, 10-Nov-2016.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = ⦋⦋𝐴 / 𝑥⦌𝐵 / 𝑦⦌𝐶)
Theorem	sbcco3g 4224*	Composition of two substitutions. (Contributed by NM, 27-Nov-2005.) (Revised by Mario Carneiro, 11-Nov-2016.)
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [𝐶 / 𝑦]𝜑))
Theorem	csbco3g 4225*	Composition of two class substitutions. (Contributed by NM, 27-Nov-2005.) (Revised by Mario Carneiro, 11-Nov-2016.)
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐷 = ⦋𝐶 / 𝑦⦌𝐷)
Theorem	csbnest1g 4226	Nest the composition of two substitutions. (Contributed by NM, 23-May-2006.) (Proof shortened by Mario Carneiro, 11-Nov-2016.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑥⦌𝐶 = ⦋⦋𝐴 / 𝑥⦌𝐵 / 𝑥⦌𝐶)
Theorem	csbidm 4227*	Idempotent law for class substitutions. (Contributed by NM, 1-Mar-2008.) (Revised by NM, 18-Aug-2018.)
⊢ ⦋𝐴 / 𝑥⦌⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵
Theorem	csbvarg 4228	The proper substitution of a class for setvar variable results in the class (if the class exists). (Contributed by NM, 10-Nov-2005.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝑥 = 𝐴)
Theorem	csbvargi 4229	The proper substitution of a class for a setvar variable results in the class (if the class exists), in inference form of csbvarg 4228. (Contributed by Giovanni Mascellani, 30-May-2019.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ⦋𝐴 / 𝑥⦌𝑥 = 𝐴
Theorem	sbccsb 4230*	Substitution into a wff expressed in terms of substitution into a class. (Contributed by NM, 15-Aug-2007.) (Revised by NM, 18-Aug-2018.)
⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝜑})
Theorem	sbccsb2 4231	Substitution into a wff expressed in using substitution into a class. (Contributed by NM, 27-Nov-2005.) (Revised by NM, 18-Aug-2018.)
⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ ⦋𝐴 / 𝑥⦌{𝑥 ∣ 𝜑})
Theorem	rspcsbela 4232*	Special case related to rspsbc 3735. (Contributed by NM, 10-Dec-2005.) (Proof shortened by Eric Schmidt, 17-Jan-2007.)
⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝐶 ∈ 𝐷) → ⦋𝐴 / 𝑥⦌𝐶 ∈ 𝐷)
Theorem	sbnfc2 4233*	Two ways of expressing "𝑥 is (effectively) not free in 𝐴". (Contributed by Mario Carneiro, 14-Oct-2016.)
⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦∀𝑧⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑧 / 𝑥⦌𝐴)
Theorem	csbab 4234*	Move substitution into a class abstraction. (Contributed by NM, 13-Dec-2005.) (Revised by NM, 19-Aug-2018.)
⊢ ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝜑} = {𝑦 ∣ [𝐴 / 𝑥]𝜑}
Theorem	csbun 4235	Distribution of class substitution over union of two classes. (Contributed by Drahflow, 23-Sep-2015.) (Revised by Mario Carneiro, 11-Dec-2016.) (Revised by NM, 13-Sep-2018.)
⊢ ⦋𝐴 / 𝑥⦌(𝐵 ∪ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∪ ⦋𝐴 / 𝑥⦌𝐶)
Theorem	csbin 4236	Distribute proper substitution into a class through an intersection relation. (Contributed by Alan Sare, 22-Jul-2012.) (Revised by NM, 18-Aug-2018.)
⊢ ⦋𝐴 / 𝑥⦌(𝐵 ∩ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∩ ⦋𝐴 / 𝑥⦌𝐶)
Theorem	un00 4237	Two classes are empty iff their union is empty. (Contributed by NM, 11-Aug-2004.)
⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) ↔ (𝐴 ∪ 𝐵) = ∅)
Theorem	vss 4238	Only the universal class has the universal class as a subclass. (Contributed by NM, 17-Sep-2003.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (V ⊆ 𝐴 ↔ 𝐴 = V)
Theorem	0pss 4239	The null set is a proper subset of any nonempty set. (Contributed by NM, 27-Feb-1996.)
⊢ (∅ ⊊ 𝐴 ↔ 𝐴 ≠ ∅)
Theorem	npss0 4240	No set is a proper subset of the empty set. (Contributed by NM, 17-Jun-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) (Proof shortened by JJ, 14-Jul-2021.)
⊢ ¬ 𝐴 ⊊ ∅
Theorem	pssv 4241	Any non-universal class is a proper subclass of the universal class. (Contributed by NM, 17-May-1998.)
⊢ (𝐴 ⊊ V ↔ ¬ 𝐴 = V)
Theorem	disj 4242*	Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 17-Feb-2004.)
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵)
Theorem	disjr 4243*	Two ways of saying that two classes are disjoint. (Contributed by Jeff Madsen, 19-Jun-2011.)
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥 ∈ 𝐵 ¬ 𝑥 ∈ 𝐴)
Theorem	disj1 4244*	Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 19-Aug-1993.)
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))
Theorem	reldisj 4245	Two ways of saying that two classes are disjoint, using the complement of 𝐵 relative to a universe 𝐶. (Contributed by NM, 15-Feb-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝐴 ⊆ 𝐶 → ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐴 ⊆ (𝐶 ∖ 𝐵)))
Theorem	disj3 4246	Two ways of saying that two classes are disjoint. (Contributed by NM, 19-May-1998.)
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐴 = (𝐴 ∖ 𝐵))
Theorem	disjne 4247	Members of disjoint sets are not equal. (Contributed by NM, 28-Mar-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → 𝐶 ≠ 𝐷)
Theorem	disjeq0 4248	Two disjoint sets are equal iff both are empty. (Contributed by AV, 19-Jun-2022.)
⊢ ((𝐴 ∩ 𝐵) = ∅ → (𝐴 = 𝐵 ↔ (𝐴 = ∅ ∧ 𝐵 = ∅)))
Theorem	disjel 4249	A set can't belong to both members of disjoint classes. (Contributed by NM, 28-Feb-2015.)
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝐶 ∈ 𝐴) → ¬ 𝐶 ∈ 𝐵)
Theorem	disj2 4250	Two ways of saying that two classes are disjoint. (Contributed by NM, 17-May-1998.)
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐴 ⊆ (V ∖ 𝐵))
Theorem	disj4 4251	Two ways of saying that two classes are disjoint. (Contributed by NM, 21-Mar-2004.)
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ¬ (𝐴 ∖ 𝐵) ⊊ 𝐴)
Theorem	ssdisj 4252	Intersection with a subclass of a disjoint class. (Contributed by FL, 24-Jan-2007.) (Proof shortened by JJ, 14-Jul-2021.)
⊢ ((𝐴 ⊆ 𝐵 ∧ (𝐵 ∩ 𝐶) = ∅) → (𝐴 ∩ 𝐶) = ∅)
Theorem	disjpss 4253	A class is a proper subset of its union with a disjoint nonempty class. (Contributed by NM, 15-Sep-2004.)
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝐵 ≠ ∅) → 𝐴 ⊊ (𝐴 ∪ 𝐵))
Theorem	undisj1 4254	The union of disjoint classes is disjoint. (Contributed by NM, 26-Sep-2004.)
⊢ (((𝐴 ∩ 𝐶) = ∅ ∧ (𝐵 ∩ 𝐶) = ∅) ↔ ((𝐴 ∪ 𝐵) ∩ 𝐶) = ∅)
Theorem	undisj2 4255	The union of disjoint classes is disjoint. (Contributed by NM, 13-Sep-2004.)
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ (𝐴 ∩ 𝐶) = ∅) ↔ (𝐴 ∩ (𝐵 ∪ 𝐶)) = ∅)
Theorem	ssindif0 4256	Subclass expressed in terms of intersection with difference from the universal class. (Contributed by NM, 17-Sep-2003.)
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ (V ∖ 𝐵)) = ∅)
Theorem	inelcm 4257	The intersection of classes with a common member is nonempty. (Contributed by NM, 7-Apr-1994.)
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → (𝐵 ∩ 𝐶) ≠ ∅)
Theorem	minel 4258	A minimum element of a class has no elements in common with the class. (Contributed by NM, 22-Jun-1994.) (Proof shortened by JJ, 14-Jul-2021.)
⊢ ((𝐴 ∈ 𝐵 ∧ (𝐶 ∩ 𝐵) = ∅) → ¬ 𝐴 ∈ 𝐶)
Theorem	undif4 4259	Distribute union over difference. (Contributed by NM, 17-May-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ((𝐴 ∩ 𝐶) = ∅ → (𝐴 ∪ (𝐵 ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ 𝐶))
Theorem	disjssun 4260	Subset relation for disjoint classes. (Contributed by NM, 25-Oct-2005.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ((𝐴 ∩ 𝐵) = ∅ → (𝐴 ⊆ (𝐵 ∪ 𝐶) ↔ 𝐴 ⊆ 𝐶))
Theorem	vdif0 4261	Universal class equality in terms of empty difference. (Contributed by NM, 17-Sep-2003.)
⊢ (𝐴 = V ↔ (V ∖ 𝐴) = ∅)
Theorem	difrab0eq 4262*	If the difference between the restricting class of a restricted class abstraction and the restricted class abstraction is empty, the restricting class is equal to this restricted class abstraction. (Contributed by Alexander van der Vekens, 31-Dec-2017.)
⊢ ((𝑉 ∖ {𝑥 ∈ 𝑉 ∣ 𝜑}) = ∅ ↔ 𝑉 = {𝑥 ∈ 𝑉 ∣ 𝜑})
Theorem	pssnel 4263*	A proper subclass has a member in one argument that's not in both. (Contributed by NM, 29-Feb-1996.)
⊢ (𝐴 ⊊ 𝐵 → ∃𝑥(𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴))
Theorem	disjdif 4264	A class and its relative complement are disjoint. Theorem 38 of [Suppes] p. 29. (Contributed by NM, 24-Mar-1998.)
⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅
Theorem	difin0 4265	The difference of a class from its intersection is empty. Theorem 37 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ((𝐴 ∩ 𝐵) ∖ 𝐵) = ∅
Theorem	unvdif 4266	The union of a class and its complement is the universe. Theorem 5.1(5) of [Stoll] p. 17. (Contributed by NM, 17-Aug-2004.)
⊢ (𝐴 ∪ (V ∖ 𝐴)) = V
Theorem	undif1 4267	Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4264). Theorem 35 of [Suppes] p. 29. (Contributed by NM, 19-May-1998.)
⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵)
Theorem	undif2 4268	Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4264). Part of proof of Corollary 6K of [Enderton] p. 144. (Contributed by NM, 19-May-1998.)
⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵)
Theorem	undifabs 4269	Absorption of difference by union. (Contributed by NM, 18-Aug-2013.)
⊢ (𝐴 ∪ (𝐴 ∖ 𝐵)) = 𝐴
Theorem	inundif 4270	The intersection and class difference of a class with another class unite to give the original class. (Contributed by Paul Chapman, 5-Jun-2009.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ((𝐴 ∩ 𝐵) ∪ (𝐴 ∖ 𝐵)) = 𝐴
Theorem	disjdif2 4271	The difference of a class and a class disjoint from it is the original class. (Contributed by BJ, 21-Apr-2019.)
⊢ ((𝐴 ∩ 𝐵) = ∅ → (𝐴 ∖ 𝐵) = 𝐴)
Theorem	difun2 4272	Absorption of union by difference. Theorem 36 of [Suppes] p. 29. (Contributed by NM, 19-May-1998.)
⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵)
Theorem	undif 4273	Union of complementary parts into whole. (Contributed by NM, 22-Mar-1998.)
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵)
Theorem	ssdifin0 4274	A subset of a difference does not intersect the subtrahend. (Contributed by Jeff Hankins, 1-Sep-2013.) (Proof shortened by Mario Carneiro, 24-Aug-2015.)
⊢ (𝐴 ⊆ (𝐵 ∖ 𝐶) → (𝐴 ∩ 𝐶) = ∅)
Theorem	ssdifeq0 4275	A class is a subclass of itself subtracted from another iff it is the empty set. (Contributed by Steve Rodriguez, 20-Nov-2015.)
⊢ (𝐴 ⊆ (𝐵 ∖ 𝐴) ↔ 𝐴 = ∅)
Theorem	ssundif 4276	A condition equivalent to inclusion in the union of two classes. (Contributed by NM, 26-Mar-2007.)
⊢ (𝐴 ⊆ (𝐵 ∪ 𝐶) ↔ (𝐴 ∖ 𝐵) ⊆ 𝐶)
Theorem	difcom 4277	Swap the arguments of a class difference. (Contributed by NM, 29-Mar-2007.)
⊢ ((𝐴 ∖ 𝐵) ⊆ 𝐶 ↔ (𝐴 ∖ 𝐶) ⊆ 𝐵)
Theorem	pssdifcom1 4278	Two ways to express overlapping subsets. (Contributed by Stefan O'Rear, 31-Oct-2014.)
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → ((𝐶 ∖ 𝐴) ⊊ 𝐵 ↔ (𝐶 ∖ 𝐵) ⊊ 𝐴))
Theorem	pssdifcom2 4279	Two ways to express non-covering pairs of subsets. (Contributed by Stefan O'Rear, 31-Oct-2014.)
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → (𝐵 ⊊ (𝐶 ∖ 𝐴) ↔ 𝐴 ⊊ (𝐶 ∖ 𝐵)))
Theorem	difdifdir 4280	Distributive law for class difference. Exercise 4.8 of [Stoll] p. 16. (Contributed by NM, 18-Aug-2004.)
⊢ ((𝐴 ∖ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∖ (𝐵 ∖ 𝐶))
Theorem	uneqdifeq 4281	Two ways to say that 𝐴 and 𝐵 partition 𝐶 (when 𝐴 and 𝐵 don't overlap and 𝐴 is a part of 𝐶). (Contributed by FL, 17-Nov-2008.) (Proof shortened by JJ, 14-Jul-2021.)
⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐴 ∪ 𝐵) = 𝐶 ↔ (𝐶 ∖ 𝐴) = 𝐵))
Theorem	raldifeq 4282*	Equality theorem for restricted universal quantifier. (Contributed by Thierry Arnoux, 6-Jul-2019.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → ∀𝑥 ∈ (𝐵 ∖ 𝐴)𝜓)    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓))
Theorem	r19.2z 4283*	Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 2026). The restricted version is valid only when the domain of quantification is not empty. (Contributed by NM, 15-Nov-2003.)
⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑥 ∈ 𝐴 𝜑)
Theorem	r19.2zb 4284*	A response to the notion that the condition 𝐴 ≠ ∅ can be removed in r19.2z 4283. Interestingly enough, 𝜑 does not figure in the left-hand side. (Contributed by Jeff Hankins, 24-Aug-2009.)
⊢ (𝐴 ≠ ∅ ↔ (∀𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜑))
Theorem	r19.3rz 4285*	Restricted quantification of wff not containing quantified variable. (Contributed by FL, 3-Jan-2008.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (𝐴 ≠ ∅ → (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑))
Theorem	r19.28z 4286*	Restricted quantifier version of Theorem 19.28 of [Margaris] p. 90. It is valid only when the domain of quantification is not empty. (Contributed by NM, 26-Oct-2010.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓)))
Theorem	r19.3rzv 4287*	Restricted quantification of wff not containing quantified variable. (Contributed by NM, 10-Mar-1997.)
⊢ (𝐴 ≠ ∅ → (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑))
Theorem	r19.9rzv 4288*	Restricted quantification of wff not containing quantified variable. (Contributed by NM, 27-May-1998.)
⊢ (𝐴 ≠ ∅ → (𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜑))
Theorem	r19.28zv 4289*	Restricted quantifier version of Theorem 19.28 of [Margaris] p. 90. It is valid only when the domain of quantification is not empty. (Contributed by NM, 19-Aug-2004.)
⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓)))
Theorem	r19.37zv 4290*	Restricted quantifier version of Theorem 19.37 of [Margaris] p. 90. It is valid only when the domain of quantification is not empty. (Contributed by Paul Chapman, 8-Oct-2007.)
⊢ (𝐴 ≠ ∅ → (∃𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)))
Theorem	r19.45zv 4291*	Restricted version of Theorem 19.45 of [Margaris] p. 90. (Contributed by NM, 27-May-1998.)
⊢ (𝐴 ≠ ∅ → (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓)))
Theorem	r19.44zv 4292*	Restricted version of Theorem 19.44 of [Margaris] p. 90. (Contributed by NM, 27-May-1998.)
⊢ (𝐴 ≠ ∅ → (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ 𝜓)))
Theorem	r19.27z 4293*	Restricted quantifier version of Theorem 19.27 of [Margaris] p. 90. It is valid only when the domain of quantification is not empty. (Contributed by NM, 26-Oct-2010.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ 𝜓)))
Theorem	r19.27zv 4294*	Restricted quantifier version of Theorem 19.27 of [Margaris] p. 90. It is valid only when the domain of quantification is not empty. (Contributed by NM, 19-Aug-2004.)
⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ 𝜓)))
Theorem	r19.36zv 4295*	Restricted quantifier version of Theorem 19.36 of [Margaris] p. 90. It is valid only when the domain of quantification is not empty. (Contributed by NM, 20-Sep-2003.)
⊢ (𝐴 ≠ ∅ → (∃𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 → 𝜓)))
Theorem	rzal 4296*	Vacuous quantification is always true. (Contributed by NM, 11-Mar-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 𝜑)
Theorem	rexn0 4297*	Restricted existential quantification implies its restriction is nonempty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.)
⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝐴 ≠ ∅)
Theorem	ralidm 4298*	Idempotent law for restricted quantifier. (Contributed by NM, 28-Mar-1997.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑)
Theorem	ral0 4299	Vacuous universal quantification is always true. (Contributed by NM, 20-Oct-2005.)
⊢ ∀𝑥 ∈ ∅ 𝜑
Theorem	ralf0 4300*	The quantification of a falsehood is vacuous when true. (Contributed by NM, 26-Nov-2005.) (Proof shortened by JJ, 14-Jul-2021.)
⊢ ¬ 𝜑    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ 𝐴 = ∅)