 Home New Foundations ExplorerTheorem List (p. 37 of 64) < Previous  Next > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  NFE Home Page  >  Theorem List Contents       This page: Page List

Theorem List for New Foundations Explorer - 3601-3700   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremdisjpss 3601 A class is a proper subset of its union with a disjoint nonempty class. (Contributed by NM, 15-Sep-2004.)
(((AB) = B) → A ⊊ (AB))

Theoremundisj1 3602 The union of disjoint classes is disjoint. (Contributed by NM, 26-Sep-2004.)
(((AC) = (BC) = ) ↔ ((AB) ∩ C) = )

Theoremundisj2 3603 The union of disjoint classes is disjoint. (Contributed by NM, 13-Sep-2004.)
(((AB) = (AC) = ) ↔ (A ∩ (BC)) = )

Theoremssindif0 3604 Subclass expressed in terms of intersection with difference from the universal class. (Contributed by NM, 17-Sep-2003.)
(A B ↔ (A ∩ (V B)) = )

Theoreminelcm 3605 The intersection of classes with a common member is nonempty. (Contributed by NM, 7-Apr-1994.)
((A B A C) → (BC) ≠ )

Theoremminel 3606 A minimum element of a class has no elements in common with the class. (Contributed by NM, 22-Jun-1994.)
((A B (CB) = ) → ¬ A C)

Theoremundif4 3607 Distribute union over difference. (Contributed by NM, 17-May-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
((AC) = → (A ∪ (B C)) = ((AB) C))

Theoremdisjssun 3608 Subset relation for disjoint classes. (Contributed by NM, 25-Oct-2005.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
((AB) = → (A (BC) ↔ A C))

Theoremssdif0 3609 Subclass expressed in terms of difference. Exercise 7 of [TakeutiZaring] p. 22. (Contributed by NM, 29-Apr-1994.)
(A B ↔ (A B) = )

Theoremvdif0 3610 Universal class equality in terms of empty difference. (Contributed by NM, 17-Sep-2003.)
(A = V ↔ (V A) = )

Theorempssdifn0 3611 A proper subclass has a nonempty difference. (Contributed by NM, 3-May-1994.)
((A B AB) → (B A) ≠ )

Theorempssdif 3612 A proper subclass has a nonempty difference. (Contributed by Mario Carneiro, 27-Apr-2016.)
(AB → (B A) ≠ )

Theoremssnelpss 3613 A subclass missing a member is a proper subclass. (Contributed by NM, 12-Jan-2002.)
(A B → ((C B ¬ C A) → AB))

Theoremssnelpssd 3614 Subclass inclusion with one element of the superclass missing is proper subclass inclusion. Deduction form of ssnelpss 3613. (Contributed by David Moews, 1-May-2017.)
(φA B)    &   (φC B)    &   (φ → ¬ C A)       (φAB)

Theorempssnel 3615* A proper subclass has a member in one argument that's not in both. (Contributed by NM, 29-Feb-1996.)
(ABx(x B ¬ x A))

Theoremdifin0ss 3616 Difference, intersection, and subclass relationship. (Contributed by NM, 30-Apr-1994.) (Proof shortened by Wolf Lammen, 30-Sep-2014.)
(((A B) ∩ C) = → (C AC B))

Theoreminssdif0 3617 Intersection, subclass, and difference relationship. (Contributed by NM, 27-Oct-1996.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) (Proof shortened by Wolf Lammen, 30-Sep-2014.)
((AB) C ↔ (A ∩ (B C)) = )

Theoremdifid 3618 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.)
(A A) =

TheoremdifidALT 3619 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 3618. (Contributed by David Abernethy, 17-Jun-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
(A A) =

Theoremdif0 3620 The difference between a class and the empty set. Part of Exercise 4.4 of [Stoll] p. 16. (Contributed by NM, 17-Aug-2004.)
(A ) = A

Theorem0dif 3621 The difference between the empty set and a class. Part of Exercise 4.4 of [Stoll] p. 16. (Contributed by NM, 17-Aug-2004.)
( A) =

Theoremdisjdif 3622 A class and its relative complement are disjoint. Theorem 38 of [Suppes] p. 29. (Contributed by NM, 24-Mar-1998.)
(A ∩ (B A)) =

Theoremdifin0 3623 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.)
((AB) B) =

Theoremundifv 3624 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.)
(A ∪ (V A)) = V

Theoremundif1 3625 Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 3622). Theorem 35 of [Suppes] p. 29. (Contributed by NM, 19-May-1998.)
((A B) ∪ B) = (AB)

Theoremundif2 3626 Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 3622). Part of proof of Corollary 6K of [Enderton] p. 144. (Contributed by NM, 19-May-1998.)
(A ∪ (B A)) = (AB)

Theoremundifabs 3627 Absorption of difference by union. (Contributed by NM, 18-Aug-2013.)
(A ∪ (A B)) = A

Theoreminundif 3628 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.)
((AB) ∪ (A B)) = A

Theoremdifun2 3629 Absorption of union by difference. Theorem 36 of [Suppes] p. 29. (Contributed by NM, 19-May-1998.)
((AB) B) = (A B)

Theoremundif 3630 Union of complementary parts into whole. (Contributed by NM, 22-Mar-1998.)
(A B ↔ (A ∪ (B A)) = B)

Theoremssdifin0 3631 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.)
(A (B C) → (AC) = )

Theoremssdifeq0 3632 A class is a subclass of itself subtracted from another iff it is the empty set. (Contributed by Steve Rodriguez, 20-Nov-2015.)
(A (B A) ↔ A = )

Theoremssundif 3633 A condition equivalent to inclusion in the union of two classes. (Contributed by NM, 26-Mar-2007.)
(A (BC) ↔ (A B) C)

Theoremdifcom 3634 Swap the arguments of a class difference. (Contributed by NM, 29-Mar-2007.)
((A B) C ↔ (A C) B)

Theorempssdifcom1 3635 Two ways to express overlapping subsets. (Contributed by Stefan O'Rear, 31-Oct-2014.)
((A C B C) → ((C A) ⊊ B ↔ (C B) ⊊ A))

Theorempssdifcom2 3636 Two ways to express non-covering pairs of subsets. (Contributed by Stefan O'Rear, 31-Oct-2014.)
((A C B C) → (B ⊊ (C A) ↔ A ⊊ (C B)))

Theoremdifdifdir 3637 Distributive law for class difference. Exercise 4.8 of [Stoll] p. 16. (Contributed by NM, 18-Aug-2004.)
((A B) C) = ((A C) (B C))

Theoremuneqdifeq 3638 Two ways to say that A and B partition C (when A and B don't overlap and A is a part of C). (Contributed by FL, 17-Nov-2008.)
((A C (AB) = ) → ((AB) = C ↔ (C A) = B))

Theoremr19.2z 3639* Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1659). The restricted version is valid only when the domain of quantification is not empty. (Contributed by NM, 15-Nov-2003.)
((A x A φ) → x A φ)

Theoremr19.2zb 3640* A response to the notion that the condition A can be removed in r19.2z 3639. Interestingly enough, φ does not figure in the left-hand side. (Contributed by Jeff Hankins, 24-Aug-2009.)
(A ↔ (x A φx A φ))

Theoremr19.3rz 3641* Restricted quantification of wff not containing quantified variable. (Contributed by FL, 3-Jan-2008.)
xφ       (A → (φx A φ))

Theoremr19.28z 3642* 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.)
xφ       (A → (x A (φ ψ) ↔ (φ x A ψ)))

Theoremr19.3rzv 3643* Restricted quantification of wff not containing quantified variable. (Contributed by NM, 10-Mar-1997.)
(A → (φx A φ))

Theoremr19.9rzv 3644* Restricted quantification of wff not containing quantified variable. (Contributed by NM, 27-May-1998.)
(A → (φx A φ))

Theoremr19.28zv 3645* 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.)
(A → (x A (φ ψ) ↔ (φ x A ψ)))

Theoremr19.37zv 3646* 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.)
(A → (x A (φψ) ↔ (φx A ψ)))

Theoremr19.45zv 3647* Restricted version of Theorem 19.45 of [Margaris] p. 90. (Contributed by NM, 27-May-1998.)
(A → (x A (φ ψ) ↔ (φ x A ψ)))

Theoremr19.27z 3648* 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.)
xψ       (A → (x A (φ ψ) ↔ (x A φ ψ)))

Theoremr19.27zv 3649* 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.)
(A → (x A (φ ψ) ↔ (x A φ ψ)))

Theoremr19.36zv 3650* 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.)
(A → (x A (φψ) ↔ (x A φψ)))

Theoremrzal 3651* Vacuous quantification is always true. (Contributed by NM, 11-Mar-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
(A = x A φ)

Theoremrexn0 3652* Restricted existential quantification implies its restriction is nonempty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.)
(x A φA)

Theoremralidm 3653* Idempotent law for restricted quantifier. (Contributed by NM, 28-Mar-1997.)
(x A x A φx A φ)

Theoremral0 3654 Vacuous universal quantification is always true. (Contributed by NM, 20-Oct-2005.)
x φ

Theoremrgenz 3655* Generalization rule that eliminates a non-zero class requirement. (Contributed by NM, 8-Dec-2012.)
((A x A) → φ)       x A φ

Theoremralf0 3656* The quantification of a falsehood is vacuous when true. (Contributed by NM, 26-Nov-2005.)
¬ φ       (x A φA = )

Theoremraaan 3657* Rearrange restricted quantifiers. (Contributed by NM, 26-Oct-2010.)
yφ    &   xψ       (x A y A (φ ψ) ↔ (x A φ y A ψ))

Theoremraaanv 3658* Rearrange restricted quantifiers. (Contributed by NM, 11-Mar-1997.)
(x A y A (φ ψ) ↔ (x A φ y A ψ))

Theoremsbss 3659* 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.)
([y / x]x Ay A)

Theoremsbcss 3660 Distribute proper substitution through a subclass relation. (Contributed by Alan Sare, 22-Jul-2012.) (Proof shortened by Alexander van der Vekens, 23-Jul-2017.)
(A B → ([̣A / xC D[A / x]C [A / x]D))

Theoremsscon34 3661 Contraposition law for subset. (Contributed by SF, 11-Mar-2015.)
(A B ↔ ∼ B A)

2.1.14  "Weak deduction theorem" for set theory

In a Hilbert system of logic (which consists of a set of axioms, modus ponens, and the generalization rule), converting a deduction to a proof using the Deduction Theorem (taught in introductory logic books) involves an exponential increase of the number of steps as hypotheses are successively eliminated. Here is a trick that is not as general as the Deduction Theorem but requires only a linear increase in the number of steps.

The general problem: We want to convert a deduction P |- Q into a proof of the theorem |- P -> Q i.e. we want to eliminate the hypothesis P. Normally this is done using the Deduction (meta)Theorem, which looks at the microscopic steps of the deduction and usually doubles or triples the number of these microscopic steps for each hypothesis that is eliminated. We will look at a special case of this problem, without appealing to the Deduction Theorem.

We assume ZF with class notation. A and B are arbitrary (possibly proper) classes. P, Q, R, S and T are wffs.

We define the conditional operator, if(P,A,B), as follows: if(P,A,B) =def= { x | (x \in A & P) v (x \in B & -. P) } (where x does not occur in A, B, or P).

Lemma 1. A = if(P,A,B) -> (P <-> R), B = if(P,A,B) -> (S <-> R), S |- R Proof: Logic and Axiom of Extensionality.

Lemma 2. A = if(P,A,B) -> (Q <-> T), T |- P -> Q Proof: Logic and Axiom of Extensionality.

Here's a simple example that illustrates how it works. Suppose we have a deduction Ord A |- Tr A which means, "Assume A is an ordinal class. Then A is a transitive class." Note that A is a class variable that may be substituted with any class expression, so this is really a deduction scheme.

We want to convert this to a proof of the theorem (scheme) |- Ord A -> Tr A.

The catch is that we must be able to prove "Ord A" for at least one object A (and this is what makes it weaker than the ordinary Deduction Theorem). However, it is easy to prove |- Ord 0 (the empty set is ordinal). (For a typical textbook "theorem," i.e. deduction, there is usually at least one object satisfying each hypothesis, otherwise the theorem would not be very useful. We can always go back to the standard Deduction Theorem for those hypotheses where this is not the case.) Continuing with the example:

Equality axioms (and Extensionality) yield |- A = if(Ord A, A, 0) -> (Ord A <-> Ord if(Ord A, A, 0)) (1) |- 0 = if(Ord A, A, 0) -> (Ord 0 <-> Ord if(Ord A, A, 0)) (2) From (1), (2) and |- Ord 0, Lemma 1 yields |- Ord if(Ord A, A, 0) (3) From (3) and substituting if(Ord A, A, 0) for A in the original deduction, |- Tr if(Ord A, A, 0) (4) Equality axioms (and Extensionality) yield |- A = if(Ord A, A, 0) -> (Tr A <-> Tr if(Ord A, A, 0)) (5) From (4) and (5), Lemma 2 yields |- Ord A -> Tr A (Q.E.D.)

Syntaxcif 3662 Extend class notation to include the conditional operator. See df-if 3663 for a description. (In older databases this was denoted "ded".)
class if(φ, A, B)

Definitiondf-if 3663* Define the conditional operator. Read if(φ, A, B) as "if φ then A else B." See iftrue 3668 and iffalse 3669 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 older versions of this database, this operator was denoted "ded" and called the "deduction class.")

An important use for us is in conjunction with the weak deduction theorem, which converts a hypothesis into an antecedent. In that role, A is a class variable in the hypothesis and B is a class (usually a constant) that makes the hypothesis true when it is substituted for A. See dedth 3703 for the main part of the weak deduction theorem, elimhyp 3710 to eliminate a hypothesis, and keephyp 3716 to keep a hypothesis. See the Deduction Theorem link on the Metamath Proof Explorer Home Page for a description of the weak deduction theorem. (Contributed by NM, 15-May-1999.)

if(φ, A, B) = {x ((x A φ) (x B ¬ φ))}

Theoremdfif2 3664* An alternate definition of the conditional operator df-if 3663 with one fewer connectives (but probably less intuitive to understand). (Contributed by NM, 30-Jan-2006.)
if(φ, A, B) = {x ((x Bφ) → (x A φ))}

Theoremdfif6 3665* An alternate definition of the conditional operator df-if 3663 as a simple class abstraction. (Contributed by Mario Carneiro, 8-Sep-2013.)
if(φ, A, B) = ({x A φ} ∪ {x B ¬ φ})

Theoremifeq1 3666 Equality theorem for conditional operator. (Contributed by NM, 1-Sep-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
(A = B → if(φ, A, C) = if(φ, B, C))

Theoremifeq2 3667 Equality theorem for conditional operator. (Contributed by NM, 1-Sep-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
(A = B → if(φ, C, A) = if(φ, C, B))

Theoremiftrue 3668 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(φ, A, B) = A)

Theoremiffalse 3669 Value of the conditional operator when its first argument is false. (Contributed by NM, 14-Aug-1999.)
φ → if(φ, A, B) = B)

Theoremifnefalse 3670 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 vs. applying iffalse 3669 directly in this case. It happens, e.g., in oevn0 in set.mm. (Contributed by David A. Wheeler, 15-May-2015.)
(AB → if(A = B, C, D) = D)

Theoremifsb 3671 Distribute a function over an if-clause. (Contributed by Mario Carneiro, 14-Aug-2013.)
( if(φ, A, B) = AC = D)    &   ( if(φ, A, B) = BC = E)       C = if(φ, D, E)

Theoremdfif3 3672* Alternate definition of the conditional operator df-if 3663. Note that φ is independent of x i.e. a constant true or false. (Contributed by NM, 25-Aug-2013.) (Revised by Mario Carneiro, 8-Sep-2013.)
C = {x φ}        if(φ, A, B) = ((AC) ∪ (B ∩ (V C)))

Theoremdfif4 3673* Alternate definition of the conditional operator df-if 3663. Note that φ is independent of x i.e. a constant true or false. (Contributed by NM, 25-Aug-2013.)
C = {x φ}        if(φ, A, B) = ((AB) ∩ ((A ∪ (V C)) ∩ (BC)))

Theoremdfif5 3674* Alternate definition of the conditional operator df-if 3663. Note that φ is independent of x i.e. a constant true or false (see also abvor0 3567). (Contributed by Gérard Lang, 18-Aug-2013.)
C = {x φ}        if(φ, A, B) = ((AB) ∪ (((A B) ∩ C) ∪ ((B A) ∩ (V C))))

Theoremifeq12 3675 Equality theorem for conditional operators. (Contributed by NM, 1-Sep-2004.)
((A = B C = D) → if(φ, A, C) = if(φ, B, D))

Theoremifeq1d 3676 Equality deduction for conditional operator. (Contributed by NM, 16-Feb-2005.)
(φA = B)       (φ → if(ψ, A, C) = if(ψ, B, C))

Theoremifeq2d 3677 Equality deduction for conditional operator. (Contributed by NM, 16-Feb-2005.)
(φA = B)       (φ → if(ψ, C, A) = if(ψ, C, B))

Theoremifeq12d 3678 Equality deduction for conditional operator. (Contributed by NM, 24-Mar-2015.)
(φA = B)    &   (φC = D)       (φ → if(ψ, A, C) = if(ψ, B, D))

Theoremifbi 3679 Equivalence theorem for conditional operators. (Contributed by Raph Levien, 15-Jan-2004.)
((φψ) → if(φ, A, B) = if(ψ, A, B))

Theoremifbid 3680 Equivalence deduction for conditional operators. (Contributed by NM, 18-Apr-2005.)
(φ → (ψχ))       (φ → if(ψ, A, B) = if(χ, A, B))

Theoremifbieq2i 3681 Equivalence/equality inference for conditional operators. (Contributed by Paul Chapman, 22-Jun-2011.)
(φψ)    &   A = B        if(φ, C, A) = if(ψ, C, B)

Theoremifbieq2d 3682 Equivalence/equality deduction for conditional operators. (Contributed by Paul Chapman, 22-Jun-2011.)
(φ → (ψχ))    &   (φA = B)       (φ → if(ψ, C, A) = if(χ, C, B))

Theoremifbieq12i 3683 Equivalence deduction for conditional operators. (Contributed by NM, 18-Mar-2013.)
(φψ)    &   A = C    &   B = D        if(φ, A, B) = if(ψ, C, D)

Theoremifbieq12d 3684 Equivalence deduction for conditional operators. (Contributed by Jeff Madsen, 2-Sep-2009.)
(φ → (ψχ))    &   (φA = C)    &   (φB = D)       (φ → if(ψ, A, B) = if(χ, C, D))

Theoremnfifd 3685 Deduction version of nfif 3686. (Contributed by NM, 15-Feb-2013.) (Revised by Mario Carneiro, 13-Oct-2016.)
(φ → Ⅎxψ)    &   (φxA)    &   (φxB)       (φx if(ψ, A, B))

Theoremnfif 3686 Bound-variable hypothesis builder for a conditional operator. (Contributed by NM, 16-Feb-2005.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
xφ    &   xA    &   xB       x if(φ, A, B)

Theoremifeq1da 3687 Conditional equality. (Contributed by Jeff Madsen, 2-Sep-2009.)
((φ ψ) → A = B)       (φ → if(ψ, A, C) = if(ψ, B, C))

Theoremifeq2da 3688 Conditional equality. (Contributed by Jeff Madsen, 2-Sep-2009.)
((φ ¬ ψ) → A = B)       (φ → if(ψ, C, A) = if(ψ, C, B))

Theoremifclda 3689 Conditional closure. (Contributed by Jeff Madsen, 2-Sep-2009.)
((φ ψ) → A C)    &   ((φ ¬ ψ) → B C)       (φ → if(ψ, A, B) C)

Theoremcsbifg 3690 Distribute proper substitution through the conditional operator. (Contributed by NM, 24-Feb-2013.) (Revised by Mario Carneiro, 14-Nov-2016.)
(A V[A / x] if(φ, B, C) = if([̣A / xφ, [A / x]B, [A / x]C))

Theoremelimif 3691 Elimination of a conditional operator contained in a wff ψ. (Contributed by NM, 15-Feb-2005.)
( if(φ, A, B) = A → (ψχ))    &   ( if(φ, A, B) = B → (ψθ))       (ψ ↔ ((φ χ) φ θ)))

Theoremifbothda 3692 A wff θ containing a conditional operator is true when both of its cases are true. (Contributed by NM, 15-Feb-2015.)
(A = if(φ, A, B) → (ψθ))    &   (B = if(φ, A, B) → (χθ))    &   ((η φ) → ψ)    &   ((η ¬ φ) → χ)       (ηθ)

Theoremifboth 3693 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.)
(A = if(φ, A, B) → (ψθ))    &   (B = if(φ, A, B) → (χθ))       ((ψ χ) → θ)

Theoremifid 3694 Identical true and false arguments in the conditional operator. (Contributed by NM, 18-Apr-2005.)
if(φ, A, A) = A

Theoremeqif 3695 Expansion of an equality with a conditional operator. (Contributed by NM, 14-Feb-2005.)
(A = if(φ, B, C) ↔ ((φ A = B) φ A = C)))

Theoremelif 3696 Membership in a conditional operator. (Contributed by NM, 14-Feb-2005.)
(A if(φ, B, C) ↔ ((φ A B) φ A C)))

Theoremifel 3697 Membership of a conditional operator. (Contributed by NM, 10-Sep-2005.)
( if(φ, A, B) C ↔ ((φ A C) φ B C)))

Theoremifcl 3698 Membership (closure) of a conditional operator. (Contributed by NM, 4-Apr-2005.)
((A C B C) → if(φ, A, B) C)

Theoremifeqor 3699 The possible values of a conditional operator. (Contributed by NM, 17-Jun-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
( if(φ, A, B) = A if(φ, A, B) = B)

Theoremifnot 3700 Negating the first argument swaps the last two arguments of a conditional operator. (Contributed by NM, 21-Jun-2007.)
if(¬ φ, A, B) = if(φ, B, A)

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6337
 Copyright terms: Public domain < Previous  Next >