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	disjpss 4401	A class is a proper subset of its union with a disjoint nonempty class. (Contributed by NM, 15-Sep-2004.)
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝐵 ≠ ∅) → 𝐴 ⊊ (𝐴 ∪ 𝐵))
Theorem	undisj1 4402	The union of disjoint classes is disjoint. (Contributed by NM, 26-Sep-2004.)
⊢ (((𝐴 ∩ 𝐶) = ∅ ∧ (𝐵 ∩ 𝐶) = ∅) ↔ ((𝐴 ∪ 𝐵) ∩ 𝐶) = ∅)
Theorem	undisj2 4403	The union of disjoint classes is disjoint. (Contributed by NM, 13-Sep-2004.)
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ (𝐴 ∩ 𝐶) = ∅) ↔ (𝐴 ∩ (𝐵 ∪ 𝐶)) = ∅)
Theorem	ssindif0 4404	Subclass expressed in terms of intersection with difference from the universal class. (Contributed by NM, 17-Sep-2003.)
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ (V ∖ 𝐵)) = ∅)
Theorem	inelcm 4405	The intersection of classes with a common member is nonempty. (Contributed by NM, 7-Apr-1994.)
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → (𝐵 ∩ 𝐶) ≠ ∅)
Theorem	minel 4406	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 4407	Distribute union over difference. (Contributed by NM, 17-May-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ((𝐴 ∩ 𝐶) = ∅ → (𝐴 ∪ (𝐵 ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ 𝐶))
Theorem	disjssun 4408	Subset relation for disjoint classes. (Contributed by NM, 25-Oct-2005.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ((𝐴 ∩ 𝐵) = ∅ → (𝐴 ⊆ (𝐵 ∪ 𝐶) ↔ 𝐴 ⊆ 𝐶))
Theorem	vdif0 4409	Universal class equality in terms of empty difference. (Contributed by NM, 17-Sep-2003.)
⊢ (𝐴 = V ↔ (V ∖ 𝐴) = ∅)
Theorem	difrab0eq 4410*	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 4411*	A proper subclass has a member in one argument that's not in both. (Contributed by NM, 29-Feb-1996.)
⊢ (𝐴 ⊊ 𝐵 → ∃𝑥(𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴))
Theorem	disjdif 4412	A class and its relative complement are disjoint. Theorem 38 of [Suppes] p. 29. (Contributed by NM, 24-Mar-1998.)
⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅
Theorem	disjdifr 4413	A class and its relative complement are disjoint. (Contributed by Thierry Arnoux, 29-Nov-2023.)
⊢ ((𝐵 ∖ 𝐴) ∩ 𝐴) = ∅
Theorem	difin0 4414	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 4415	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 4416	Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4412). Theorem 35 of [Suppes] p. 29. (Contributed by NM, 19-May-1998.)
⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵)
Theorem	undif2 4417	Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4412). Part of proof of Corollary 6K of [Enderton] p. 144. (Contributed by NM, 19-May-1998.)
⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵)
Theorem	undifabs 4418	Absorption of difference by union. (Contributed by NM, 18-Aug-2013.)
⊢ (𝐴 ∪ (𝐴 ∖ 𝐵)) = 𝐴
Theorem	inundif 4419	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 4420	The difference of a class and a class disjoint from it is the original class. (Contributed by BJ, 21-Apr-2019.)
⊢ ((𝐴 ∩ 𝐵) = ∅ → (𝐴 ∖ 𝐵) = 𝐴)
Theorem	difun2 4421	Absorption of union by difference. Theorem 36 of [Suppes] p. 29. (Contributed by NM, 19-May-1998.)
⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵)
Theorem	undif 4422	Union of complementary parts into whole. (Contributed by NM, 22-Mar-1998.)
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵)
Theorem	undifr 4423	Union of complementary parts into whole. (Contributed by Thierry Arnoux, 21-Nov-2023.) (Proof shortened by SN, 11-Mar-2025.)
⊢ (𝐴 ⊆ 𝐵 ↔ ((𝐵 ∖ 𝐴) ∪ 𝐴) = 𝐵)
Theorem	undif5 4424	An equality involving class union and class difference. (Contributed by Thierry Arnoux, 26-Jun-2024.)
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐴 ∪ 𝐵) ∖ 𝐵) = 𝐴)
Theorem	ssdifin0 4425	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 4426	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 4427	A condition equivalent to inclusion in the union of two classes. (Contributed by NM, 26-Mar-2007.)
⊢ (𝐴 ⊆ (𝐵 ∪ 𝐶) ↔ (𝐴 ∖ 𝐵) ⊆ 𝐶)
Theorem	difcom 4428	Swap the arguments of a class difference. (Contributed by NM, 29-Mar-2007.)
⊢ ((𝐴 ∖ 𝐵) ⊆ 𝐶 ↔ (𝐴 ∖ 𝐶) ⊆ 𝐵)
Theorem	pssdifcom1 4429	Two ways to express overlapping subsets. (Contributed by Stefan O'Rear, 31-Oct-2014.)
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → ((𝐶 ∖ 𝐴) ⊊ 𝐵 ↔ (𝐶 ∖ 𝐵) ⊊ 𝐴))
Theorem	pssdifcom2 4430	Two ways to express non-covering pairs of subsets. (Contributed by Stefan O'Rear, 31-Oct-2014.)
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → (𝐵 ⊊ (𝐶 ∖ 𝐴) ↔ 𝐴 ⊊ (𝐶 ∖ 𝐵)))
Theorem	difdifdir 4431	Distributive law for class difference. Exercise 4.8 of [Stoll] p. 16. (Contributed by NM, 18-Aug-2004.)
⊢ ((𝐴 ∖ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∖ (𝐵 ∖ 𝐶))
Theorem	uneqdifeq 4432	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 4433*	Equality theorem for restricted universal quantifier. (Contributed by Thierry Arnoux, 6-Jul-2019.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → ∀𝑥 ∈ (𝐵 ∖ 𝐴)𝜓)    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓))
Theorem	rzal 4434*	Vacuous quantification is always true. (Contributed by NM, 11-Mar-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) Avoid df-clel 2811, ax-8 2116. (Revised by GG, 2-Sep-2024.)
⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 𝜑)
Theorem	rzalALT 4435*	Alternate proof of rzal 4434. Shorter, but requiring df-clel 2811, ax-8 2116. (Contributed by NM, 11-Mar-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 𝜑)
Theorem	rexn0 4436*	Restricted existential quantification implies its restriction is nonempty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) Avoid df-clel 2811, ax-8 2116. (Revised by GG, 2-Sep-2024.)
⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝐴 ≠ ∅)
Theorem	ralf0 4437*	The quantification of a falsehood is vacuous when true. (Contributed by NM, 26-Nov-2005.) (Proof shortened by JJ, 14-Jul-2021.)
⊢ ¬ 𝜑    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ 𝐴 = ∅)
Theorem	ral0 4438	Vacuous universal quantification is always true. (Contributed by NM, 20-Oct-2005.) Avoid df-clel 2811, ax-8 2116. (Revised by GG, 2-Sep-2024.)
⊢ ∀𝑥 ∈ ∅ 𝜑
Theorem	r19.2z 4439*	Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1978). The restricted version is valid only when the domain of quantification is not empty. (Contributed by NM, 15-Nov-2003.)
⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑥 ∈ 𝐴 𝜑)
Theorem	r19.2zb 4440*	A response to the notion that the condition 𝐴 ≠ ∅ can be removed in r19.2z 4439. Interestingly enough, 𝜑 does not figure in the left-hand side. (Contributed by Jeff Hankins, 24-Aug-2009.)
⊢ (𝐴 ≠ ∅ ↔ (∀𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜑))
Theorem	r19.3rz 4441*	Restricted quantification of wff not containing quantified variable. (Contributed by FL, 3-Jan-2008.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (𝐴 ≠ ∅ → (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑))
Theorem	r19.28z 4442*	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 4443*	Restricted quantification of wff not containing quantified variable. (Contributed by NM, 10-Mar-1997.) Avoid ax-12 2185. (Revised by TM, 16-Feb-2026.)
⊢ (𝐴 ≠ ∅ → (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑))
Theorem	r19.3rzvOLD 4444*	Obsolete version of r19.3rzv 4443 as of 16-Feb-2026. (Contributed by NM, 10-Mar-1997.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ≠ ∅ → (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑))
Theorem	r19.9rzv 4445*	Restricted quantification of wff not containing quantified variable. (Contributed by NM, 27-May-1998.)
⊢ (𝐴 ≠ ∅ → (𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜑))
Theorem	r19.28zv 4446*	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 4447*	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 4448*	Restricted version of Theorem 19.45 of [Margaris] p. 90. (Contributed by NM, 27-May-1998.)
⊢ (𝐴 ≠ ∅ → (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓)))
Theorem	r19.44zv 4449*	Restricted version of Theorem 19.44 of [Margaris] p. 90. (Contributed by NM, 27-May-1998.)
⊢ (𝐴 ≠ ∅ → (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ 𝜓)))
Theorem	r19.27z 4450*	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 4451*	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 4452*	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	ralnralall 4453*	A contradiction concerning restricted generalization for a nonempty set implies anything. (Contributed by Alexander van der Vekens, 4-Sep-2018.)
⊢ (𝐴 ≠ ∅ → ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 ¬ 𝜑) → 𝜓))
Theorem	falseral0 4454*	A false statement can only be true for elements of an empty set. (Contributed by AV, 30-Oct-2020.) (Proof shortened by TM, 16-Feb-2026.)
⊢ ((∀𝑥 ¬ 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜑) → 𝐴 = ∅)
Theorem	falseral0OLD 4455*	Obsolete version of falseral0 4454 as of 16-Feb-2026. (Contributed by AV, 30-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((∀𝑥 ¬ 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜑) → 𝐴 = ∅)
Theorem	ralidmw 4456*	Idempotent law for restricted quantifier. Weak version of ralidm 4457, which does not require ax-10 2147, ax-12 2185, but requires ax-8 2116. (Contributed by GG, 30-Sep-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑)
Theorem	ralidm 4457	Idempotent law for restricted quantifier. (Contributed by NM, 28-Mar-1997.) Reduce axiom usage. (Revised by GG, 2-Sep-2024.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑)
Theorem	raaan 4458*	Rearrange restricted quantifiers. (Contributed by NM, 26-Oct-2010.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐴 𝜓))
Theorem	raaanv 4459*	Rearrange restricted quantifiers. (Contributed by NM, 11-Mar-1997.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐴 𝜓))
Theorem	sbss 4460*	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 4461	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 4462*	Rearrange restricted quantifiers with two different restricting classes, analogous to raaan 4458. 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 4463*	Lemma for 2reu4 4464. (Contributed by Alexander van der Vekens, 1-Jul-2017.)
⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))))
Theorem	2reu4 4464*	Definition of double restricted existential uniqueness ("exactly one 𝑥 and exactly one 𝑦"), analogous to 2eu4 2655. (Contributed by Alexander van der Vekens, 1-Jul-2017.)
⊢ ((∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))))
Theorem	csbdif 4465	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 4467). It is the analogue for classes of the conditional operator for propositions, denoted by if-(𝜑, 𝜓, 𝜒) (see df-ifp 1064).
Syntax	cif 4466	Extend class notation to include the conditional operator for classes.
class if(𝜑, 𝐴, 𝐵)
Definition	df-if 4467*	Definition of the conditional operator for classes. The expression if(𝜑, 𝐴, 𝐵) is read "if 𝜑 then 𝐴 else 𝐵". See iftrue 4472 and iffalse 4475 for its values. In the mathematical literature, this operator is rarely defined formally but is implicit in informal definitions such as "let f(x)=0 if x=0 and 1/x otherwise". An important use for us is in conjunction with the weak deduction theorem, which is described in the next section, beginning at dedth 4525. (Contributed by NM, 15-May-1999.)
⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))}
Theorem	dfif2 4468*	An alternate definition of the conditional operator df-if 4467 with one fewer connectives (but probably less intuitive to understand). (Contributed by NM, 30-Jan-2006.)
⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜑))}
Theorem	dfif6 4469*	An alternate definition of the conditional operator df-if 4467 as a simple class abstraction. (Contributed by Mario Carneiro, 8-Sep-2013.)
⊢ if(𝜑, 𝐴, 𝐵) = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐵 ∣ ¬ 𝜑})
Theorem	ifeq1 4470	Equality theorem for conditional operator. (Contributed by NM, 1-Sep-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
⊢ (𝐴 = 𝐵 → if(𝜑, 𝐴, 𝐶) = if(𝜑, 𝐵, 𝐶))
Theorem	ifeq2 4471	Equality theorem for conditional operator. (Contributed by NM, 1-Sep-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
⊢ (𝐴 = 𝐵 → if(𝜑, 𝐶, 𝐴) = if(𝜑, 𝐶, 𝐵))
Theorem	iftrue 4472	Value of the conditional operator when its first argument is true. (Contributed by NM, 15-May-1999.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
Theorem	iftruei 4473	Inference associated with iftrue 4472. (Contributed by BJ, 7-Oct-2018.)
⊢ 𝜑    ⇒   ⊢ if(𝜑, 𝐴, 𝐵) = 𝐴
Theorem	iftrued 4474	Value of the conditional operator when its first argument is true. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝜒)    ⇒   ⊢ (𝜑 → if(𝜒, 𝐴, 𝐵) = 𝐴)
Theorem	iffalse 4475	Value of the conditional operator when its first argument is false. (Contributed by NM, 14-Aug-1999.)
⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
Theorem	iffalsei 4476	Inference associated with iffalse 4475. (Contributed by BJ, 7-Oct-2018.)
⊢ ¬ 𝜑    ⇒   ⊢ if(𝜑, 𝐴, 𝐵) = 𝐵
Theorem	iffalsed 4477	Value of the conditional operator when its first argument is false. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → ¬ 𝜒)    ⇒   ⊢ (𝜑 → if(𝜒, 𝐴, 𝐵) = 𝐵)
Theorem	ifnefalse 4478	When values are unequal, but an "if" condition checks if they are equal, then the "false" branch results. This is a simple utility to provide a slight shortening and simplification of proofs versus applying iffalse 4475 directly in this case. It happens, e.g., in oevn0 8450. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ (𝐴 ≠ 𝐵 → if(𝐴 = 𝐵, 𝐶, 𝐷) = 𝐷)
Theorem	iftrueb 4479	When the branches are not equal, an "if" condition results in the first branch if and only if its condition is true. (Contributed by SN, 16-Oct-2025.)
⊢ (𝐴 ≠ 𝐵 → (if(𝜑, 𝐴, 𝐵) = 𝐴 ↔ 𝜑))
Theorem	ifsb 4480	Distribute a function over an if-clause. (Contributed by Mario Carneiro, 14-Aug-2013.)
⊢ (if(𝜑, 𝐴, 𝐵) = 𝐴 → 𝐶 = 𝐷)    &   ⊢ (if(𝜑, 𝐴, 𝐵) = 𝐵 → 𝐶 = 𝐸)    ⇒   ⊢ 𝐶 = if(𝜑, 𝐷, 𝐸)
Theorem	dfif3 4481*	Alternate definition of the conditional operator df-if 4467. Note that 𝜑 is independent of 𝑥 i.e. a constant true or false. (Contributed by NM, 25-Aug-2013.) (Revised by Mario Carneiro, 8-Sep-2013.)
⊢ 𝐶 = {𝑥 ∣ 𝜑}    ⇒   ⊢ if(𝜑, 𝐴, 𝐵) = ((𝐴 ∩ 𝐶) ∪ (𝐵 ∩ (V ∖ 𝐶)))
Theorem	dfif4 4482*	Alternate definition of the conditional operator df-if 4467. Note that 𝜑 is independent of 𝑥 i.e. a constant true or false. (Contributed by NM, 25-Aug-2013.)
⊢ 𝐶 = {𝑥 ∣ 𝜑}    ⇒   ⊢ if(𝜑, 𝐴, 𝐵) = ((𝐴 ∪ 𝐵) ∩ ((𝐴 ∪ (V ∖ 𝐶)) ∩ (𝐵 ∪ 𝐶)))
Theorem	dfif5 4483*	Alternate definition of the conditional operator df-if 4467. Note that 𝜑 is independent of 𝑥 i.e. a constant true or false (see also ab0orv 4323). (Contributed by Gérard Lang, 18-Aug-2013.)
⊢ 𝐶 = {𝑥 ∣ 𝜑}    ⇒   ⊢ if(𝜑, 𝐴, 𝐵) = ((𝐴 ∩ 𝐵) ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))))
Theorem	ifssun 4484	A conditional class is included in the union of its two alternatives. (Contributed by BJ, 15-Aug-2024.)
⊢ if(𝜑, 𝐴, 𝐵) ⊆ (𝐴 ∪ 𝐵)
Theorem	ifeq12 4485	Equality theorem for conditional operators. (Contributed by NM, 1-Sep-2004.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → if(𝜑, 𝐴, 𝐶) = if(𝜑, 𝐵, 𝐷))
Theorem	ifeq1d 4486	Equality deduction for conditional operator. (Contributed by NM, 16-Feb-2005.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
Theorem	ifeq2d 4487	Equality deduction for conditional operator. (Contributed by NM, 16-Feb-2005.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))
Theorem	ifeq12d 4488	Equality deduction for conditional operator. (Contributed by NM, 24-Mar-2015.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐷))
Theorem	ifbi 4489	Equivalence theorem for conditional operators. (Contributed by Raph Levien, 15-Jan-2004.)
⊢ ((𝜑 ↔ 𝜓) → if(𝜑, 𝐴, 𝐵) = if(𝜓, 𝐴, 𝐵))
Theorem	ifbid 4490	Equivalence deduction for conditional operators. (Contributed by NM, 18-Apr-2005.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵))
Theorem	ifbieq1d 4491	Equivalence/equality deduction for conditional operators. (Contributed by JJ, 25-Sep-2018.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜒, 𝐵, 𝐶))
Theorem	ifbieq2i 4492	Equivalence/equality inference for conditional operators. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ 𝐴 = 𝐵    ⇒   ⊢ if(𝜑, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵)
Theorem	ifbieq2d 4493	Equivalence/equality deduction for conditional operators. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐵))
Theorem	ifbieq12i 4494	Equivalence deduction for conditional operators. (Contributed by NM, 18-Mar-2013.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ if(𝜑, 𝐴, 𝐵) = if(𝜓, 𝐶, 𝐷)
Theorem	ifbieq12d 4495	Equivalence deduction for conditional operators. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐶, 𝐷))
Theorem	nfifd 4496	Deduction form of nfif 4497. (Contributed by NM, 15-Feb-2013.) (Revised by Mario Carneiro, 13-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥if(𝜓, 𝐴, 𝐵))
Theorem	nfif 4497	Bound-variable hypothesis builder for a conditional operator. (Contributed by NM, 16-Feb-2005.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥if(𝜑, 𝐴, 𝐵)
Theorem	ifeq1da 4498	Conditional equality. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
Theorem	ifeq2da 4499	Conditional equality. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))
Theorem	ifeq12da 4500	Equivalence deduction for conditional operators. (Contributed by Wolf Lammen, 24-Jun-2021.)
⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)    &   ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜓, 𝐶, 𝐷))