HomeHome New Foundations Explorer
Theorem List (p. 35 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 - 3401-3500   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremssdif 3401 Difference law for subsets. (Contributed by NM, 28-May-1998.)
(A B → (A C) (B C))
 
Theoremssdifd 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))
 
Theoremsscond 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))
 
Theoremssdifssd 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)
 
Theoremssdif2d 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))
 
Theoremuneqri 3406* Inference from membership to union. (Contributed by NM, 5-Aug-1993.)
((x A x B) ↔ x C)       (AB) = C
 
Theoremunidm 3407 Idempotent law for union of classes. Theorem 23 of [Suppes] p. 27. (Contributed by NM, 5-Aug-1993.)
(AA) = A
 
Theoremuncom 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.)
(AB) = (BA)
 
Theoremequncom 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 = (BC) ↔ A = (CB))
 
Theoremequncomi 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 = (BC)       A = (CB)
 
Theoremuneq1 3411 Equality theorem for union of two classes. (Contributed by NM, 5-Aug-1993.)
(A = B → (AC) = (BC))
 
Theoremuneq2 3412 Equality theorem for the union of two classes. (Contributed by NM, 5-Aug-1993.)
(A = B → (CA) = (CB))
 
Theoremuneq12 3413 Equality theorem for union of two classes. (Contributed by NM, 29-Mar-1998.)
((A = B C = D) → (AC) = (BD))
 
Theoremuneq1i 3414 Inference adding union to the right in a class equality. (Contributed by NM, 30-Aug-1993.)
A = B       (AC) = (BC)
 
Theoremuneq2i 3415 Inference adding union to the left in a class equality. (Contributed by NM, 30-Aug-1993.)
A = B       (CA) = (CB)
 
Theoremuneq12i 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       (AC) = (BD)
 
Theoremuneq1d 3417 Deduction adding union to the right in a class equality. (Contributed by NM, 29-Mar-1998.)
(φA = B)       (φ → (AC) = (BC))
 
Theoremuneq2d 3418 Deduction adding union to the left in a class equality. (Contributed by NM, 29-Mar-1998.)
(φA = B)       (φ → (CA) = (CB))
 
Theoremuneq12d 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)       (φ → (AC) = (BD))
 
Theoremunass 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.)
((AB) ∪ C) = (A ∪ (BC))
 
Theoremun12 3421 A rearrangement of union. (Contributed by NM, 12-Aug-2004.)
(A ∪ (BC)) = (B ∪ (AC))
 
Theoremun23 3422 A rearrangement of union. (Contributed by NM, 12-Aug-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
((AB) ∪ C) = ((AC) ∪ B)
 
Theoremun4 3423 A rearrangement of the union of 4 classes. (Contributed by NM, 12-Aug-2004.)
((AB) ∪ (CD)) = ((AC) ∪ (BD))
 
Theoremunundi 3424 Union distributes over itself. (Contributed by NM, 17-Aug-2004.)
(A ∪ (BC)) = ((AB) ∪ (AC))
 
Theoremunundir 3425 Union distributes over itself. (Contributed by NM, 17-Aug-2004.)
((AB) ∪ C) = ((AC) ∪ (BC))
 
Theoremssun1 3426 Subclass relationship for union of classes. Theorem 25 of [Suppes] p. 27. (Contributed by NM, 5-Aug-1993.)
A (AB)
 
Theoremssun2 3427 Subclass relationship for union of classes. (Contributed by NM, 30-Aug-1993.)
A (BA)
 
Theoremssun3 3428 Subclass law for union of classes. (Contributed by NM, 5-Aug-1993.)
(A BA (BC))
 
Theoremssun4 3429 Subclass law for union of classes. (Contributed by NM, 14-Aug-1994.)
(A BA (CB))
 
Theoremelun1 3430 Membership law for union of classes. (Contributed by NM, 5-Aug-1993.)
(A BA (BC))
 
Theoremelun2 3431 Membership law for union of classes. (Contributed by NM, 30-Aug-1993.)
(A BA (CB))
 
Theoremunss1 3432 Subclass law for union of classes. (Contributed by NM, 14-Oct-1999.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
(A B → (AC) (BC))
 
Theoremssequn1 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 ↔ (AB) = B)
 
Theoremunss2 3434 Subclass law for union of classes. Exercise 7 of [TakeutiZaring] p. 18. (Contributed by NM, 14-Oct-1999.)
(A B → (CA) (CB))
 
Theoremunss12 3435 Subclass law for union of classes. (Contributed by NM, 2-Jun-2004.)
((A B C D) → (AC) (BD))
 
Theoremssequn2 3436 A relationship between subclass and union. (Contributed by NM, 13-Jun-1994.)
(A B ↔ (BA) = B)
 
Theoremunss 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) ↔ (AB) C)
 
Theoremunssi 3438 An inference showing the union of two subclasses is a subclass. (Contributed by Raph Levien, 10-Dec-2002.)
A C    &   B C       (AB) C
 
Theoremunssd 3439 A deduction showing the union of two subclasses is a subclass. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
(φA C)    &   (φB C)       (φ → (AB) C)
 
Theoremunssad 3440 If (AB) 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.)
(φ → (AB) C)       (φA C)
 
Theoremunssbd 3441 If (AB) 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.)
(φ → (AB) C)       (φB C)
 
Theoremssun 3442 A condition that implies inclusion in the union of two classes. (Contributed by NM, 23-Nov-2003.)
((A B A C) → A (BC))
 
Theoremrexun 3443 Restricted existential quantification over union. (Contributed by Jeff Madsen, 5-Jan-2011.)
(x (AB)φ ↔ (x A φ x B φ))
 
Theoremralunb 3444 Restricted quantification over a union. (Contributed by Scott Fenton, 12-Apr-2011.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
(x (AB)φ ↔ (x A φ x B φ))
 
Theoremralun 3445 Restricted quantification over union. (Contributed by Jeff Madsen, 2-Sep-2009.)
((x A φ x B φ) → x (AB)φ)
 
Theoremelin2 3446 Membership in a class defined as an intersection. (Contributed by Stefan O'Rear, 29-Mar-2015.)
X = (BC)       (A X ↔ (A B A C))
 
Theoremelin3 3447 Membership in a class defined as a ternary intersection. (Contributed by Stefan O'Rear, 29-Mar-2015.)
X = ((BC) ∩ D)       (A X ↔ (A B A C A D))
 
Theoremincom 3448 Commutative law for intersection of classes. Exercise 7 of [TakeutiZaring] p. 17. (Contributed by NM, 5-Aug-1993.)
(AB) = (BA)
 
Theoremineqri 3449* Inference from membership to intersection. (Contributed by NM, 5-Aug-1993.)
((x A x B) ↔ x C)       (AB) = C
 
Theoremineq1 3450 Equality theorem for intersection of two classes. (Contributed by NM, 14-Dec-1993.)
(A = B → (AC) = (BC))
 
Theoremineq2 3451 Equality theorem for intersection of two classes. (Contributed by NM, 26-Dec-1993.)
(A = B → (CA) = (CB))
 
Theoremineq12 3452 Equality theorem for intersection of two classes. (Contributed by NM, 8-May-1994.)
((A = B C = D) → (AC) = (BD))
 
Theoremineq1i 3453 Equality inference for intersection of two classes. (Contributed by NM, 26-Dec-1993.)
A = B       (AC) = (BC)
 
Theoremineq2i 3454 Equality inference for intersection of two classes. (Contributed by NM, 26-Dec-1993.)
A = B       (CA) = (CB)
 
Theoremineq12i 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       (AC) = (BD)
 
Theoremineq1d 3456 Equality deduction for intersection of two classes. (Contributed by NM, 10-Apr-1994.)
(φA = B)       (φ → (AC) = (BC))
 
Theoremineq2d 3457 Equality deduction for intersection of two classes. (Contributed by NM, 10-Apr-1994.)
(φA = B)       (φ → (CA) = (CB))
 
Theoremineq12d 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)       (φ → (AC) = (BD))
 
Theoremineqan12d 3459 Equality deduction for intersection of two classes. (Contributed by NM, 7-Feb-2007.)
(φA = B)    &   (ψC = D)       ((φ ψ) → (AC) = (BD))
 
Theoremdfss1 3460 A frequently-used variant of subclass definition df-ss 3259. (Contributed by NM, 10-Jan-2015.)
(A B ↔ (BA) = A)
 
Theoremdfss5 3461 Another definition of subclasshood. Similar to df-ss 3259, dfss 3260, and dfss1 3460. (Contributed by David Moews, 1-May-2017.)
(A BA = (BA))
 
Theoremcsbing 3462 Distribute proper substitution through an intersection relation. (Contributed by Alan Sare, 22-Jul-2012.)
(A B[A / x](CD) = ([A / x]C[A / x]D))
 
Theoremrabbi2dva 3463* Deduction from a wff to a restricted class abstraction. (Contributed by NM, 14-Jan-2014.)
((φ x A) → (x Bψ))       (φ → (AB) = {x A ψ})
 
Theoreminidm 3464 Idempotent law for intersection of classes. Theorem 15 of [Suppes] p. 26. (Contributed by NM, 5-Aug-1993.)
(AA) = A
 
Theoreminass 3465 Associative law for intersection of classes. Exercise 9 of [TakeutiZaring] p. 17. (Contributed by NM, 3-May-1994.)
((AB) ∩ C) = (A ∩ (BC))
 
Theoremin12 3466 A rearrangement of intersection. (Contributed by NM, 21-Apr-2001.)
(A ∩ (BC)) = (B ∩ (AC))
 
Theoremin32 3467 A rearrangement of intersection. (Contributed by NM, 21-Apr-2001.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
((AB) ∩ C) = ((AC) ∩ B)
 
Theoremin13 3468 A rearrangement of intersection. (Contributed by NM, 27-Aug-2012.)
(A ∩ (BC)) = (C ∩ (BA))
 
Theoremin31 3469 A rearrangement of intersection. (Contributed by NM, 27-Aug-2012.)
((AB) ∩ C) = ((CB) ∩ A)
 
Theoreminrot 3470 Rotate the intersection of 3 classes. (Contributed by NM, 27-Aug-2012.)
((AB) ∩ C) = ((CA) ∩ B)
 
Theoremin4 3471 Rearrangement of intersection of 4 classes. (Contributed by NM, 21-Apr-2001.)
((AB) ∩ (CD)) = ((AC) ∩ (BD))
 
Theoreminindi 3472 Intersection distributes over itself. (Contributed by NM, 6-May-1994.)
(A ∩ (BC)) = ((AB) ∩ (AC))
 
Theoreminindir 3473 Intersection distributes over itself. (Contributed by NM, 17-Aug-2004.)
((AB) ∩ C) = ((AC) ∩ (BC))
 
Theoremsseqin2 3474 A relationship between subclass and intersection. Similar to Exercise 9 of [TakeutiZaring] p. 18. (Contributed by NM, 17-May-1994.)
(A B ↔ (BA) = A)
 
Theoreminss1 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.)
(AB) A
 
Theoreminss2 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.)
(AB) B
 
Theoremssin 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 (BC))
 
Theoremssini 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 (BC)
 
Theoremssind 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 (BC))
 
Theoremssrin 3480 Add right intersection to subclass relation. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
(A B → (AC) (BC))
 
Theoremsslin 3481 Add left intersection to subclass relation. (Contributed by NM, 19-Oct-1999.)
(A B → (CA) (CB))
 
Theoremss2in 3482 Intersection of subclasses. (Contributed by NM, 5-May-2000.)
((A B C D) → (AC) (BD))
 
Theoremssinss1 3483 Intersection preserves subclass relationship. (Contributed by NM, 14-Sep-1999.)
(A C → (AB) C)
 
Theoreminss 3484 Inclusion of an intersection of two classes. (Contributed by NM, 30-Oct-2014.)
((A C B C) → (AB) C)
 
Theoremunabs 3485 Absorption law for union. (Contributed by NM, 16-Apr-2006.)
(A ∪ (AB)) = A
 
Theoreminabs 3486 Absorption law for intersection. (Contributed by NM, 16-Apr-2006.)
(A ∩ (AB)) = A
 
Theoremnssinpss 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 ↔ (AB) ⊊ A)
 
Theoremnsspssun 3488 Negation of subclass expressed in terms of proper subclass and union. (Contributed by NM, 15-Sep-2004.)
A BB ⊊ (AB))
 
Theoremdfss4 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)
 
Theoremdfun2 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.)
(AB) = (V ((V A) B))
 
Theoremdfin2 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.)
(AB) = (A (V B))
 
Theoremdifin 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 (AB)) = (A B)
 
Theoremdfun3 3493 Union defined in terms of intersection (De Morgan's law). Definition of union in [Mendelson] p. 231. (Contributed by NM, 8-Jan-2002.)
(AB) = (V ((V A) ∩ (V B)))
 
Theoremdfin3 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.)
(AB) = (V ((V A) ∪ (V B)))
 
Theoremdfin4 3495 Alternate definition of the intersection of two classes. Exercise 4.10(q) of [Mendelson] p. 231. (Contributed by NM, 25-Nov-2003.)
(AB) = (A (A B))
 
Theoreminvdif 3496 Intersection with universal complement. Remark in [Stoll] p. 20. (Contributed by NM, 17-Aug-2004.)
(A ∩ (V B)) = (A B)
 
Theoremindif 3497 Intersection with class difference. Theorem 34 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.)
(A ∩ (A B)) = (A B)
 
Theoremindif2 3498 Bring an intersection in and out of a class difference. (Contributed by Jeff Hankins, 15-Jul-2009.)
(A ∩ (B C)) = ((AB) C)
 
Theoremindif1 3499 Bring an intersection in and out of a class difference. (Contributed by Mario Carneiro, 15-May-2015.)
((A C) ∩ B) = ((AB) C)
 
Theoremindifcom 3500 Commutation law for intersection and difference. (Contributed by Scott Fenton, 18-Feb-2013.)
(A ∩ (B C)) = (B ∩ (A C))
    < Previous  Next >

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-6338
  Copyright terms: Public domain < Previous  Next >