Home New Foundations ExplorerTheorem 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.)

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.)
&ncap

Theoremnfcompl 3229 Hypothesis builder for complement. (Contributed by SF, 2-Jan-2018.)

Theoremnfin 3230 Hypothesis builder for intersection. (Contributed by SF, 2-Jan-2018.)

Theoremnfun 3231 Hypothesis builder for union. (Contributed by SF, 2-Jan-2018.)

Theoremnfdif 3232 Hypothesis builder for difference. (Contributed by SF, 2-Jan-2018.)

Theoremnfsymdif 3233 Hypothesis builder for symmetric difference. (Contributed by SF, 2-Jan-2018.)

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

Theoremdfss3f 3265 Equivalence for subclass relation, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 20-Mar-2004.)

Theoremnfss 3266 If is not free in and , it is not free in . (Contributed by NM, 27-Dec-1996.)

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

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 >