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)) |