P. 37 of Theorem List - New Foundations Explorer

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

Type	Label	Description
Statement
Theorem	ssdisj 3601	Intersection with a subclass of a disjoint class. (Contributed by FL, 24-Jan-2007.)
|- ((A C_ B /\ (B i^i C) = (/)) -> (A i^i C) = (/))
Theorem	disjpss 3602	A class is a proper subset of its union with a disjoint nonempty class. (Contributed by NM, 15-Sep-2004.)
|- (((A i^i B) = (/) /\ B =/= (/)) -> A C. (A u. B))
Theorem	undisj1 3603	The union of disjoint classes is disjoint. (Contributed by NM, 26-Sep-2004.)
|- (((A i^i C) = (/) /\ (B i^i C) = (/)) <-> ((A u. B) i^i C) = (/))
Theorem	undisj2 3604	The union of disjoint classes is disjoint. (Contributed by NM, 13-Sep-2004.)
|- (((A i^i B) = (/) /\ (A i^i C) = (/)) <-> (A i^i (B u. C)) = (/))
Theorem	ssindif0 3605	Subclass expressed in terms of intersection with difference from the universal class. (Contributed by NM, 17-Sep-2003.)
|- (A C_ B <-> (A i^i (_V \ B)) = (/))
Theorem	inelcm 3606	The intersection of classes with a common member is nonempty. (Contributed by NM, 7-Apr-1994.)
|- ((A e. B /\ A e. C) -> (B i^i C) =/= (/))
Theorem	minel 3607	A minimum element of a class has no elements in common with the class. (Contributed by NM, 22-Jun-1994.)
|- ((A e. B /\ (C i^i B) = (/)) -> -. A e. C)
Theorem	undif4 3608	Distribute union over difference. (Contributed by NM, 17-May-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ((A i^i C) = (/) -> (A u. (B \ C)) = ((A u. B) \ C))
Theorem	disjssun 3609	Subset relation for disjoint classes. (Contributed by NM, 25-Oct-2005.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ((A i^i B) = (/) -> (A C_ (B u. C) <-> A C_ C))
Theorem	ssdif0 3610	Subclass expressed in terms of difference. Exercise 7 of [TakeutiZaring] p. 22. (Contributed by NM, 29-Apr-1994.)
|- (A C_ B <-> (A \ B) = (/))
Theorem	vdif0 3611	Universal class equality in terms of empty difference. (Contributed by NM, 17-Sep-2003.)
|- (A = _V <-> (_V \ A) = (/))
Theorem	pssdifn0 3612	A proper subclass has a nonempty difference. (Contributed by NM, 3-May-1994.)
|- ((A C_ B /\ A =/= B) -> (B \ A) =/= (/))
Theorem	pssdif 3613	A proper subclass has a nonempty difference. (Contributed by Mario Carneiro, 27-Apr-2016.)
|- (A C. B -> (B \ A) =/= (/))
Theorem	ssnelpss 3614	A subclass missing a member is a proper subclass. (Contributed by NM, 12-Jan-2002.)
|- (A C_ B -> ((C e. B /\ -. C e. A) -> A C. B))
Theorem	ssnelpssd 3615	Subclass inclusion with one element of the superclass missing is proper subclass inclusion. Deduction form of ssnelpss 3614. (Contributed by David Moews, 1-May-2017.)
|- (ph -> A C_ B)   &   |- (ph -> C e. B)   &   |- (ph -> -. C e. A)   =>   |- (ph -> A C. B)
Theorem	pssnel 3616*	A proper subclass has a member in one argument that's not in both. (Contributed by NM, 29-Feb-1996.)
|- (A C. B -> E.x(x e. B /\ -. x e. A))
Theorem	difin0ss 3617	Difference, intersection, and subclass relationship. (Contributed by NM, 30-Apr-1994.) (Proof shortened by Wolf Lammen, 30-Sep-2014.)
|- (((A \ B) i^i C) = (/) -> (C C_ A -> C C_ B))
Theorem	inssdif0 3618	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.)
|- ((A i^i B) C_ C <-> (A i^i (B \ C)) = (/))
Theorem	difid 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. (Contributed by NM, 22-Apr-2004.)
|- (A \ A) = (/)
Theorem	difidALT 3620	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 3619. (Contributed by David Abernethy, 17-Jun-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (A \ A) = (/)
Theorem	dif0 3621	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
Theorem	0dif 3622	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) = (/)
Theorem	disjdif 3623	A class and its relative complement are disjoint. Theorem 38 of [Suppes] p. 29. (Contributed by NM, 24-Mar-1998.)
|- (A i^i (B \ A)) = (/)
Theorem	difin0 3624	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.)
|- ((A i^i B) \ B) = (/)
Theorem	undifv 3625	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 u. (_V \ A)) = _V
Theorem	undif1 3626	Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 3623). Theorem 35 of [Suppes] p. 29. (Contributed by NM, 19-May-1998.)
|- ((A \ B) u. B) = (A u. B)
Theorem	undif2 3627	Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 3623). Part of proof of Corollary 6K of [Enderton] p. 144. (Contributed by NM, 19-May-1998.)
|- (A u. (B \ A)) = (A u. B)
Theorem	undifabs 3628	Absorption of difference by union. (Contributed by NM, 18-Aug-2013.)
|- (A u. (A \ B)) = A
Theorem	inundif 3629	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.)
|- ((A i^i B) u. (A \ B)) = A
Theorem	difun2 3630	Absorption of union by difference. Theorem 36 of [Suppes] p. 29. (Contributed by NM, 19-May-1998.)
|- ((A u. B) \ B) = (A \ B)
Theorem	undif 3631	Union of complementary parts into whole. (Contributed by NM, 22-Mar-1998.)
|- (A C_ B <-> (A u. (B \ A)) = B)
Theorem	ssdifin0 3632	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 C_ (B \ C) -> (A i^i C) = (/))
Theorem	ssdifeq0 3633	A class is a subclass of itself subtracted from another iff it is the empty set. (Contributed by Steve Rodriguez, 20-Nov-2015.)
|- (A C_ (B \ A) <-> A = (/))
Theorem	ssundif 3634	A condition equivalent to inclusion in the union of two classes. (Contributed by NM, 26-Mar-2007.)
|- (A C_ (B u. C) <-> (A \ B) C_ C)
Theorem	difcom 3635	Swap the arguments of a class difference. (Contributed by NM, 29-Mar-2007.)
|- ((A \ B) C_ C <-> (A \ C) C_ B)
Theorem	pssdifcom1 3636	Two ways to express overlapping subsets. (Contributed by Stefan O'Rear, 31-Oct-2014.)
|- ((A C_ C /\ B C_ C) -> ((C \ A) C. B <-> (C \ B) C. A))
Theorem	pssdifcom2 3637	Two ways to express non-covering pairs of subsets. (Contributed by Stefan O'Rear, 31-Oct-2014.)
|- ((A C_ C /\ B C_ C) -> (B C. (C \ A) <-> A C. (C \ B)))
Theorem	difdifdir 3638	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))
Theorem	uneqdifeq 3639	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_ C /\ (A i^i B) = (/)) -> ((A u. B) = C <-> (C \ A) = B))
Theorem	r19.2z 3640*	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 =/= (/) /\ A.x e. A ph) -> E.x e. A ph)
Theorem	r19.2zb 3641*	A response to the notion that the condition A =/= (/) can be removed in r19.2z 3640. Interestingly enough, ph does not figure in the left-hand side. (Contributed by Jeff Hankins, 24-Aug-2009.)
|- (A =/= (/) <-> (A.x e. A ph -> E.x e. A ph))
Theorem	r19.3rz 3642*	Restricted quantification of wff not containing quantified variable. (Contributed by FL, 3-Jan-2008.)
|- F/xph   =>   |- (A =/= (/) -> (ph <-> A.x e. A ph))
Theorem	r19.28z 3643*	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.)
|- F/xph   =>   |- (A =/= (/) -> (A.x e. A (ph /\ ps) <-> (ph /\ A.x e. A ps)))
Theorem	r19.3rzv 3644*	Restricted quantification of wff not containing quantified variable. (Contributed by NM, 10-Mar-1997.)
|- (A =/= (/) -> (ph <-> A.x e. A ph))
Theorem	r19.9rzv 3645*	Restricted quantification of wff not containing quantified variable. (Contributed by NM, 27-May-1998.)
|- (A =/= (/) -> (ph <-> E.x e. A ph))
Theorem	r19.28zv 3646*	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 =/= (/) -> (A.x e. A (ph /\ ps) <-> (ph /\ A.x e. A ps)))
Theorem	r19.37zv 3647*	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 =/= (/) -> (E.x e. A (ph -> ps) <-> (ph -> E.x e. A ps)))
Theorem	r19.45zv 3648*	Restricted version of Theorem 19.45 of [Margaris] p. 90. (Contributed by NM, 27-May-1998.)
|- (A =/= (/) -> (E.x e. A (ph \/ ps) <-> (ph \/ E.x e. A ps)))
Theorem	r19.27z 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, 26-Oct-2010.)
|- F/xps   =>   |- (A =/= (/) -> (A.x e. A (ph /\ ps) <-> (A.x e. A ph /\ ps)))
Theorem	r19.27zv 3650*	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 =/= (/) -> (A.x e. A (ph /\ ps) <-> (A.x e. A ph /\ ps)))
Theorem	r19.36zv 3651*	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 =/= (/) -> (E.x e. A (ph -> ps) <-> (A.x e. A ph -> ps)))
Theorem	rzal 3652*	Vacuous quantification is always true. (Contributed by NM, 11-Mar-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- (A = (/) -> A.x e. A ph)
Theorem	rexn0 3653*	Restricted existential quantification implies its restriction is nonempty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.)
|- (E.x e. A ph -> A =/= (/))
Theorem	ralidm 3654*	Idempotent law for restricted quantifier. (Contributed by NM, 28-Mar-1997.)
|- (A.x e. A A.x e. A ph <-> A.x e. A ph)
Theorem	ral0 3655	Vacuous universal quantification is always true. (Contributed by NM, 20-Oct-2005.)
|- A.x e. (/) ph
Theorem	rgenz 3656*	Generalization rule that eliminates a nonzero class requirement. (Contributed by NM, 8-Dec-2012.)
|- ((A =/= (/) /\ x e. A) -> ph)   =>   |- A.x e. A ph
Theorem	ralf0 3657*	The quantification of a falsehood is vacuous when true. (Contributed by NM, 26-Nov-2005.)
|- -. ph   =>   |- (A.x e. A ph <-> A = (/))
Theorem	raaan 3658*	Rearrange restricted quantifiers. (Contributed by NM, 26-Oct-2010.)
|- F/yph   &   |- F/xps   =>   |- (A.x e. A A.y e. A (ph /\ ps) <-> (A.x e. A ph /\ A.y e. A ps))
Theorem	raaanv 3659*	Rearrange restricted quantifiers. (Contributed by NM, 11-Mar-1997.)
|- (A.x e. A A.y e. A (ph /\ ps) <-> (A.x e. A ph /\ A.y e. A ps))
Theorem	sbss 3660*	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 C_ A <-> y C_ A)
Theorem	sbcss 3661	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 e. B -> ( [.A / x ].C C_ D <-> [_A / x]_C C_ [_A / x]_D))
Theorem	sscon34 3662	Contraposition law for subset. (Contributed by SF, 11-Mar-2015.)
|- (A C_ B <-> ∼ B C_ ∼ 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.)
Syntax	cif 3663	Extend class notation to include the conditional operator. See df-if 3664 for a description. (In older databases this was denoted "ded".)
class if(ph, A, B)
Definition	df-if 3664*	Define the conditional operator. Read if(ph, A, B) as "if ph then A else B." See iftrue 3669 and iffalse 3670 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 3704 for the main part of the weak deduction theorem, elimhyp 3711 to eliminate a hypothesis, and keephyp 3717 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(ph, A, B) = {x | ((x e. A /\ ph) \/ (x e. B /\ -. ph))}
Theorem	dfif2 3665*	An alternate definition of the conditional operator df-if 3664 with one fewer connectives (but probably less intuitive to understand). (Contributed by NM, 30-Jan-2006.)
|- if(ph, A, B) = {x | ((x e. B -> ph) -> (x e. A /\ ph))}
Theorem	dfif6 3666*	An alternate definition of the conditional operator df-if 3664 as a simple class abstraction. (Contributed by Mario Carneiro, 8-Sep-2013.)
|- if(ph, A, B) = ({x e. A | ph} u. {x e. B | -. ph})
Theorem	ifeq1 3667	Equality theorem for conditional operator. (Contributed by NM, 1-Sep-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- (A = B -> if(ph, A, C) = if(ph, B, C))
Theorem	ifeq2 3668	Equality theorem for conditional operator. (Contributed by NM, 1-Sep-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- (A = B -> if(ph, C, A) = if(ph, C, B))
Theorem	iftrue 3669	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.)
|- (ph -> if(ph, A, B) = A)
Theorem	iffalse 3670	Value of the conditional operator when its first argument is false. (Contributed by NM, 14-Aug-1999.)
|- (-. ph -> if(ph, A, B) = B)
Theorem	ifnefalse 3671	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 3670 directly in this case. It happens, e.g., in oevn0 in set.mm. (Contributed by David A. Wheeler, 15-May-2015.)
|- (A =/= B -> if(A = B, C, D) = D)
Theorem	ifsb 3672	Distribute a function over an if-clause. (Contributed by Mario Carneiro, 14-Aug-2013.)
|- (if(ph, A, B) = A -> C = D)   &   |- (if(ph, A, B) = B -> C = E)   =>   |- C = if(ph, D, E)
Theorem	dfif3 3673*	Alternate definition of the conditional operator df-if 3664. Note that ph 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 | ph}   =>   |- if(ph, A, B) = ((A i^i C) u. (B i^i (_V \ C)))
Theorem	dfif4 3674*	Alternate definition of the conditional operator df-if 3664. Note that ph is independent of x i.e. a constant true or false. (Contributed by NM, 25-Aug-2013.)
|- C = {x | ph}   =>   |- if(ph, A, B) = ((A u. B) i^i ((A u. (_V \ C)) i^i (B u. C)))
Theorem	dfif5 3675*	Alternate definition of the conditional operator df-if 3664. Note that ph is independent of x i.e. a constant true or false (see also abvor0 3568). (Contributed by Gérard Lang, 18-Aug-2013.)
|- C = {x | ph}   =>   |- if(ph, A, B) = ((A i^i B) u. (((A \ B) i^i C) u. ((B \ A) i^i (_V \ C))))
Theorem	ifeq12 3676	Equality theorem for conditional operators. (Contributed by NM, 1-Sep-2004.)
|- ((A = B /\ C = D) -> if(ph, A, C) = if(ph, B, D))
Theorem	ifeq1d 3677	Equality deduction for conditional operator. (Contributed by NM, 16-Feb-2005.)
|- (ph -> A = B)   =>   |- (ph -> if(ps, A, C) = if(ps, B, C))
Theorem	ifeq2d 3678	Equality deduction for conditional operator. (Contributed by NM, 16-Feb-2005.)
|- (ph -> A = B)   =>   |- (ph -> if(ps, C, A) = if(ps, C, B))
Theorem	ifeq12d 3679	Equality deduction for conditional operator. (Contributed by NM, 24-Mar-2015.)
|- (ph -> A = B)   &   |- (ph -> C = D)   =>   |- (ph -> if(ps, A, C) = if(ps, B, D))
Theorem	ifbi 3680	Equivalence theorem for conditional operators. (Contributed by Raph Levien, 15-Jan-2004.)
|- ((ph <-> ps) -> if(ph, A, B) = if(ps, A, B))
Theorem	ifbid 3681	Equivalence deduction for conditional operators. (Contributed by NM, 18-Apr-2005.)
|- (ph -> (ps <-> ch))   =>   |- (ph -> if(ps, A, B) = if(ch, A, B))
Theorem	ifbieq2i 3682	Equivalence/equality inference for conditional operators. (Contributed by Paul Chapman, 22-Jun-2011.)
|- (ph <-> ps)   &   |- A = B   =>   |- if(ph, C, A) = if(ps, C, B)
Theorem	ifbieq2d 3683	Equivalence/equality deduction for conditional operators. (Contributed by Paul Chapman, 22-Jun-2011.)
|- (ph -> (ps <-> ch))   &   |- (ph -> A = B)   =>   |- (ph -> if(ps, C, A) = if(ch, C, B))
Theorem	ifbieq12i 3684	Equivalence deduction for conditional operators. (Contributed by NM, 18-Mar-2013.)
|- (ph <-> ps)   &   |- A = C   &   |- B = D   =>   |- if(ph, A, B) = if(ps, C, D)
Theorem	ifbieq12d 3685	Equivalence deduction for conditional operators. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- (ph -> (ps <-> ch))   &   |- (ph -> A = C)   &   |- (ph -> B = D)   =>   |- (ph -> if(ps, A, B) = if(ch, C, D))
Theorem	nfifd 3686	Deduction version of nfif 3687. (Contributed by NM, 15-Feb-2013.) (Revised by Mario Carneiro, 13-Oct-2016.)
|- (ph -> F/xps)   &   |- (ph -> F/_xA)   &   |- (ph -> F/_xB)   =>   |- (ph -> F/_xif(ps, A, B))
Theorem	nfif 3687	Bound-variable hypothesis builder for a conditional operator. (Contributed by NM, 16-Feb-2005.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- F/xph   &   |- F/_xA   &   |- F/_xB   =>   |- F/_xif(ph, A, B)
Theorem	ifeq1da 3688	Conditional equality. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ((ph /\ ps) -> A = B)   =>   |- (ph -> if(ps, A, C) = if(ps, B, C))
Theorem	ifeq2da 3689	Conditional equality. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ((ph /\ -. ps) -> A = B)   =>   |- (ph -> if(ps, C, A) = if(ps, C, B))
Theorem	ifclda 3690	Conditional closure. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ((ph /\ ps) -> A e. C)   &   |- ((ph /\ -. ps) -> B e. C)   =>   |- (ph -> if(ps, A, B) e. C)
Theorem	csbifg 3691	Distribute proper substitution through the conditional operator. (Contributed by NM, 24-Feb-2013.) (Revised by Mario Carneiro, 14-Nov-2016.)
|- (A e. V -> [_A / x]_if(ph, B, C) = if( [.A / x ].ph, [_A / x]_B, [_A / x]_C))
Theorem	elimif 3692	Elimination of a conditional operator contained in a wff ps. (Contributed by NM, 15-Feb-2005.)
|- (if(ph, A, B) = A -> (ps <-> ch))   &   |- (if(ph, A, B) = B -> (ps <-> th))   =>   |- (ps <-> ((ph /\ ch) \/ (-. ph /\ th)))
Theorem	ifbothda 3693	A wff th containing a conditional operator is true when both of its cases are true. (Contributed by NM, 15-Feb-2015.)
|- (A = if(ph, A, B) -> (ps <-> th))   &   |- (B = if(ph, A, B) -> (ch <-> th))   &   |- ((et /\ ph) -> ps)   &   |- ((et /\ -. ph) -> ch)   =>   |- (et -> th)
Theorem	ifboth 3694	A wff th 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(ph, A, B) -> (ps <-> th))   &   |- (B = if(ph, A, B) -> (ch <-> th))   =>   |- ((ps /\ ch) -> th)
Theorem	ifid 3695	Identical true and false arguments in the conditional operator. (Contributed by NM, 18-Apr-2005.)
|- if(ph, A, A) = A
Theorem	eqif 3696	Expansion of an equality with a conditional operator. (Contributed by NM, 14-Feb-2005.)
|- (A = if(ph, B, C) <-> ((ph /\ A = B) \/ (-. ph /\ A = C)))
Theorem	elif 3697	Membership in a conditional operator. (Contributed by NM, 14-Feb-2005.)
|- (A e. if(ph, B, C) <-> ((ph /\ A e. B) \/ (-. ph /\ A e. C)))
Theorem	ifel 3698	Membership of a conditional operator. (Contributed by NM, 10-Sep-2005.)
|- (if(ph, A, B) e. C <-> ((ph /\ A e. C) \/ (-. ph /\ B e. C)))
Theorem	ifcl 3699	Membership (closure) of a conditional operator. (Contributed by NM, 4-Apr-2005.)
|- ((A e. C /\ B e. C) -> if(ph, A, B) e. C)
Theorem	ifeqor 3700	The possible values of a conditional operator. (Contributed by NM, 17-Jun-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- (if(ph, A, B) = A \/ if(ph, A, B) = B)