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