HomeHome New Foundations Explorer
Theorem List (p. 33 of 64)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  NFE Home Page  >  Theorem List Contents       This page: Page List

Theorem List for New Foundations Explorer - 3201-3300   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremcbvrabcsf 3201 A more general version of cbvrab 2857 with no distinct variable restrictions. (Contributed by Andrew Salmon, 13-Jul-2011.)
 F/_   &     F/_   &     F/   &     F/   &       &       =>   
 
Theoremcbvralv2 3202* Rule used to change the bound variable in a restricted universal quantifier with implicit substitution which also changes the quantifier domain. (Contributed by David Moews, 1-May-2017.)
   &       =>   
 
Theoremcbvrexv2 3203* Rule used to change the bound variable in a restricted existential quantifier with implicit substitution which also changes the quantifier domain. (Contributed by David Moews, 1-May-2017.)
   &       =>   
 
2.1.10  Define boolean set operations
 
Syntaxcnin 3204 Extend class notation to include anti-intersection (read: "the anti-intersection of and ").
&ncap
 
Syntaxccompl 3205 Extend class notation to include complement. (read: "the complement of " ).
 
Syntaxcdif 3206 Extend class notation to include class difference (read: " minus ").
 
Syntaxcun 3207 Extend class notation to include union of two classes (read: " union ").
 
Syntaxcin 3208 Extend class notation to include the intersection of two classes (read: " intersect ").
 
Syntaxcsymdif 3209 Extend class notation to include the symmetric difference of two classes.
 
Theoremninjust 3210* Soundness theorem for df-nin 3211. (Contributed by SF, 10-Jan-2015.)
 
Definitiondf-nin 3211* Define the anti-intersection of two classes. This operation is used implicitly after Axiom P1 of [Hailperin] p. 6, though there does not seem to be any notation for it in the literature. (Contributed by SF, 10-Jan-2015.)
&ncap
 
Definitiondf-compl 3212 Define the complement of a class. Compare nic-dfneg 1435. (Contributed by SF, 10-Jan-2015.)
&ncap
 
Definitiondf-in 3213 Define the intersection of two classes. See elin 3219 for membership. (Contributed by SF, 10-Jan-2015.)
&ncap
 
Definitiondf-un 3214 Define the union of two classes. See elun 3220 for membership. (Contributed by SF, 10-Jan-2015.)
&ncap ∼
 
Definitiondf-dif 3215 Define the difference of two classes. See eldif 3221 for membership. (Contributed by SF, 10-Jan-2015.)
 
Definitiondf-symdif 3216 Define the symmetric difference of two classes. Definition IX.9.10, [Rosser] p. 238. (Contributed by SF, 10-Jan-2015.)
 
Theoremelning 3217 Membership in anti-intersection. (Contributed by SF, 10-Jan-2015.)
&ncap
 
Theoremelcomplg 3218 Membership in class complement. (Contributed by SF, 10-Jan-2015.)
 
Theoremelin 3219 Membership in intersection. (Contributed by SF, 10-Jan-2015.)
 
Theoremelun 3220 Membership in union. (Contributed by SF, 10-Jan-2015.)
 
Theoremeldif 3221 Membership in difference. (Contributed by SF, 10-Jan-2015.)
 
Theoremdfdif2 3222* Alternate definition of class difference. (Contributed by NM, 25-Mar-2004.)
 
Theoremelsymdif 3223 Membership in symmetric difference. (Contributed by SF, 10-Jan-2015.)
 
Theoremelnin 3224 Membership in anti-intersection. (Contributed by SF, 10-Jan-2015.)
   =>    &ncap
 
Theoremelcompl 3225 Membership in complement. (Contributed by SF, 10-Jan-2015.)
   =>   
 
Theoremnincom 3226 Anti-intersection commutes. (Contributed by SF, 10-Jan-2015.)
&ncap &ncap
 
Theoremdblcompl 3227 Double complement law. (Contributed by SF, 10-Jan-2015.)
∼ ∼
 
Theoremnfnin 3228 Hypothesis builder for anti-intersection. (Contributed by SF, 2-Jan-2018.)
 F/_   &     F/_   =>     F/_ &ncap
 
Theoremnfcompl 3229 Hypothesis builder for complement. (Contributed by SF, 2-Jan-2018.)
 F/_   =>     F/_
 
Theoremnfin 3230 Hypothesis builder for intersection. (Contributed by SF, 2-Jan-2018.)
 F/_   &     F/_   =>     F/_
 
Theoremnfun 3231 Hypothesis builder for union. (Contributed by SF, 2-Jan-2018.)
 F/_   &     F/_   =>     F/_
 
Theoremnfdif 3232 Hypothesis builder for difference. (Contributed by SF, 2-Jan-2018.)
 F/_   &     F/_   =>     F/_
 
Theoremnfsymdif 3233 Hypothesis builder for symmetric difference. (Contributed by SF, 2-Jan-2018.)
 F/_   &     F/_   =>     F/_
 
Theoremnineq1 3234 Equality law for anti-intersection. (Contributed by SF, 11-Jan-2015.)
&ncap &ncap
 
Theoremnineq2 3235 Equality law for anti-intersection. (Contributed by SF, 11-Jan-2015.)
&ncap &ncap
 
Theoremnineq12 3236 Equality law for anti-intersection. (Contributed by SF, 11-Jan-2015.)
&ncap &ncap
 
Theoremnineq1i 3237 Equality inference for anti-intersection. (Contributed by SF, 11-Jan-2015.)
   =>    &ncap &ncap
 
Theoremnineq2i 3238 Equality inference for anti-intersection. (Contributed by SF, 11-Jan-2015.)
   =>    &ncap &ncap
 
Theoremnineq12i 3239 Equality inference for anti-intersection. (Contributed by SF, 11-Jan-2015.)
   &       =>    &ncap &ncap
 
Theoremnineq1d 3240 Equality deduction for anti-intersection. (Contributed by SF, 11-Jan-2015.)
   =>    &ncap &ncap
 
Theoremnineq2d 3241 Equality deduction for anti-intersection. (Contributed by SF, 11-Jan-2015.)
   =>    &ncap &ncap
 
Theoremnineq12d 3242 Equality inference for anti-intersection. (Contributed by SF, 11-Jan-2015.)
   &       =>    &ncap &ncap
 
Theoremcompleq 3243 Equality law for complement. (Contributed by SF, 11-Jan-2015.)
 
Theoremcompleqi 3244 Equality inference for complement. (Contributed by SF, 11-Jan-2015.)
   =>   
 
Theoremcompleqd 3245 Equality deduction for complement. (Contributed by SF, 11-Jan-2015.)
   =>   
 
Theoremdifeq1 3246 Equality theorem for class difference. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
 
Theoremdifeq2 3247 Equality theorem for class difference. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
 
Theoremsymdifeq1 3248 Equality law for intersection. (Contributed by SF, 11-Jan-2015.)
 
Theoremsymdifeq2 3249 Equality law for intersection. (Contributed by SF, 11-Jan-2015.)
 
Theoremsymdifeq12 3250 Equality law for intersection. (Contributed by SF, 11-Jan-2015.)
 
Theoremsymdifeq1i 3251 Equality inference for symmetric difference. (Contributed by SF, 11-Jan-2015.)
   =>   
 
Theoremsymdifeq2i 3252 Equality inference for symmetric difference. (Contributed by SF, 11-Jan-2015.)
   =>   
 
Theoremsymdifeq12i 3253 Equality inference for symmetric difference. (Contributed by SF, 11-Jan-2015.)
   &       =>   
 
Theoremsymdifeq1d 3254 Equality deduction for symmetric difference. (Contributed by SF, 11-Jan-2015.)
   =>   
 
Theoremsymdifeq2d 3255 Equality deduction for symmetric difference. (Contributed by SF, 11-Jan-2015.)
   =>   
 
Theoremsymdifeq12d 3256 Equality inference for symmetric difference. (Contributed by SF, 11-Jan-2015.)
   &       =>   
 
2.1.11  Subclasses and subsets
 
Syntaxwss 3257 Extend wff notation to include the subclass relation. This is read " is a subclass of " or " includes ." When exists as a set, it is also read " is a subset of ."
 
Syntaxwpss 3258 Extend wff notation with proper subclass relation.
 
Definitiondf-ss 3259 Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example, 1 , 2 1 , 2 , 3 (ex-ss in set.mm). Note that (proved in ssid 3290). Contrast this relationship with the relationship (as will be defined in df-pss 3261). For a more traditional definition, but requiring a dummy variable, see dfss2 3262. Other possible definitions are given by dfss3 3263, dfss4 3489, sspss 3368, ssequn1 3433, ssequn2 3436, sseqin2 3474, and ssdif0 3609. (Contributed by NM, 27-Apr-1994.)
 
Theoremdfss 3260 Variant of subclass definition df-ss 3259. (Contributed by NM, 3-Sep-2004.)
 
Definitiondf-pss 3261 Define proper subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. For example, 1 , 2 1 , 2 , 3 (ex-pss in set.mm). Note that (proved in pssirr 3369). Contrast this relationship with the relationship (as defined in df-ss 3259). Other possible definitions are given by dfpss2 3354 and dfpss3 3355. (Contributed by NM, 7-Feb-1996.)
 
Theoremdfss2 3262* Alternate definition of the subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. (Contributed by NM, 8-Jan-2002.)
 
Theoremdfss3 3263* Alternate definition of subclass relationship. (Contributed by NM, 14-Oct-1999.)
 
Theoremdfss2f 3264 Equivalence for subclass relation, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 3-Jul-1994.) (Revised by Andrew Salmon, 27-Aug-2011.)
 F/_   &     F/_   =>   
 
Theoremdfss3f 3265 Equivalence for subclass relation, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 20-Mar-2004.)
 F/_   &     F/_   =>   
 
Theoremnfss 3266 If is not free in and , it is not free in . (Contributed by NM, 27-Dec-1996.)
 F/_   &     F/_   =>     F/
 
Theoremssel 3267 Membership relationships follow from a subclass relationship. (Contributed by NM, 5-Aug-1993.)
 
Theoremssel2 3268 Membership relationships follow from a subclass relationship. (Contributed by NM, 7-Jun-2004.)
 
Theoremsseli 3269 Membership inference from subclass relationship. (Contributed by NM, 5-Aug-1993.)
   =>   
 
Theoremsselii 3270 Membership inference from subclass relationship. (Contributed by NM, 31-May-1999.)
   &       =>   
 
Theoremsseldi 3271 Membership inference from subclass relationship. (Contributed by NM, 25-Jun-2014.)
   &       =>   
 
Theoremsseld 3272 Membership deduction from subclass relationship. (Contributed by NM, 15-Nov-1995.)
   =>   
 
Theoremsselda 3273 Membership deduction from subclass relationship. (Contributed by NM, 26-Jun-2014.)
   =>   
 
Theoremsseldd 3274 Membership inference from subclass relationship. (Contributed by NM, 14-Dec-2004.)
   &       =>   
 
Theoremssneld 3275 If a class is not in another class, it is also not in a subclass of that class. Deduction form. (Contributed by David Moews, 1-May-2017.)
   =>   
 
Theoremssneldd 3276 If an element is not in a class, it is also not in a subclass of that class. Deduction form. (Contributed by David Moews, 1-May-2017.)
   &       =>   
 
Theoremssriv 3277* Inference rule based on subclass definition. (Contributed by NM, 5-Aug-1993.)
   =>   
 
Theoremssrdv 3278* Deduction rule based on subclass definition. (Contributed by NM, 15-Nov-1995.)
   =>   
 
Theoremsstr2 3279 Transitivity of subclasses. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
 
Theoremsstr 3280 Transitivity of subclasses. Theorem 6 of [Suppes] p. 23. (Contributed by NM, 5-Sep-2003.)
 
Theoremsstri 3281 Subclass transitivity inference. (Contributed by NM, 5-May-2000.)
   &       =>   
 
Theoremsstrd 3282 Subclass transitivity deduction. (Contributed by NM, 2-Jun-2004.)
   &       =>   
 
Theoremsyl5ss 3283 Subclass transitivity deduction. (Contributed by NM, 6-Feb-2014.)
   &       =>   
 
Theoremsyl6ss 3284 Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
   &       =>   
 
Theoremsylan9ss 3285 A subclass transitivity deduction. (Contributed by NM, 27-Sep-2004.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
   &       =>   
 
Theoremsylan9ssr 3286 A subclass transitivity deduction. (Contributed by NM, 27-Sep-2004.)
   &       =>   
 
Theoremeqss 3287 The subclass relationship is antisymmetric. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 5-Aug-1993.)
 
Theoremeqssi 3288 Infer equality from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 9-Sep-1993.)
   &       =>   
 
Theoremeqssd 3289 Equality deduction from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 27-Jun-2004.)
   &       =>   
 
Theoremssid 3290 Any class is a subclass of itself. Exercise 10 of [TakeutiZaring] p. 18. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
 
Theoremssv 3291 Any class is a subclass of the universal class. (Contributed by NM, 31-Oct-1995.)
 
Theoremsseq1 3292 Equality theorem for subclasses. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)
 
Theoremsseq2 3293 Equality theorem for the subclass relationship. (Contributed by NM, 25-Jun-1998.)
 
Theoremsseq12 3294 Equality theorem for the subclass relationship. (Contributed by NM, 31-May-1999.)
 
Theoremsseq1i 3295 An equality inference for the subclass relationship. (Contributed by NM, 18-Aug-1993.)
   =>   
 
Theoremsseq2i 3296 An equality inference for the subclass relationship. (Contributed by NM, 30-Aug-1993.)
   =>   
 
Theoremsseq12i 3297 An equality inference for the subclass relationship. (Contributed by NM, 31-May-1999.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)
   &       =>   
 
Theoremsseq1d 3298 An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.)
   =>   
 
Theoremsseq2d 3299 An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.)
   =>   
 
Theoremsseq12d 3300 An equality deduction for the subclass relationship. (Contributed by NM, 31-May-1999.)
   &       =>   
    < 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 >