P. 35 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 3401-3500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sscon 3401	Contraposition law for subsets. Exercise 15 of [TakeutiZaring] p. 22. (Contributed by NM, 22-Mar-1998.)
|- (A C_ B -> (C \ B) C_ (C \ A))
Theorem	ssdif 3402	Difference law for subsets. (Contributed by NM, 28-May-1998.)
|- (A C_ B -> (A \ C) C_ (B \ C))
Theorem	ssdifd 3403	If A is contained in B, then (A \ C) is contained in (B \ C). Deduction form of ssdif 3402. (Contributed by David Moews, 1-May-2017.)
|- (ph -> A C_ B)   =>   |- (ph -> (A \ C) C_ (B \ C))
Theorem	sscond 3404	If A is contained in B, then (C \ B) is contained in (C \ A). Deduction form of sscon 3401. (Contributed by David Moews, 1-May-2017.)
|- (ph -> A C_ B)   =>   |- (ph -> (C \ B) C_ (C \ A))
Theorem	ssdifssd 3405	If A is contained in B, then (A \ C) is also contained in B. Deduction form of ssdifss 3398. (Contributed by David Moews, 1-May-2017.)
|- (ph -> A C_ B)   =>   |- (ph -> (A \ C) C_ B)
Theorem	ssdif2d 3406	If A is contained in B and C is contained in D, then (A \ D) is contained in (B \ C). Deduction form. (Contributed by David Moews, 1-May-2017.)
|- (ph -> A C_ B)   &   |- (ph -> C C_ D)   =>   |- (ph -> (A \ D) C_ (B \ C))
Theorem	uneqri 3407*	Inference from membership to union. (Contributed by NM, 5-Aug-1993.)
|- ((x e. A \/ x e. B) <-> x e. C)   =>   |- (A u. B) = C
Theorem	unidm 3408	Idempotent law for union of classes. Theorem 23 of [Suppes] p. 27. (Contributed by NM, 5-Aug-1993.)
|- (A u. A) = A
Theorem	uncom 3409	Commutative law for union of classes. Exercise 6 of [TakeutiZaring] p. 17. (Contributed by NM, 25-Jun-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- (A u. B) = (B u. A)
Theorem	equncom 3410	If a class equals the union of two other classes, then it equals the union of those two classes commuted. equncom 3410 was automatically derived from equncomVD in set.mm using the tools program translate_without_overwriting.cmd and minimizing. (Contributed by Alan Sare, 18-Feb-2012.)
|- (A = (B u. C) <-> A = (C u. B))
Theorem	equncomi 3411	Inference form of equncom 3410. equncomi 3411 was automatically derived from equncomiVD in set.mm using the tools program translate_without_overwriting.cmd and minimizing. (Contributed by Alan Sare, 18-Feb-2012.)
|- A = (B u. C)   =>   |- A = (C u. B)
Theorem	uneq1 3412	Equality theorem for union of two classes. (Contributed by NM, 5-Aug-1993.)
|- (A = B -> (A u. C) = (B u. C))
Theorem	uneq2 3413	Equality theorem for the union of two classes. (Contributed by NM, 5-Aug-1993.)
|- (A = B -> (C u. A) = (C u. B))
Theorem	uneq12 3414	Equality theorem for union of two classes. (Contributed by NM, 29-Mar-1998.)
|- ((A = B /\ C = D) -> (A u. C) = (B u. D))
Theorem	uneq1i 3415	Inference adding union to the right in a class equality. (Contributed by NM, 30-Aug-1993.)
|- A = B   =>   |- (A u. C) = (B u. C)
Theorem	uneq2i 3416	Inference adding union to the left in a class equality. (Contributed by NM, 30-Aug-1993.)
|- A = B   =>   |- (C u. A) = (C u. B)
Theorem	uneq12i 3417	Equality inference for union of two classes. (Contributed by NM, 12-Aug-2004.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)
|- A = B   &   |- C = D   =>   |- (A u. C) = (B u. D)
Theorem	uneq1d 3418	Deduction adding union to the right in a class equality. (Contributed by NM, 29-Mar-1998.)
|- (ph -> A = B)   =>   |- (ph -> (A u. C) = (B u. C))
Theorem	uneq2d 3419	Deduction adding union to the left in a class equality. (Contributed by NM, 29-Mar-1998.)
|- (ph -> A = B)   =>   |- (ph -> (C u. A) = (C u. B))
Theorem	uneq12d 3420	Equality deduction for union of two classes. (Contributed by NM, 29-Sep-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- (ph -> A = B)   &   |- (ph -> C = D)   =>   |- (ph -> (A u. C) = (B u. D))
Theorem	unass 3421	Associative law for union of classes. Exercise 8 of [TakeutiZaring] p. 17. (Contributed by NM, 3-May-1994.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ((A u. B) u. C) = (A u. (B u. C))
Theorem	un12 3422	A rearrangement of union. (Contributed by NM, 12-Aug-2004.)
|- (A u. (B u. C)) = (B u. (A u. C))
Theorem	un23 3423	A rearrangement of union. (Contributed by NM, 12-Aug-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ((A u. B) u. C) = ((A u. C) u. B)
Theorem	un4 3424	A rearrangement of the union of 4 classes. (Contributed by NM, 12-Aug-2004.)
|- ((A u. B) u. (C u. D)) = ((A u. C) u. (B u. D))
Theorem	unundi 3425	Union distributes over itself. (Contributed by NM, 17-Aug-2004.)
|- (A u. (B u. C)) = ((A u. B) u. (A u. C))
Theorem	unundir 3426	Union distributes over itself. (Contributed by NM, 17-Aug-2004.)
|- ((A u. B) u. C) = ((A u. C) u. (B u. C))
Theorem	ssun1 3427	Subclass relationship for union of classes. Theorem 25 of [Suppes] p. 27. (Contributed by NM, 5-Aug-1993.)
|- A C_ (A u. B)
Theorem	ssun2 3428	Subclass relationship for union of classes. (Contributed by NM, 30-Aug-1993.)
|- A C_ (B u. A)
Theorem	ssun3 3429	Subclass law for union of classes. (Contributed by NM, 5-Aug-1993.)
|- (A C_ B -> A C_ (B u. C))
Theorem	ssun4 3430	Subclass law for union of classes. (Contributed by NM, 14-Aug-1994.)
|- (A C_ B -> A C_ (C u. B))
Theorem	elun1 3431	Membership law for union of classes. (Contributed by NM, 5-Aug-1993.)
|- (A e. B -> A e. (B u. C))
Theorem	elun2 3432	Membership law for union of classes. (Contributed by NM, 30-Aug-1993.)
|- (A e. B -> A e. (C u. B))
Theorem	unss1 3433	Subclass law for union of classes. (Contributed by NM, 14-Oct-1999.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- (A C_ B -> (A u. C) C_ (B u. C))
Theorem	ssequn1 3434	A relationship between subclass and union. Theorem 26 of [Suppes] p. 27. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- (A C_ B <-> (A u. B) = B)
Theorem	unss2 3435	Subclass law for union of classes. Exercise 7 of [TakeutiZaring] p. 18. (Contributed by NM, 14-Oct-1999.)
|- (A C_ B -> (C u. A) C_ (C u. B))
Theorem	unss12 3436	Subclass law for union of classes. (Contributed by NM, 2-Jun-2004.)
|- ((A C_ B /\ C C_ D) -> (A u. C) C_ (B u. D))
Theorem	ssequn2 3437	A relationship between subclass and union. (Contributed by NM, 13-Jun-1994.)
|- (A C_ B <-> (B u. A) = B)
Theorem	unss 3438	The union of two subclasses is a subclass. Theorem 27 of [Suppes] p. 27 and its converse. (Contributed by NM, 11-Jun-2004.)
|- ((A C_ C /\ B C_ C) <-> (A u. B) C_ C)
Theorem	unssi 3439	An inference showing the union of two subclasses is a subclass. (Contributed by Raph Levien, 10-Dec-2002.)
|- A C_ C   &   |- B C_ C   =>   |- (A u. B) C_ C
Theorem	unssd 3440	A deduction showing the union of two subclasses is a subclass. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- (ph -> A C_ C)   &   |- (ph -> B C_ C)   =>   |- (ph -> (A u. B) C_ C)
Theorem	unssad 3441	If (A u. B) is contained in C, so is A. One-way deduction form of unss 3438. Partial converse of unssd 3440. (Contributed by David Moews, 1-May-2017.)
|- (ph -> (A u. B) C_ C)   =>   |- (ph -> A C_ C)
Theorem	unssbd 3442	If (A u. B) is contained in C, so is B. One-way deduction form of unss 3438. Partial converse of unssd 3440. (Contributed by David Moews, 1-May-2017.)
|- (ph -> (A u. B) C_ C)   =>   |- (ph -> B C_ C)
Theorem	ssun 3443	A condition that implies inclusion in the union of two classes. (Contributed by NM, 23-Nov-2003.)
|- ((A C_ B \/ A C_ C) -> A C_ (B u. C))
Theorem	rexun 3444	Restricted existential quantification over union. (Contributed by Jeff Madsen, 5-Jan-2011.)
|- (E.x e. (A u. B)ph <-> (E.x e. A ph \/ E.x e. B ph))
Theorem	ralunb 3445	Restricted quantification over a union. (Contributed by Scott Fenton, 12-Apr-2011.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|- (A.x e. (A u. B)ph <-> (A.x e. A ph /\ A.x e. B ph))
Theorem	ralun 3446	Restricted quantification over union. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ((A.x e. A ph /\ A.x e. B ph) -> A.x e. (A u. B)ph)
Theorem	elin2 3447	Membership in a class defined as an intersection. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- X = (B i^i C)   =>   |- (A e. X <-> (A e. B /\ A e. C))
Theorem	elin3 3448	Membership in a class defined as a ternary intersection. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- X = ((B i^i C) i^i D)   =>   |- (A e. X <-> (A e. B /\ A e. C /\ A e. D))
Theorem	incom 3449	Commutative law for intersection of classes. Exercise 7 of [TakeutiZaring] p. 17. (Contributed by NM, 5-Aug-1993.)
|- (A i^i B) = (B i^i A)
Theorem	ineqri 3450*	Inference from membership to intersection. (Contributed by NM, 5-Aug-1993.)
|- ((x e. A /\ x e. B) <-> x e. C)   =>   |- (A i^i B) = C
Theorem	ineq1 3451	Equality theorem for intersection of two classes. (Contributed by NM, 14-Dec-1993.)
|- (A = B -> (A i^i C) = (B i^i C))
Theorem	ineq2 3452	Equality theorem for intersection of two classes. (Contributed by NM, 26-Dec-1993.)
|- (A = B -> (C i^i A) = (C i^i B))
Theorem	ineq12 3453	Equality theorem for intersection of two classes. (Contributed by NM, 8-May-1994.)
|- ((A = B /\ C = D) -> (A i^i C) = (B i^i D))
Theorem	ineq1i 3454	Equality inference for intersection of two classes. (Contributed by NM, 26-Dec-1993.)
|- A = B   =>   |- (A i^i C) = (B i^i C)
Theorem	ineq2i 3455	Equality inference for intersection of two classes. (Contributed by NM, 26-Dec-1993.)
|- A = B   =>   |- (C i^i A) = (C i^i B)
Theorem	ineq12i 3456	Equality inference for intersection of two classes. (Contributed by NM, 24-Jun-2004.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)
|- A = B   &   |- C = D   =>   |- (A i^i C) = (B i^i D)
Theorem	ineq1d 3457	Equality deduction for intersection of two classes. (Contributed by NM, 10-Apr-1994.)
|- (ph -> A = B)   =>   |- (ph -> (A i^i C) = (B i^i C))
Theorem	ineq2d 3458	Equality deduction for intersection of two classes. (Contributed by NM, 10-Apr-1994.)
|- (ph -> A = B)   =>   |- (ph -> (C i^i A) = (C i^i B))
Theorem	ineq12d 3459	Equality deduction for intersection of two classes. (Contributed by NM, 24-Jun-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- (ph -> A = B)   &   |- (ph -> C = D)   =>   |- (ph -> (A i^i C) = (B i^i D))
Theorem	ineqan12d 3460	Equality deduction for intersection of two classes. (Contributed by NM, 7-Feb-2007.)
|- (ph -> A = B)   &   |- (ps -> C = D)   =>   |- ((ph /\ ps) -> (A i^i C) = (B i^i D))
Theorem	dfss1 3461	A frequently-used variant of subclass definition df-ss 3260. (Contributed by NM, 10-Jan-2015.)
|- (A C_ B <-> (B i^i A) = A)
Theorem	dfss5 3462	Another definition of subclasshood. Similar to df-ss 3260, dfss 3261, and dfss1 3461. (Contributed by David Moews, 1-May-2017.)
|- (A C_ B <-> A = (B i^i A))
Theorem	csbing 3463	Distribute proper substitution through an intersection relation. (Contributed by Alan Sare, 22-Jul-2012.)
|- (A e. B -> [_A / x]_(C i^i D) = ([_A / x]_C i^i [_A / x]_D))
Theorem	rabbi2dva 3464*	Deduction from a wff to a restricted class abstraction. (Contributed by NM, 14-Jan-2014.)
|- ((ph /\ x e. A) -> (x e. B <-> ps))   =>   |- (ph -> (A i^i B) = {x e. A | ps})
Theorem	inidm 3465	Idempotent law for intersection of classes. Theorem 15 of [Suppes] p. 26. (Contributed by NM, 5-Aug-1993.)
|- (A i^i A) = A
Theorem	inass 3466	Associative law for intersection of classes. Exercise 9 of [TakeutiZaring] p. 17. (Contributed by NM, 3-May-1994.)
|- ((A i^i B) i^i C) = (A i^i (B i^i C))
Theorem	in12 3467	A rearrangement of intersection. (Contributed by NM, 21-Apr-2001.)
|- (A i^i (B i^i C)) = (B i^i (A i^i C))
Theorem	in32 3468	A rearrangement of intersection. (Contributed by NM, 21-Apr-2001.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ((A i^i B) i^i C) = ((A i^i C) i^i B)
Theorem	in13 3469	A rearrangement of intersection. (Contributed by NM, 27-Aug-2012.)
|- (A i^i (B i^i C)) = (C i^i (B i^i A))
Theorem	in31 3470	A rearrangement of intersection. (Contributed by NM, 27-Aug-2012.)
|- ((A i^i B) i^i C) = ((C i^i B) i^i A)
Theorem	inrot 3471	Rotate the intersection of 3 classes. (Contributed by NM, 27-Aug-2012.)
|- ((A i^i B) i^i C) = ((C i^i A) i^i B)
Theorem	in4 3472	Rearrangement of intersection of 4 classes. (Contributed by NM, 21-Apr-2001.)
|- ((A i^i B) i^i (C i^i D)) = ((A i^i C) i^i (B i^i D))
Theorem	inindi 3473	Intersection distributes over itself. (Contributed by NM, 6-May-1994.)
|- (A i^i (B i^i C)) = ((A i^i B) i^i (A i^i C))
Theorem	inindir 3474	Intersection distributes over itself. (Contributed by NM, 17-Aug-2004.)
|- ((A i^i B) i^i C) = ((A i^i C) i^i (B i^i C))
Theorem	sseqin2 3475	A relationship between subclass and intersection. Similar to Exercise 9 of [TakeutiZaring] p. 18. (Contributed by NM, 17-May-1994.)
|- (A C_ B <-> (B i^i A) = A)
Theorem	inss1 3476	The intersection of two classes is a subset of one of them. Part of Exercise 12 of [TakeutiZaring] p. 18. (Contributed by NM, 27-Apr-1994.)
|- (A i^i B) C_ A
Theorem	inss2 3477	The intersection of two classes is a subset of one of them. Part of Exercise 12 of [TakeutiZaring] p. 18. (Contributed by NM, 27-Apr-1994.)
|- (A i^i B) C_ B
Theorem	ssin 3478	Subclass of intersection. Theorem 2.8(vii) of [Monk1] p. 26. (Contributed by NM, 15-Jun-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ((A C_ B /\ A C_ C) <-> A C_ (B i^i C))
Theorem	ssini 3479	An inference showing that a subclass of two classes is a subclass of their intersection. (Contributed by NM, 24-Nov-2003.)
|- A C_ B   &   |- A C_ C   =>   |- A C_ (B i^i C)
Theorem	ssind 3480	A deduction showing that a subclass of two classes is a subclass of their intersection. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- (ph -> A C_ B)   &   |- (ph -> A C_ C)   =>   |- (ph -> A C_ (B i^i C))
Theorem	ssrin 3481	Add right intersection to subclass relation. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- (A C_ B -> (A i^i C) C_ (B i^i C))
Theorem	sslin 3482	Add left intersection to subclass relation. (Contributed by NM, 19-Oct-1999.)
|- (A C_ B -> (C i^i A) C_ (C i^i B))
Theorem	ss2in 3483	Intersection of subclasses. (Contributed by NM, 5-May-2000.)
|- ((A C_ B /\ C C_ D) -> (A i^i C) C_ (B i^i D))
Theorem	ssinss1 3484	Intersection preserves subclass relationship. (Contributed by NM, 14-Sep-1999.)
|- (A C_ C -> (A i^i B) C_ C)
Theorem	inss 3485	Inclusion of an intersection of two classes. (Contributed by NM, 30-Oct-2014.)
|- ((A C_ C \/ B C_ C) -> (A i^i B) C_ C)
Theorem	unabs 3486	Absorption law for union. (Contributed by NM, 16-Apr-2006.)
|- (A u. (A i^i B)) = A
Theorem	inabs 3487	Absorption law for intersection. (Contributed by NM, 16-Apr-2006.)
|- (A i^i (A u. B)) = A
Theorem	nssinpss 3488	Negation of subclass expressed in terms of intersection and proper subclass. (Contributed by NM, 30-Jun-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- (-. A C_ B <-> (A i^i B) C. A)
Theorem	nsspssun 3489	Negation of subclass expressed in terms of proper subclass and union. (Contributed by NM, 15-Sep-2004.)
|- (-. A C_ B <-> B C. (A u. B))
Theorem	dfss4 3490	Subclass defined in terms of class difference. See comments under dfun2 3491. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- (A C_ B <-> (B \ (B \ A)) = A)
Theorem	dfun2 3491	An alternate definition of the union of two classes in terms of class difference, requiring no dummy variables. Along with dfin2 3492 and dfss4 3490 it shows we can express union, intersection, and subset directly in terms of the single "primitive" operation \ (class difference). (Contributed by NM, 10-Jun-2004.)
|- (A u. B) = (_V \ ((_V \ A) \ B))
Theorem	dfin2 3492	An alternate definition of the intersection of two classes in terms of class difference, requiring no dummy variables. See comments under dfun2 3491. Another version is given by dfin4 3496. (Contributed by NM, 10-Jun-2004.)
|- (A i^i B) = (A \ (_V \ B))
Theorem	difin 3493	Difference with intersection. Theorem 33 of [Suppes] p. 29. (Contributed by NM, 31-Mar-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- (A \ (A i^i B)) = (A \ B)
Theorem	dfun3 3494	Union defined in terms of intersection (De Morgan's law). Definition of union in [Mendelson] p. 231. (Contributed by NM, 8-Jan-2002.)
|- (A u. B) = (_V \ ((_V \ A) i^i (_V \ B)))
Theorem	dfin3 3495	Intersection defined in terms of union (De Morgan's law. Similar to Exercise 4.10(n) of [Mendelson] p. 231. (Contributed by NM, 8-Jan-2002.)
|- (A i^i B) = (_V \ ((_V \ A) u. (_V \ B)))
Theorem	dfin4 3496	Alternate definition of the intersection of two classes. Exercise 4.10(q) of [Mendelson] p. 231. (Contributed by NM, 25-Nov-2003.)
|- (A i^i B) = (A \ (A \ B))
Theorem	invdif 3497	Intersection with universal complement. Remark in [Stoll] p. 20. (Contributed by NM, 17-Aug-2004.)
|- (A i^i (_V \ B)) = (A \ B)
Theorem	indif 3498	Intersection with class difference. Theorem 34 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.)
|- (A i^i (A \ B)) = (A \ B)
Theorem	indif2 3499	Bring an intersection in and out of a class difference. (Contributed by Jeff Hankins, 15-Jul-2009.)
|- (A i^i (B \ C)) = ((A i^i B) \ C)
Theorem	indif1 3500	Bring an intersection in and out of a class difference. (Contributed by Mario Carneiro, 15-May-2015.)
|- ((A \ C) i^i B) = ((A i^i B) \ C)