Home | Intuitionistic Logic Explorer Theorem List (p. 35 of 135) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rabxmdc 3401* | Law of excluded middle given decidability, in terms of restricted class abstractions. (Contributed by Jim Kingdon, 2-Aug-2018.) |
⊢ (∀𝑥DECID 𝜑 → 𝐴 = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑})) | ||
Theorem | rabnc 3402* | Law of noncontradiction, in terms of restricted class abstractions. (Contributed by Jeff Madsen, 20-Jun-2011.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}) = ∅ | ||
Theorem | un0 3403 | The union of a class with the empty set is itself. Theorem 24 of [Suppes] p. 27. (Contributed by NM, 5-Aug-1993.) |
⊢ (𝐴 ∪ ∅) = 𝐴 | ||
Theorem | in0 3404 | The intersection of a class with the empty set is the empty set. Theorem 16 of [Suppes] p. 26. (Contributed by NM, 5-Aug-1993.) |
⊢ (𝐴 ∩ ∅) = ∅ | ||
Theorem | 0in 3405 | The intersection of the empty set with a class is the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (∅ ∩ 𝐴) = ∅ | ||
Theorem | inv1 3406 | The intersection of a class with the universal class is itself. Exercise 4.10(k) of [Mendelson] p. 231. (Contributed by NM, 17-May-1998.) |
⊢ (𝐴 ∩ V) = 𝐴 | ||
Theorem | unv 3407 | The union of a class with the universal class is the universal class. Exercise 4.10(l) of [Mendelson] p. 231. (Contributed by NM, 17-May-1998.) |
⊢ (𝐴 ∪ V) = V | ||
Theorem | 0ss 3408 | The null set is a subset of any class. Part of Exercise 1 of [TakeutiZaring] p. 22. (Contributed by NM, 5-Aug-1993.) |
⊢ ∅ ⊆ 𝐴 | ||
Theorem | ss0b 3409 | Any subset of the empty set is empty. Theorem 5 of [Suppes] p. 23 and its converse. (Contributed by NM, 17-Sep-2003.) |
⊢ (𝐴 ⊆ ∅ ↔ 𝐴 = ∅) | ||
Theorem | ss0 3410 | Any subset of the empty set is empty. Theorem 5 of [Suppes] p. 23. (Contributed by NM, 13-Aug-1994.) |
⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅) | ||
Theorem | sseq0 3411 | A subclass of an empty class is empty. (Contributed by NM, 7-Mar-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅) | ||
Theorem | ssn0 3412 | A class with a nonempty subclass is nonempty. (Contributed by NM, 17-Feb-2007.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → 𝐵 ≠ ∅) | ||
Theorem | abf 3413 | A class builder with a false argument is empty. (Contributed by NM, 20-Jan-2012.) |
⊢ ¬ 𝜑 ⇒ ⊢ {𝑥 ∣ 𝜑} = ∅ | ||
Theorem | eq0rdv 3414* | Deduction for equality to the empty set. (Contributed by NM, 11-Jul-2014.) |
⊢ (𝜑 → ¬ 𝑥 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 = ∅) | ||
Theorem | csbprc 3415 | The proper substitution of a proper class for a set into a class results in the empty set. (Contributed by NM, 17-Aug-2018.) |
⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 = ∅) | ||
Theorem | un00 3416 | Two classes are empty iff their union is empty. (Contributed by NM, 11-Aug-2004.) |
⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) ↔ (𝐴 ∪ 𝐵) = ∅) | ||
Theorem | vss 3417 | 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 | disj 3418* | Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 17-Feb-2004.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵) | ||
Theorem | disjr 3419* | Two ways of saying that two classes are disjoint. (Contributed by Jeff Madsen, 19-Jun-2011.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥 ∈ 𝐵 ¬ 𝑥 ∈ 𝐴) | ||
Theorem | disj1 3420* | Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 19-Aug-1993.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵)) | ||
Theorem | reldisj 3421 | 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 3422 | Two ways of saying that two classes are disjoint. (Contributed by NM, 19-May-1998.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐴 = (𝐴 ∖ 𝐵)) | ||
Theorem | disjne 3423 | Members of disjoint sets are not equal. (Contributed by NM, 28-Mar-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → 𝐶 ≠ 𝐷) | ||
Theorem | disjel 3424 | A set can't belong to both members of disjoint classes. (Contributed by NM, 28-Feb-2015.) |
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝐶 ∈ 𝐴) → ¬ 𝐶 ∈ 𝐵) | ||
Theorem | disj2 3425 | Two ways of saying that two classes are disjoint. (Contributed by NM, 17-May-1998.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐴 ⊆ (V ∖ 𝐵)) | ||
Theorem | ssdisj 3426 | Intersection with a subclass of a disjoint class. (Contributed by FL, 24-Jan-2007.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ (𝐵 ∩ 𝐶) = ∅) → (𝐴 ∩ 𝐶) = ∅) | ||
Theorem | undisj1 3427 | The union of disjoint classes is disjoint. (Contributed by NM, 26-Sep-2004.) |
⊢ (((𝐴 ∩ 𝐶) = ∅ ∧ (𝐵 ∩ 𝐶) = ∅) ↔ ((𝐴 ∪ 𝐵) ∩ 𝐶) = ∅) | ||
Theorem | undisj2 3428 | The union of disjoint classes is disjoint. (Contributed by NM, 13-Sep-2004.) |
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ (𝐴 ∩ 𝐶) = ∅) ↔ (𝐴 ∩ (𝐵 ∪ 𝐶)) = ∅) | ||
Theorem | ssindif0im 3429 | Subclass implies empty intersection with difference from the universal class. (Contributed by NM, 17-Sep-2003.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ (V ∖ 𝐵)) = ∅) | ||
Theorem | inelcm 3430 | The intersection of classes with a common member is nonempty. (Contributed by NM, 7-Apr-1994.) |
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → (𝐵 ∩ 𝐶) ≠ ∅) | ||
Theorem | minel 3431 | A minimum element of a class has no elements in common with the class. (Contributed by NM, 22-Jun-1994.) |
⊢ ((𝐴 ∈ 𝐵 ∧ (𝐶 ∩ 𝐵) = ∅) → ¬ 𝐴 ∈ 𝐶) | ||
Theorem | undif4 3432 | Distribute union over difference. (Contributed by NM, 17-May-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ((𝐴 ∩ 𝐶) = ∅ → (𝐴 ∪ (𝐵 ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ 𝐶)) | ||
Theorem | disjssun 3433 | Subset relation for disjoint classes. (Contributed by NM, 25-Oct-2005.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ → (𝐴 ⊆ (𝐵 ∪ 𝐶) ↔ 𝐴 ⊆ 𝐶)) | ||
Theorem | ssdif0im 3434 | Subclass implies empty difference. One direction of Exercise 7 of [TakeutiZaring] p. 22. In classical logic this would be an equivalence. (Contributed by Jim Kingdon, 2-Aug-2018.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐵) = ∅) | ||
Theorem | vdif0im 3435 | Universal class equality in terms of empty difference. (Contributed by Jim Kingdon, 3-Aug-2018.) |
⊢ (𝐴 = V → (V ∖ 𝐴) = ∅) | ||
Theorem | difrab0eqim 3436* | 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 Jim Kingdon, 3-Aug-2018.) |
⊢ (𝑉 = {𝑥 ∈ 𝑉 ∣ 𝜑} → (𝑉 ∖ {𝑥 ∈ 𝑉 ∣ 𝜑}) = ∅) | ||
Theorem | inssdif0im 3437 | Intersection, subclass, and difference relationship. In classical logic the converse would also hold. (Contributed by Jim Kingdon, 3-Aug-2018.) |
⊢ ((𝐴 ∩ 𝐵) ⊆ 𝐶 → (𝐴 ∩ (𝐵 ∖ 𝐶)) = ∅) | ||
Theorem | difid 3438 | The difference between a class and itself is the empty set. Proposition 5.15 of [TakeutiZaring] p. 20. Also Theorem 32 of [Suppes] p. 28. (Contributed by NM, 22-Apr-2004.) |
⊢ (𝐴 ∖ 𝐴) = ∅ | ||
Theorem | difidALT 3439 | The difference between a class and itself is the empty set. Proposition 5.15 of [TakeutiZaring] p. 20. Also Theorem 32 of [Suppes] p. 28. Alternate proof of difid 3438. (Contributed by David Abernethy, 17-Jun-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∖ 𝐴) = ∅ | ||
Theorem | dif0 3440 | The difference between a class and the empty set. Part of Exercise 4.4 of [Stoll] p. 16. (Contributed by NM, 17-Aug-2004.) |
⊢ (𝐴 ∖ ∅) = 𝐴 | ||
Theorem | 0dif 3441 | 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 | disjdif 3442 | A class and its relative complement are disjoint. Theorem 38 of [Suppes] p. 29. (Contributed by NM, 24-Mar-1998.) |
⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅ | ||
Theorem | difin0 3443 | 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 | undif1ss 3444 | Absorption of difference by union. In classical logic, as Theorem 35 of [Suppes] p. 29, this would be equality rather than subset. (Contributed by Jim Kingdon, 4-Aug-2018.) |
⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) ⊆ (𝐴 ∪ 𝐵) | ||
Theorem | undif2ss 3445 | Absorption of difference by union. In classical logic, as in Part of proof of Corollary 6K of [Enderton] p. 144, this would be equality rather than subset. (Contributed by Jim Kingdon, 4-Aug-2018.) |
⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) ⊆ (𝐴 ∪ 𝐵) | ||
Theorem | undifabs 3446 | Absorption of difference by union. (Contributed by NM, 18-Aug-2013.) |
⊢ (𝐴 ∪ (𝐴 ∖ 𝐵)) = 𝐴 | ||
Theorem | inundifss 3447 | The intersection and class difference of a class with another class are contained in the original class. In classical logic we'd be able to make a stronger statement: that everything in the original class is in the intersection or the difference (that is, this theorem would be equality rather than subset). (Contributed by Jim Kingdon, 4-Aug-2018.) |
⊢ ((𝐴 ∩ 𝐵) ∪ (𝐴 ∖ 𝐵)) ⊆ 𝐴 | ||
Theorem | disjdif2 3448 | The difference of a class and a class disjoint from it is the original class. (Contributed by BJ, 21-Apr-2019.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ → (𝐴 ∖ 𝐵) = 𝐴) | ||
Theorem | difun2 3449 | Absorption of union by difference. Theorem 36 of [Suppes] p. 29. (Contributed by NM, 19-May-1998.) |
⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵) | ||
Theorem | undifss 3450 | Union of complementary parts into whole. (Contributed by Jim Kingdon, 4-Aug-2018.) |
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ (𝐵 ∖ 𝐴)) ⊆ 𝐵) | ||
Theorem | ssdifin0 3451 | 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 3452 | A class is a subclass of itself subtracted from another iff it is the empty set. (Contributed by Steve Rodriguez, 20-Nov-2015.) |
⊢ (𝐴 ⊆ (𝐵 ∖ 𝐴) ↔ 𝐴 = ∅) | ||
Theorem | ssundifim 3453 | A consequence of inclusion in the union of two classes. In classical logic this would be a biconditional. (Contributed by Jim Kingdon, 4-Aug-2018.) |
⊢ (𝐴 ⊆ (𝐵 ∪ 𝐶) → (𝐴 ∖ 𝐵) ⊆ 𝐶) | ||
Theorem | difdifdirss 3454 | Distributive law for class difference. In classical logic, as in Exercise 4.8 of [Stoll] p. 16, this would be equality rather than subset. (Contributed by Jim Kingdon, 4-Aug-2018.) |
⊢ ((𝐴 ∖ 𝐵) ∖ 𝐶) ⊆ ((𝐴 ∖ 𝐶) ∖ (𝐵 ∖ 𝐶)) | ||
Theorem | uneqdifeqim 3455 | Two ways that 𝐴 and 𝐵 can "partition" 𝐶 (when 𝐴 and 𝐵 don't overlap and 𝐴 is a part of 𝐶). In classical logic, the second implication would be a biconditional. (Contributed by Jim Kingdon, 4-Aug-2018.) |
⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐴 ∪ 𝐵) = 𝐶 → (𝐶 ∖ 𝐴) = 𝐵)) | ||
Theorem | r19.2m 3456* | Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1618). The restricted version is valid only when the domain of quantification is inhabited. (Contributed by Jim Kingdon, 5-Aug-2018.) (Revised by Jim Kingdon, 7-Apr-2023.) |
⊢ ((∃𝑦 𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑥 ∈ 𝐴 𝜑) | ||
Theorem | r19.2mOLD 3457* | Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1618). The restricted version is valid only when the domain of quantification is inhabited. (Contributed by Jim Kingdon, 5-Aug-2018.) Obsolete version of r19.2m 3456 as of 7-Apr-2023. (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((∃𝑥 𝑥 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑥 ∈ 𝐴 𝜑) | ||
Theorem | r19.3rm 3458* | Restricted quantification of wff not containing quantified variable. (Contributed by Jim Kingdon, 19-Dec-2018.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∃𝑦 𝑦 ∈ 𝐴 → (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑)) | ||
Theorem | r19.28m 3459* | Restricted quantifier version of Theorem 19.28 of [Margaris] p. 90. It is valid only when the domain of quantification is inhabited. (Contributed by Jim Kingdon, 5-Aug-2018.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∃𝑥 𝑥 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))) | ||
Theorem | r19.3rmv 3460* | Restricted quantification of wff not containing quantified variable. (Contributed by Jim Kingdon, 6-Aug-2018.) |
⊢ (∃𝑦 𝑦 ∈ 𝐴 → (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑)) | ||
Theorem | r19.9rmv 3461* | Restricted quantification of wff not containing quantified variable. (Contributed by Jim Kingdon, 5-Aug-2018.) |
⊢ (∃𝑦 𝑦 ∈ 𝐴 → (𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜑)) | ||
Theorem | r19.28mv 3462* | Restricted quantifier version of Theorem 19.28 of [Margaris] p. 90. It is valid only when the domain of quantification is inhabited. (Contributed by Jim Kingdon, 6-Aug-2018.) |
⊢ (∃𝑥 𝑥 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))) | ||
Theorem | r19.45mv 3463* | Restricted version of Theorem 19.45 of [Margaris] p. 90. (Contributed by NM, 27-May-1998.) |
⊢ (∃𝑥 𝑥 ∈ 𝐴 → (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓))) | ||
Theorem | r19.44mv 3464* | Restricted version of Theorem 19.44 of [Margaris] p. 90. (Contributed by NM, 27-May-1998.) |
⊢ (∃𝑦 𝑦 ∈ 𝐴 → (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ 𝜓))) | ||
Theorem | r19.27m 3465* | Restricted quantifier version of Theorem 19.27 of [Margaris] p. 90. It is valid only when the domain of quantification is inhabited. (Contributed by Jim Kingdon, 5-Aug-2018.) |
⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∃𝑥 𝑥 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))) | ||
Theorem | r19.27mv 3466* | Restricted quantifier version of Theorem 19.27 of [Margaris] p. 90. It is valid only when the domain of quantification is inhabited. (Contributed by Jim Kingdon, 5-Aug-2018.) |
⊢ (∃𝑥 𝑥 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))) | ||
Theorem | rzal 3467* | Vacuous quantification is always true. (Contributed by NM, 11-Mar-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rexn0 3468* | Restricted existential quantification implies its restriction is nonempty (it is also inhabited as shown in rexm 3469). (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) |
⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝐴 ≠ ∅) | ||
Theorem | rexm 3469* | Restricted existential quantification implies its restriction is inhabited. (Contributed by Jim Kingdon, 16-Oct-2018.) |
⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 𝑥 ∈ 𝐴) | ||
Theorem | ralidm 3470* | Idempotent law for restricted quantifier. (Contributed by NM, 28-Mar-1997.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | ral0 3471 | Vacuous universal quantification is always true. (Contributed by NM, 20-Oct-2005.) |
⊢ ∀𝑥 ∈ ∅ 𝜑 | ||
Theorem | rgenm 3472* | Generalization rule that eliminates an inhabited class requirement. (Contributed by Jim Kingdon, 5-Aug-2018.) |
⊢ ((∃𝑥 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝜑) ⇒ ⊢ ∀𝑥 ∈ 𝐴 𝜑 | ||
Theorem | ralf0 3473* | The quantification of a falsehood is vacuous when true. (Contributed by NM, 26-Nov-2005.) |
⊢ ¬ 𝜑 ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ 𝐴 = ∅) | ||
Theorem | ralm 3474 | Inhabited classes and restricted quantification. (Contributed by Jim Kingdon, 6-Aug-2018.) |
⊢ ((∃𝑥 𝑥 ∈ 𝐴 → ∀𝑥 ∈ 𝐴 𝜑) ↔ ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | raaanlem 3475* | Special case of raaan 3476 where 𝐴 is inhabited. (Contributed by Jim Kingdon, 6-Aug-2018.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∃𝑥 𝑥 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐴 𝜓))) | ||
Theorem | raaan 3476* | Rearrange restricted quantifiers. (Contributed by NM, 26-Oct-2010.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐴 𝜓)) | ||
Theorem | raaanv 3477* | Rearrange restricted quantifiers. (Contributed by NM, 11-Mar-1997.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐴 𝜓)) | ||
Theorem | sbss 3478* | 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 3479 | 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 | dcun 3480 | The union of two decidable classes is decidable. (Contributed by Jim Kingdon, 5-Oct-2022.) |
⊢ (𝜑 → DECID 𝑘 ∈ 𝐴) & ⊢ (𝜑 → DECID 𝑘 ∈ 𝐵) ⇒ ⊢ (𝜑 → DECID 𝑘 ∈ (𝐴 ∪ 𝐵)) | ||
Syntax | cif 3481 | Extend class notation to include the conditional operator. See df-if 3482 for a description. (In older databases this was denoted "ded".) |
class if(𝜑, 𝐴, 𝐵) | ||
Definition | df-if 3482* |
Define the conditional operator. Read if(𝜑, 𝐴, 𝐵) as "if
𝜑 then 𝐴 else 𝐵."
See iftrue 3486 and iffalse 3489 for its
values. In 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."
In the absence of excluded middle, this will tend to be useful where 𝜑 is decidable (in the sense of df-dc 821). (Contributed by NM, 15-May-1999.) |
⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))} | ||
Theorem | dfif6 3483* | An alternate definition of the conditional operator df-if 3482 as a simple class abstraction. (Contributed by Mario Carneiro, 8-Sep-2013.) |
⊢ if(𝜑, 𝐴, 𝐵) = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐵 ∣ ¬ 𝜑}) | ||
Theorem | ifeq1 3484 | Equality theorem for conditional operator. (Contributed by NM, 1-Sep-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ (𝐴 = 𝐵 → if(𝜑, 𝐴, 𝐶) = if(𝜑, 𝐵, 𝐶)) | ||
Theorem | ifeq2 3485 | Equality theorem for conditional operator. (Contributed by NM, 1-Sep-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ (𝐴 = 𝐵 → if(𝜑, 𝐶, 𝐴) = if(𝜑, 𝐶, 𝐵)) | ||
Theorem | iftrue 3486 | 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 3487 | Inference associated with iftrue 3486. (Contributed by BJ, 7-Oct-2018.) |
⊢ 𝜑 ⇒ ⊢ if(𝜑, 𝐴, 𝐵) = 𝐴 | ||
Theorem | iftrued 3488 | Value of the conditional operator when its first argument is true. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝜒) ⇒ ⊢ (𝜑 → if(𝜒, 𝐴, 𝐵) = 𝐴) | ||
Theorem | iffalse 3489 | Value of the conditional operator when its first argument is false. (Contributed by NM, 14-Aug-1999.) |
⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵) | ||
Theorem | iffalsei 3490 | Inference associated with iffalse 3489. (Contributed by BJ, 7-Oct-2018.) |
⊢ ¬ 𝜑 ⇒ ⊢ if(𝜑, 𝐴, 𝐵) = 𝐵 | ||
Theorem | iffalsed 3491 | Value of the conditional operator when its first argument is false. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → ¬ 𝜒) ⇒ ⊢ (𝜑 → if(𝜒, 𝐴, 𝐵) = 𝐵) | ||
Theorem | ifnefalse 3492 | 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 3489 directly in this case. (Contributed by David A. Wheeler, 15-May-2015.) |
⊢ (𝐴 ≠ 𝐵 → if(𝐴 = 𝐵, 𝐶, 𝐷) = 𝐷) | ||
Theorem | ifsbdc 3493 | Distribute a function over an if-clause. (Contributed by Jim Kingdon, 1-Jan-2022.) |
⊢ (if(𝜑, 𝐴, 𝐵) = 𝐴 → 𝐶 = 𝐷) & ⊢ (if(𝜑, 𝐴, 𝐵) = 𝐵 → 𝐶 = 𝐸) ⇒ ⊢ (DECID 𝜑 → 𝐶 = if(𝜑, 𝐷, 𝐸)) | ||
Theorem | dfif3 3494* | Alternate definition of the conditional operator df-if 3482. 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 | ifeq12 3495 | Equality theorem for conditional operators. (Contributed by NM, 1-Sep-2004.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → if(𝜑, 𝐴, 𝐶) = if(𝜑, 𝐵, 𝐷)) | ||
Theorem | ifeq1d 3496 | Equality deduction for conditional operator. (Contributed by NM, 16-Feb-2005.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶)) | ||
Theorem | ifeq2d 3497 | Equality deduction for conditional operator. (Contributed by NM, 16-Feb-2005.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵)) | ||
Theorem | ifeq12d 3498 | Equality deduction for conditional operator. (Contributed by NM, 24-Mar-2015.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐷)) | ||
Theorem | ifbi 3499 | Equivalence theorem for conditional operators. (Contributed by Raph Levien, 15-Jan-2004.) |
⊢ ((𝜑 ↔ 𝜓) → if(𝜑, 𝐴, 𝐵) = if(𝜓, 𝐴, 𝐵)) | ||
Theorem | ifbid 3500 | Equivalence deduction for conditional operators. (Contributed by NM, 18-Apr-2005.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |