P. 45 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 4401-4500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sbcnestgf 4401	Nest the composition of two substitutions. Usage of this theorem is discouraged because it depends on ax-13 2376. Use the weaker sbcnestgfw 4396 when possible. (Contributed by Mario Carneiro, 11-Nov-2016.) (New usage is discouraged.)
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑦Ⅎ𝑥𝜑) → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦]𝜑))
Theorem	csbnestgf 4402	Nest the composition of two substitutions. Usage of this theorem is discouraged because it depends on ax-13 2376. Use the weaker csbnestgfw 4397 when possible. (Contributed by NM, 23-Nov-2005.) (Proof shortened by Mario Carneiro, 10-Nov-2016.) (New usage is discouraged.)
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑦Ⅎ𝑥𝐶) → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = ⦋⦋𝐴 / 𝑥⦌𝐵 / 𝑦⦌𝐶)
Theorem	sbcnestg 4403*	Nest the composition of two substitutions. Usage of this theorem is discouraged because it depends on ax-13 2376. Use the weaker sbcnestgw 4398 when possible. (Contributed by NM, 27-Nov-2005.) (Proof shortened by Mario Carneiro, 11-Nov-2016.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦]𝜑))
Theorem	csbnestg 4404*	Nest the composition of two substitutions. Usage of this theorem is discouraged because it depends on ax-13 2376. Use the weaker csbnestgw 4399 when possible. (Contributed by NM, 23-Nov-2005.) (Proof shortened by Mario Carneiro, 10-Nov-2016.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = ⦋⦋𝐴 / 𝑥⦌𝐵 / 𝑦⦌𝐶)
Theorem	sbcco3g 4405*	Composition of two substitutions. Usage of this theorem is discouraged because it depends on ax-13 2376. Use the weaker sbcco3gw 4400 when possible. (Contributed by NM, 27-Nov-2005.) (Revised by Mario Carneiro, 11-Nov-2016.) (New usage is discouraged.)
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [𝐶 / 𝑦]𝜑))
Theorem	csbco3g 4406*	Composition of two class substitutions. Usage of this theorem is discouraged because it depends on ax-13 2376. (Contributed by NM, 27-Nov-2005.) (Revised by Mario Carneiro, 11-Nov-2016.) (New usage is discouraged.)
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐷 = ⦋𝐶 / 𝑦⦌𝐷)
Theorem	csbnest1g 4407	Nest the composition of two substitutions. (Contributed by NM, 23-May-2006.) (Proof shortened by Mario Carneiro, 11-Nov-2016.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑥⦌𝐶 = ⦋⦋𝐴 / 𝑥⦌𝐵 / 𝑥⦌𝐶)
Theorem	csbidm 4408*	Idempotent law for class substitutions. (Contributed by NM, 1-Mar-2008.) (Revised by NM, 18-Aug-2018.)
⊢ ⦋𝐴 / 𝑥⦌⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵
Theorem	csbvarg 4409	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 4410	The proper substitution of a class for a setvar variable results in the class (if the class exists), in inference form of csbvarg 4409. (Contributed by Giovanni Mascellani, 30-May-2019.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ⦋𝐴 / 𝑥⦌𝑥 = 𝐴
Theorem	sbccsb 4411*	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 4412	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 4413*	Special case related to rspsbc 3854. (Contributed by NM, 10-Dec-2005.) (Proof shortened by Eric Schmidt, 17-Jan-2007.)
⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝐶 ∈ 𝐷) → ⦋𝐴 / 𝑥⦌𝐶 ∈ 𝐷)
Theorem	sbnfc2 4414*	Two ways of expressing "𝑥 is (effectively) not free in 𝐴". (Contributed by Mario Carneiro, 14-Oct-2016.)
⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦∀𝑧⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑧 / 𝑥⦌𝐴)
Theorem	csbab 4415*	Move substitution into a class abstraction. (Contributed by NM, 13-Dec-2005.) (Revised by NM, 19-Aug-2018.)
⊢ ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝜑} = {𝑦 ∣ [𝐴 / 𝑥]𝜑}
Theorem	csbun 4416	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 4417	Distribute proper substitution into a class through an intersection relation. (Contributed by Alan Sare, 22-Jul-2012.) (Revised by NM, 18-Aug-2018.)
⊢ ⦋𝐴 / 𝑥⦌(𝐵 ∩ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∩ ⦋𝐴 / 𝑥⦌𝐶)
Theorem	csbie2df 4418*	Conversion of implicit substitution to explicit class substitution. This version of csbiedf 3904 avoids a disjointness condition on 𝑥, 𝐴 and 𝑥, 𝐷 by substituting twice. Deduction form of csbie2 3913. (Contributed by AV, 29-Mar-2024.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐶)    &   ⊢ (𝜑 → Ⅎ𝑥𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑦 = 𝐴) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐷)
Theorem	2nreu 4419*	If there are two different sets fulfilling a wff (by implicit substitution), then there is no unique set fulfilling the wff. (Contributed by AV, 20-Jun-2023.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))    ⇒   ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) → ((𝜓 ∧ 𝜒) → ¬ ∃!𝑥 ∈ 𝑋 𝜑))
Theorem	un00 4420	Two classes are empty iff their union is empty. (Contributed by NM, 11-Aug-2004.)
⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) ↔ (𝐴 ∪ 𝐵) = ∅)
Theorem	vss 4421	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 4422	The null set is a proper subset of any nonempty set. (Contributed by NM, 27-Feb-1996.)
⊢ (∅ ⊊ 𝐴 ↔ 𝐴 ≠ ∅)
Theorem	npss0 4423	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 4424	Any non-universal class is a proper subclass of the universal class. (Contributed by NM, 17-May-1998.)
⊢ (𝐴 ⊊ V ↔ ¬ 𝐴 = V)
Theorem	disj 4425*	Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 17-Feb-2004.) Avoid ax-10 2141, ax-11 2157, ax-12 2177. (Revised by GG, 28-Jun-2024.)
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵)
Theorem	disjr 4426*	Two ways of saying that two classes are disjoint. (Contributed by Jeff Madsen, 19-Jun-2011.)
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥 ∈ 𝐵 ¬ 𝑥 ∈ 𝐴)
Theorem	disj1 4427*	Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 19-Aug-1993.)
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))
Theorem	reldisj 4428	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.) Avoid ax-12 2177. (Revised by GG, 28-Jun-2024.)
⊢ (𝐴 ⊆ 𝐶 → ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐴 ⊆ (𝐶 ∖ 𝐵)))
Theorem	disj3 4429	Two ways of saying that two classes are disjoint. (Contributed by NM, 19-May-1998.)
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐴 = (𝐴 ∖ 𝐵))
Theorem	disjne 4430	Members of disjoint sets are not equal. (Contributed by NM, 28-Mar-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → 𝐶 ≠ 𝐷)
Theorem	disjeq0 4431	Two disjoint sets are equal iff both are empty. (Contributed by AV, 19-Jun-2022.)
⊢ ((𝐴 ∩ 𝐵) = ∅ → (𝐴 = 𝐵 ↔ (𝐴 = ∅ ∧ 𝐵 = ∅)))
Theorem	disjel 4432	A set can't belong to both members of disjoint classes. (Contributed by NM, 28-Feb-2015.)
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝐶 ∈ 𝐴) → ¬ 𝐶 ∈ 𝐵)
Theorem	disj2 4433	Two ways of saying that two classes are disjoint. (Contributed by NM, 17-May-1998.)
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐴 ⊆ (V ∖ 𝐵))
Theorem	disj4 4434	Two ways of saying that two classes are disjoint. (Contributed by NM, 21-Mar-2004.)
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ¬ (𝐴 ∖ 𝐵) ⊊ 𝐴)
Theorem	ssdisj 4435	Intersection with a subclass of a disjoint class. (Contributed by FL, 24-Jan-2007.) (Proof shortened by JJ, 14-Jul-2021.)
⊢ ((𝐴 ⊆ 𝐵 ∧ (𝐵 ∩ 𝐶) = ∅) → (𝐴 ∩ 𝐶) = ∅)
Theorem	disjpss 4436	A class is a proper subset of its union with a disjoint nonempty class. (Contributed by NM, 15-Sep-2004.)
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝐵 ≠ ∅) → 𝐴 ⊊ (𝐴 ∪ 𝐵))
Theorem	undisj1 4437	The union of disjoint classes is disjoint. (Contributed by NM, 26-Sep-2004.)
⊢ (((𝐴 ∩ 𝐶) = ∅ ∧ (𝐵 ∩ 𝐶) = ∅) ↔ ((𝐴 ∪ 𝐵) ∩ 𝐶) = ∅)
Theorem	undisj2 4438	The union of disjoint classes is disjoint. (Contributed by NM, 13-Sep-2004.)
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ (𝐴 ∩ 𝐶) = ∅) ↔ (𝐴 ∩ (𝐵 ∪ 𝐶)) = ∅)
Theorem	ssindif0 4439	Subclass expressed in terms of intersection with difference from the universal class. (Contributed by NM, 17-Sep-2003.)
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ (V ∖ 𝐵)) = ∅)
Theorem	inelcm 4440	The intersection of classes with a common member is nonempty. (Contributed by NM, 7-Apr-1994.)
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → (𝐵 ∩ 𝐶) ≠ ∅)
Theorem	minel 4441	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 4442	Distribute union over difference. (Contributed by NM, 17-May-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ((𝐴 ∩ 𝐶) = ∅ → (𝐴 ∪ (𝐵 ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ 𝐶))
Theorem	disjssun 4443	Subset relation for disjoint classes. (Contributed by NM, 25-Oct-2005.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ((𝐴 ∩ 𝐵) = ∅ → (𝐴 ⊆ (𝐵 ∪ 𝐶) ↔ 𝐴 ⊆ 𝐶))
Theorem	vdif0 4444	Universal class equality in terms of empty difference. (Contributed by NM, 17-Sep-2003.)
⊢ (𝐴 = V ↔ (V ∖ 𝐴) = ∅)
Theorem	difrab0eq 4445*	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 4446*	A proper subclass has a member in one argument that's not in both. (Contributed by NM, 29-Feb-1996.)
⊢ (𝐴 ⊊ 𝐵 → ∃𝑥(𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴))
Theorem	disjdif 4447	A class and its relative complement are disjoint. Theorem 38 of [Suppes] p. 29. (Contributed by NM, 24-Mar-1998.)
⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅
Theorem	disjdifr 4448	A class and its relative complement are disjoint. (Contributed by Thierry Arnoux, 29-Nov-2023.)
⊢ ((𝐵 ∖ 𝐴) ∩ 𝐴) = ∅
Theorem	difin0 4449	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 4450	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 4451	Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4447). Theorem 35 of [Suppes] p. 29. (Contributed by NM, 19-May-1998.)
⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵)
Theorem	undif2 4452	Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4447). Part of proof of Corollary 6K of [Enderton] p. 144. (Contributed by NM, 19-May-1998.)
⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵)
Theorem	undifabs 4453	Absorption of difference by union. (Contributed by NM, 18-Aug-2013.)
⊢ (𝐴 ∪ (𝐴 ∖ 𝐵)) = 𝐴
Theorem	inundif 4454	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 4455	The difference of a class and a class disjoint from it is the original class. (Contributed by BJ, 21-Apr-2019.)
⊢ ((𝐴 ∩ 𝐵) = ∅ → (𝐴 ∖ 𝐵) = 𝐴)
Theorem	difun2 4456	Absorption of union by difference. Theorem 36 of [Suppes] p. 29. (Contributed by NM, 19-May-1998.)
⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵)
Theorem	undif 4457	Union of complementary parts into whole. (Contributed by NM, 22-Mar-1998.)
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵)
Theorem	undifr 4458	Union of complementary parts into whole. (Contributed by Thierry Arnoux, 21-Nov-2023.) (Proof shortened by SN, 11-Mar-2025.)
⊢ (𝐴 ⊆ 𝐵 ↔ ((𝐵 ∖ 𝐴) ∪ 𝐴) = 𝐵)
Theorem	undifrOLD 4459	Obsolete version of undifr 4458 as of 11-Mar-2025. (Contributed by Thierry Arnoux, 21-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ⊆ 𝐵 ↔ ((𝐵 ∖ 𝐴) ∪ 𝐴) = 𝐵)
Theorem	undif5 4460	An equality involving class union and class difference. (Contributed by Thierry Arnoux, 26-Jun-2024.)
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐴 ∪ 𝐵) ∖ 𝐵) = 𝐴)
Theorem	ssdifin0 4461	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 4462	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 4463	A condition equivalent to inclusion in the union of two classes. (Contributed by NM, 26-Mar-2007.)
⊢ (𝐴 ⊆ (𝐵 ∪ 𝐶) ↔ (𝐴 ∖ 𝐵) ⊆ 𝐶)
Theorem	difcom 4464	Swap the arguments of a class difference. (Contributed by NM, 29-Mar-2007.)
⊢ ((𝐴 ∖ 𝐵) ⊆ 𝐶 ↔ (𝐴 ∖ 𝐶) ⊆ 𝐵)
Theorem	pssdifcom1 4465	Two ways to express overlapping subsets. (Contributed by Stefan O'Rear, 31-Oct-2014.)
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → ((𝐶 ∖ 𝐴) ⊊ 𝐵 ↔ (𝐶 ∖ 𝐵) ⊊ 𝐴))
Theorem	pssdifcom2 4466	Two ways to express non-covering pairs of subsets. (Contributed by Stefan O'Rear, 31-Oct-2014.)
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → (𝐵 ⊊ (𝐶 ∖ 𝐴) ↔ 𝐴 ⊊ (𝐶 ∖ 𝐵)))
Theorem	difdifdir 4467	Distributive law for class difference. Exercise 4.8 of [Stoll] p. 16. (Contributed by NM, 18-Aug-2004.)
⊢ ((𝐴 ∖ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∖ (𝐵 ∖ 𝐶))
Theorem	uneqdifeq 4468	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 4469*	Equality theorem for restricted universal quantifier. (Contributed by Thierry Arnoux, 6-Jul-2019.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → ∀𝑥 ∈ (𝐵 ∖ 𝐴)𝜓)    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓))
Theorem	r19.2z 4470*	Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1976). The restricted version is valid only when the domain of quantification is not empty. (Contributed by NM, 15-Nov-2003.)
⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑥 ∈ 𝐴 𝜑)
Theorem	r19.2zb 4471*	A response to the notion that the condition 𝐴 ≠ ∅ can be removed in r19.2z 4470. Interestingly enough, 𝜑 does not figure in the left-hand side. (Contributed by Jeff Hankins, 24-Aug-2009.)
⊢ (𝐴 ≠ ∅ ↔ (∀𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜑))
Theorem	r19.3rz 4472*	Restricted quantification of wff not containing quantified variable. (Contributed by FL, 3-Jan-2008.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (𝐴 ≠ ∅ → (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑))
Theorem	r19.28z 4473*	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 4474*	Restricted quantification of wff not containing quantified variable. (Contributed by NM, 10-Mar-1997.)
⊢ (𝐴 ≠ ∅ → (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑))
Theorem	r19.9rzv 4475*	Restricted quantification of wff not containing quantified variable. (Contributed by NM, 27-May-1998.)
⊢ (𝐴 ≠ ∅ → (𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜑))
Theorem	r19.28zv 4476*	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 4477*	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 4478*	Restricted version of Theorem 19.45 of [Margaris] p. 90. (Contributed by NM, 27-May-1998.)
⊢ (𝐴 ≠ ∅ → (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓)))
Theorem	r19.44zv 4479*	Restricted version of Theorem 19.44 of [Margaris] p. 90. (Contributed by NM, 27-May-1998.)
⊢ (𝐴 ≠ ∅ → (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ 𝜓)))
Theorem	r19.27z 4480*	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 4481*	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 4482*	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	ralidmw 4483*	Idempotent law for restricted quantifier. Weak version of ralidm 4487, which does not require ax-10 2141, ax-12 2177, but requires ax-8 2110. (Contributed by GG, 30-Sep-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑)
Theorem	rzal 4484*	Vacuous quantification is always true. (Contributed by NM, 11-Mar-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) Avoid df-clel 2809, ax-8 2110. (Revised by GG, 2-Sep-2024.)
⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 𝜑)
Theorem	rzalALT 4485*	Alternate proof of rzal 4484. Shorter, but requiring df-clel 2809, ax-8 2110. (Contributed by NM, 11-Mar-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 𝜑)
Theorem	rexn0 4486*	Restricted existential quantification implies its restriction is nonempty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) Avoid df-clel 2809, ax-8 2110. (Revised by GG, 2-Sep-2024.)
⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝐴 ≠ ∅)
Theorem	ralidm 4487	Idempotent law for restricted quantifier. (Contributed by NM, 28-Mar-1997.) Reduce axiom usage. (Revised by GG, 2-Sep-2024.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑)
Theorem	ral0 4488	Vacuous universal quantification is always true. (Contributed by NM, 20-Oct-2005.) Avoid df-clel 2809, ax-8 2110. (Revised by GG, 2-Sep-2024.)
⊢ ∀𝑥 ∈ ∅ 𝜑
Theorem	ralf0 4489*	The quantification of a falsehood is vacuous when true. (Contributed by NM, 26-Nov-2005.) (Proof shortened by JJ, 14-Jul-2021.) Avoid df-clel 2809, ax-8 2110. (Revised by GG, 2-Sep-2024.)
⊢ ¬ 𝜑    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ 𝐴 = ∅)
Theorem	ralnralall 4490*	A contradiction concerning restricted generalization for a nonempty set implies anything. (Contributed by Alexander van der Vekens, 4-Sep-2018.)
⊢ (𝐴 ≠ ∅ → ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 ¬ 𝜑) → 𝜓))
Theorem	falseral0 4491*	A false statement can only be true for elements of an empty set. (Contributed by AV, 30-Oct-2020.)
⊢ ((∀𝑥 ¬ 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜑) → 𝐴 = ∅)
Theorem	raaan 4492*	Rearrange restricted quantifiers. (Contributed by NM, 26-Oct-2010.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐴 𝜓))
Theorem	raaanv 4493*	Rearrange restricted quantifiers. (Contributed by NM, 11-Mar-1997.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐴 𝜓))
Theorem	sbss 4494*	Set substitution into the first argument of a subset relation. (Contributed by Rodolfo Medina, 7-Jul-2010.) (Proof shortened by Mario Carneiro, 14-Nov-2016.)
⊢ ([𝑦 / 𝑥]𝑥 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴)
Theorem	sbcssg 4495	Distribute proper substitution through a subclass relation. (Contributed by Alan Sare, 22-Jul-2012.) (Proof shortened by Alexander van der Vekens, 23-Jul-2017.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 ⊆ 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 ⊆ ⦋𝐴 / 𝑥⦌𝐶))
Theorem	raaan2 4496*	Rearrange restricted quantifiers with two different restricting classes, analogous to raaan 4492. It is necessary that either both restricting classes are empty or both are not empty. (Contributed by Alexander van der Vekens, 29-Jun-2017.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ ((𝐴 = ∅ ↔ 𝐵 = ∅) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)))
Theorem	2reu4lem 4497*	Lemma for 2reu4 4498. (Contributed by Alexander van der Vekens, 1-Jul-2017.)
⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))))
Theorem	2reu4 4498*	Definition of double restricted existential uniqueness ("exactly one 𝑥 and exactly one 𝑦"), analogous to 2eu4 2654. (Contributed by Alexander van der Vekens, 1-Jul-2017.)
⊢ ((∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))))
Theorem	csbdif 4499	Distribution of class substitution over difference of two classes. (Contributed by ML, 14-Jul-2020.)
⊢ ⦋𝐴 / 𝑥⦌(𝐵 ∖ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∖ ⦋𝐴 / 𝑥⦌𝐶)
2.1.15  The conditional operator for classes This subsection introduces the conditional operator for classes, denoted by if(𝜑, 𝐴, 𝐵) (see df-if 4501). It is the analogue for classes of the conditional operator for propositions, denoted by if-(𝜑, 𝜓, 𝜒) (see df-ifp 1063).
Syntax	cif 4500	Extend class notation to include the conditional operator for classes.
class if(𝜑, 𝐴, 𝐵)