Home | Metamath
Proof Explorer Theorem List (p. 45 of 466) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29289) |
Hilbert Space Explorer
(29290-30812) |
Users' Mathboxes
(30813-46532) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | undif4 4401 | Distribute union over difference. (Contributed by NM, 17-May-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ((𝐴 ∩ 𝐶) = ∅ → (𝐴 ∪ (𝐵 ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ 𝐶)) | ||
Theorem | disjssun 4402 | Subset relation for disjoint classes. (Contributed by NM, 25-Oct-2005.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ → (𝐴 ⊆ (𝐵 ∪ 𝐶) ↔ 𝐴 ⊆ 𝐶)) | ||
Theorem | vdif0 4403 | Universal class equality in terms of empty difference. (Contributed by NM, 17-Sep-2003.) |
⊢ (𝐴 = V ↔ (V ∖ 𝐴) = ∅) | ||
Theorem | difrab0eq 4404* | 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 4405* | A proper subclass has a member in one argument that's not in both. (Contributed by NM, 29-Feb-1996.) |
⊢ (𝐴 ⊊ 𝐵 → ∃𝑥(𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴)) | ||
Theorem | disjdif 4406 | A class and its relative complement are disjoint. Theorem 38 of [Suppes] p. 29. (Contributed by NM, 24-Mar-1998.) |
⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅ | ||
Theorem | disjdifr 4407 | A class and its relative complement are disjoint. (Contributed by Thierry Arnoux, 29-Nov-2023.) |
⊢ ((𝐵 ∖ 𝐴) ∩ 𝐴) = ∅ | ||
Theorem | difin0 4408 | 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 4409 | 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 4410 | Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4406). Theorem 35 of [Suppes] p. 29. (Contributed by NM, 19-May-1998.) |
⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵) | ||
Theorem | undif2 4411 | Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4406). Part of proof of Corollary 6K of [Enderton] p. 144. (Contributed by NM, 19-May-1998.) |
⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵) | ||
Theorem | undifabs 4412 | Absorption of difference by union. (Contributed by NM, 18-Aug-2013.) |
⊢ (𝐴 ∪ (𝐴 ∖ 𝐵)) = 𝐴 | ||
Theorem | inundif 4413 | 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 4414 | The difference of a class and a class disjoint from it is the original class. (Contributed by BJ, 21-Apr-2019.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ → (𝐴 ∖ 𝐵) = 𝐴) | ||
Theorem | difun2 4415 | Absorption of union by difference. Theorem 36 of [Suppes] p. 29. (Contributed by NM, 19-May-1998.) |
⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵) | ||
Theorem | undif 4416 | Union of complementary parts into whole. (Contributed by NM, 22-Mar-1998.) |
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵) | ||
Theorem | ssdifin0 4417 | 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 4418 | 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 4419 | A condition equivalent to inclusion in the union of two classes. (Contributed by NM, 26-Mar-2007.) |
⊢ (𝐴 ⊆ (𝐵 ∪ 𝐶) ↔ (𝐴 ∖ 𝐵) ⊆ 𝐶) | ||
Theorem | difcom 4420 | Swap the arguments of a class difference. (Contributed by NM, 29-Mar-2007.) |
⊢ ((𝐴 ∖ 𝐵) ⊆ 𝐶 ↔ (𝐴 ∖ 𝐶) ⊆ 𝐵) | ||
Theorem | pssdifcom1 4421 | Two ways to express overlapping subsets. (Contributed by Stefan O'Rear, 31-Oct-2014.) |
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → ((𝐶 ∖ 𝐴) ⊊ 𝐵 ↔ (𝐶 ∖ 𝐵) ⊊ 𝐴)) | ||
Theorem | pssdifcom2 4422 | Two ways to express non-covering pairs of subsets. (Contributed by Stefan O'Rear, 31-Oct-2014.) |
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → (𝐵 ⊊ (𝐶 ∖ 𝐴) ↔ 𝐴 ⊊ (𝐶 ∖ 𝐵))) | ||
Theorem | difdifdir 4423 | Distributive law for class difference. Exercise 4.8 of [Stoll] p. 16. (Contributed by NM, 18-Aug-2004.) |
⊢ ((𝐴 ∖ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∖ (𝐵 ∖ 𝐶)) | ||
Theorem | uneqdifeq 4424 | 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 4425* | Equality theorem for restricted universal quantifier. (Contributed by Thierry Arnoux, 6-Jul-2019.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → ∀𝑥 ∈ (𝐵 ∖ 𝐴)𝜓) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | r19.2z 4426* | Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1981). The restricted version is valid only when the domain of quantification is not empty. (Contributed by NM, 15-Nov-2003.) |
⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑥 ∈ 𝐴 𝜑) | ||
Theorem | r19.2zb 4427* | A response to the notion that the condition 𝐴 ≠ ∅ can be removed in r19.2z 4426. Interestingly enough, 𝜑 does not figure in the left-hand side. (Contributed by Jeff Hankins, 24-Aug-2009.) |
⊢ (𝐴 ≠ ∅ ↔ (∀𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜑)) | ||
Theorem | r19.3rz 4428* | Restricted quantification of wff not containing quantified variable. (Contributed by FL, 3-Jan-2008.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (𝐴 ≠ ∅ → (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑)) | ||
Theorem | r19.28z 4429* | 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 4430* | Restricted quantification of wff not containing quantified variable. (Contributed by NM, 10-Mar-1997.) |
⊢ (𝐴 ≠ ∅ → (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑)) | ||
Theorem | r19.9rzv 4431* | Restricted quantification of wff not containing quantified variable. (Contributed by NM, 27-May-1998.) |
⊢ (𝐴 ≠ ∅ → (𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜑)) | ||
Theorem | r19.28zv 4432* | 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 4433* | 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 4434* | Restricted version of Theorem 19.45 of [Margaris] p. 90. (Contributed by NM, 27-May-1998.) |
⊢ (𝐴 ≠ ∅ → (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓))) | ||
Theorem | r19.44zv 4435* | Restricted version of Theorem 19.44 of [Margaris] p. 90. (Contributed by NM, 27-May-1998.) |
⊢ (𝐴 ≠ ∅ → (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ 𝜓))) | ||
Theorem | r19.27z 4436* | 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 4437* | 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 4438* | 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 4439* | Idempotent law for restricted quantifier. Weak version of ralidm 4443, which does not require ax-10 2138, ax-12 2172, but requires ax-8 2109. (Contributed by Gino Giotto, 30-Sep-2024.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rzal 4440* | Vacuous quantification is always true. (Contributed by NM, 11-Mar-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) Avoid df-clel 2817, ax-8 2109. (Revised by Gino Giotto, 2-Sep-2024.) |
⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rzalALT 4441* | Alternate proof of rzal 4440. Shorter, but requiring df-clel 2817, ax-8 2109. (Contributed by NM, 11-Mar-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rexn0 4442* | Restricted existential quantification implies its restriction is nonempty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) Avoid df-clel 2817, ax-8 2109. (Revised by Gino Giotto, 2-Sep-2024.) |
⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝐴 ≠ ∅) | ||
Theorem | ralidm 4443 | Idempotent law for restricted quantifier. (Contributed by NM, 28-Mar-1997.) Reduce axiom usage. (Revised by Gino Giotto, 2-Sep-2024.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | ral0 4444 | Vacuous universal quantification is always true. (Contributed by NM, 20-Oct-2005.) Avoid df-clel 2817, ax-8 2109. (Revised by Gino Giotto, 2-Sep-2024.) |
⊢ ∀𝑥 ∈ ∅ 𝜑 | ||
Theorem | ralf0 4445* | 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 2817, ax-8 2109. (Revised by Gino Giotto, 2-Sep-2024.) |
⊢ ¬ 𝜑 ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ 𝐴 = ∅) | ||
Theorem | rexn0OLD 4446* | Obsolete version of rexn0 4442 as of 2-Sep-2024. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝐴 ≠ ∅) | ||
Theorem | ralidmOLD 4447* | Obsolete version of ralidm 4443 as of 2-Sep-2024. (Contributed by NM, 28-Mar-1997.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | ral0OLD 4448 | Obsolete version of ral0 4444 as of 2-Sep-2024. (Contributed by NM, 20-Oct-2005.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ∀𝑥 ∈ ∅ 𝜑 | ||
Theorem | ralf0OLD 4449* | Obsolete version of ralf0 4445 as of 2-Sep-2024. (Contributed by NM, 26-Nov-2005.) (Proof shortened by JJ, 14-Jul-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ¬ 𝜑 ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ 𝐴 = ∅) | ||
Theorem | ralnralall 4450* | A contradiction concerning restricted generalization for a nonempty set implies anything. (Contributed by Alexander van der Vekens, 4-Sep-2018.) |
⊢ (𝐴 ≠ ∅ → ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 ¬ 𝜑) → 𝜓)) | ||
Theorem | falseral0 4451* | A false statement can only be true for elements of an empty set. (Contributed by AV, 30-Oct-2020.) |
⊢ ((∀𝑥 ¬ 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜑) → 𝐴 = ∅) | ||
Theorem | raaan 4452* | Rearrange restricted quantifiers. (Contributed by NM, 26-Oct-2010.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐴 𝜓)) | ||
Theorem | raaanv 4453* | Rearrange restricted quantifiers. (Contributed by NM, 11-Mar-1997.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐴 𝜓)) | ||
Theorem | sbss 4454* | 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 4455 | 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 4456* | Rearrange restricted quantifiers with two different restricting classes, analogous to raaan 4452. 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 4457* | Lemma for 2reu4 4458. (Contributed by Alexander van der Vekens, 1-Jul-2017.) |
⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))))) | ||
Theorem | 2reu4 4458* | Definition of double restricted existential uniqueness ("exactly one 𝑥 and exactly one 𝑦"), analogous to 2eu4 2657. (Contributed by Alexander van der Vekens, 1-Jul-2017.) |
⊢ ((∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))) | ||
Theorem | csbdif 4459 | Distribution of class substitution over difference of two classes. (Contributed by ML, 14-Jul-2020.) |
⊢ ⦋𝐴 / 𝑥⦌(𝐵 ∖ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∖ ⦋𝐴 / 𝑥⦌𝐶) | ||
This subsection introduces the conditional operator for classes, denoted by if(𝜑, 𝐴, 𝐵) (see df-if 4461). It is the analogue for classes of the conditional operator for propositions, denoted by if-(𝜑, 𝜓, 𝜒) (see df-ifp 1061). | ||
Syntax | cif 4460 | Extend class notation to include the conditional operator for classes. |
class if(𝜑, 𝐴, 𝐵) | ||
Definition | df-if 4461* |
Definition of the conditional operator for classes. The expression
if(𝜑,
𝐴, 𝐵) is read "if 𝜑 then
𝐴
else 𝐵". See
iftrue 4466 and iffalse 4469 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 4518. (Contributed by NM, 15-May-1999.) |
⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))} | ||
Theorem | dfif2 4462* | An alternate definition of the conditional operator df-if 4461 with one fewer connectives (but probably less intuitive to understand). (Contributed by NM, 30-Jan-2006.) |
⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜑))} | ||
Theorem | dfif6 4463* | An alternate definition of the conditional operator df-if 4461 as a simple class abstraction. (Contributed by Mario Carneiro, 8-Sep-2013.) |
⊢ if(𝜑, 𝐴, 𝐵) = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐵 ∣ ¬ 𝜑}) | ||
Theorem | ifeq1 4464 | Equality theorem for conditional operator. (Contributed by NM, 1-Sep-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ (𝐴 = 𝐵 → if(𝜑, 𝐴, 𝐶) = if(𝜑, 𝐵, 𝐶)) | ||
Theorem | ifeq2 4465 | Equality theorem for conditional operator. (Contributed by NM, 1-Sep-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ (𝐴 = 𝐵 → if(𝜑, 𝐶, 𝐴) = if(𝜑, 𝐶, 𝐵)) | ||
Theorem | iftrue 4466 | 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 4467 | Inference associated with iftrue 4466. (Contributed by BJ, 7-Oct-2018.) |
⊢ 𝜑 ⇒ ⊢ if(𝜑, 𝐴, 𝐵) = 𝐴 | ||
Theorem | iftrued 4468 | Value of the conditional operator when its first argument is true. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝜒) ⇒ ⊢ (𝜑 → if(𝜒, 𝐴, 𝐵) = 𝐴) | ||
Theorem | iffalse 4469 | Value of the conditional operator when its first argument is false. (Contributed by NM, 14-Aug-1999.) |
⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵) | ||
Theorem | iffalsei 4470 | Inference associated with iffalse 4469. (Contributed by BJ, 7-Oct-2018.) |
⊢ ¬ 𝜑 ⇒ ⊢ if(𝜑, 𝐴, 𝐵) = 𝐵 | ||
Theorem | iffalsed 4471 | Value of the conditional operator when its first argument is false. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → ¬ 𝜒) ⇒ ⊢ (𝜑 → if(𝜒, 𝐴, 𝐵) = 𝐵) | ||
Theorem | ifnefalse 4472 | 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 4469 directly in this case. It happens, e.g., in oevn0 8354. (Contributed by David A. Wheeler, 15-May-2015.) |
⊢ (𝐴 ≠ 𝐵 → if(𝐴 = 𝐵, 𝐶, 𝐷) = 𝐷) | ||
Theorem | ifsb 4473 | Distribute a function over an if-clause. (Contributed by Mario Carneiro, 14-Aug-2013.) |
⊢ (if(𝜑, 𝐴, 𝐵) = 𝐴 → 𝐶 = 𝐷) & ⊢ (if(𝜑, 𝐴, 𝐵) = 𝐵 → 𝐶 = 𝐸) ⇒ ⊢ 𝐶 = if(𝜑, 𝐷, 𝐸) | ||
Theorem | dfif3 4474* | Alternate definition of the conditional operator df-if 4461. 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 4475* | Alternate definition of the conditional operator df-if 4461. Note that 𝜑 is independent of 𝑥 i.e. a constant true or false. (Contributed by NM, 25-Aug-2013.) |
⊢ 𝐶 = {𝑥 ∣ 𝜑} ⇒ ⊢ if(𝜑, 𝐴, 𝐵) = ((𝐴 ∪ 𝐵) ∩ ((𝐴 ∪ (V ∖ 𝐶)) ∩ (𝐵 ∪ 𝐶))) | ||
Theorem | dfif5 4476* | Alternate definition of the conditional operator df-if 4461. Note that 𝜑 is independent of 𝑥 i.e. a constant true or false (see also ab0orv 4313). (Contributed by Gérard Lang, 18-Aug-2013.) |
⊢ 𝐶 = {𝑥 ∣ 𝜑} ⇒ ⊢ if(𝜑, 𝐴, 𝐵) = ((𝐴 ∩ 𝐵) ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) | ||
Theorem | ifssun 4477 | A conditional class is included in the union of its two alternatives. (Contributed by BJ, 15-Aug-2024.) |
⊢ if(𝜑, 𝐴, 𝐵) ⊆ (𝐴 ∪ 𝐵) | ||
Theorem | ifeq12 4478 | Equality theorem for conditional operators. (Contributed by NM, 1-Sep-2004.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → if(𝜑, 𝐴, 𝐶) = if(𝜑, 𝐵, 𝐷)) | ||
Theorem | ifeq1d 4479 | Equality deduction for conditional operator. (Contributed by NM, 16-Feb-2005.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶)) | ||
Theorem | ifeq2d 4480 | Equality deduction for conditional operator. (Contributed by NM, 16-Feb-2005.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵)) | ||
Theorem | ifeq12d 4481 | Equality deduction for conditional operator. (Contributed by NM, 24-Mar-2015.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐷)) | ||
Theorem | ifbi 4482 | Equivalence theorem for conditional operators. (Contributed by Raph Levien, 15-Jan-2004.) |
⊢ ((𝜑 ↔ 𝜓) → if(𝜑, 𝐴, 𝐵) = if(𝜓, 𝐴, 𝐵)) | ||
Theorem | ifbid 4483 | Equivalence deduction for conditional operators. (Contributed by NM, 18-Apr-2005.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵)) | ||
Theorem | ifbieq1d 4484 | Equivalence/equality deduction for conditional operators. (Contributed by JJ, 25-Sep-2018.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜒, 𝐵, 𝐶)) | ||
Theorem | ifbieq2i 4485 | Equivalence/equality inference for conditional operators. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ 𝐴 = 𝐵 ⇒ ⊢ if(𝜑, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵) | ||
Theorem | ifbieq2d 4486 | Equivalence/equality deduction for conditional operators. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐵)) | ||
Theorem | ifbieq12i 4487 | Equivalence deduction for conditional operators. (Contributed by NM, 18-Mar-2013.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ 𝐴 = 𝐶 & ⊢ 𝐵 = 𝐷 ⇒ ⊢ if(𝜑, 𝐴, 𝐵) = if(𝜓, 𝐶, 𝐷) | ||
Theorem | ifbieq12d 4488 | Equivalence deduction for conditional operators. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐶, 𝐷)) | ||
Theorem | nfifd 4489 | Deduction form of nfif 4490. (Contributed by NM, 15-Feb-2013.) (Revised by Mario Carneiro, 13-Oct-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥if(𝜓, 𝐴, 𝐵)) | ||
Theorem | nfif 4490 | 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 4491 | Conditional equality. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶)) | ||
Theorem | ifeq2da 4492 | Conditional equality. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵)) | ||
Theorem | ifeq12da 4493 | Equivalence deduction for conditional operators. (Contributed by Wolf Lammen, 24-Jun-2021.) |
⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶) & ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜓, 𝐶, 𝐷)) | ||
Theorem | ifbieq12d2 4494 | Equivalence deduction for conditional operators. (Contributed by Thierry Arnoux, 14-Feb-2017.) (Proof shortened by Wolf Lammen, 24-Jun-2021.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶) & ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐶, 𝐷)) | ||
Theorem | ifclda 4495 | Conditional closure. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ 𝐶) & ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶) | ||
Theorem | ifeqda 4496 | Separation of the values of the conditional operator. (Contributed by Alexander van der Vekens, 13-Apr-2018.) |
⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶) & ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = 𝐶) | ||
Theorem | elimif 4497 | Elimination of a conditional operator contained in a wff 𝜓. (Contributed by NM, 15-Feb-2005.) (Proof shortened by NM, 25-Apr-2019.) |
⊢ (if(𝜑, 𝐴, 𝐵) = 𝐴 → (𝜓 ↔ 𝜒)) & ⊢ (if(𝜑, 𝐴, 𝐵) = 𝐵 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝜓 ↔ ((𝜑 ∧ 𝜒) ∨ (¬ 𝜑 ∧ 𝜃))) | ||
Theorem | ifbothda 4498 | A wff 𝜃 containing a conditional operator is true when both of its cases are true. (Contributed by NM, 15-Feb-2015.) |
⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜃)) & ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜃)) & ⊢ ((𝜂 ∧ 𝜑) → 𝜓) & ⊢ ((𝜂 ∧ ¬ 𝜑) → 𝜒) ⇒ ⊢ (𝜂 → 𝜃) | ||
Theorem | ifboth 4499 | A wff 𝜃 containing a conditional operator is true when both of its cases are true. (Contributed by NM, 3-Sep-2006.) (Revised by Mario Carneiro, 15-Feb-2015.) |
⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜃)) & ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜃)) ⇒ ⊢ ((𝜓 ∧ 𝜒) → 𝜃) | ||
Theorem | ifid 4500 | Identical true and false arguments in the conditional operator. (Contributed by NM, 18-Apr-2005.) |
⊢ if(𝜑, 𝐴, 𝐴) = 𝐴 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |