HomeHome New Foundations Explorer
Theorem List (p. 33 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 - 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.)
yA    &   xB    &   yφ    &   xψ    &   (x = yA = B)    &   (x = y → (φψ))       {x A φ} = {y B ψ}
 
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.)
(x = y → (ψχ))    &   (x = yA = B)       (x A ψy B χ)
 
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.)
(x = y → (ψχ))    &   (x = yA = B)       (x A ψy B χ)
 
2.1.10  Define boolean set operations
 
Syntaxcnin 3204 Extend class notation to include anti-intersection (read: "the anti-intersection of A and B").
class (AB)
 
Syntaxccompl 3205 Extend class notation to include complement. (read: "the complement of A " ).
class A
 
Syntaxcdif 3206 Extend class notation to include class difference (read: "A minus B").
class (A B)
 
Syntaxcun 3207 Extend class notation to include union of two classes (read: "A union B").
class (AB)
 
Syntaxcin 3208 Extend class notation to include the intersection of two classes (read: "A intersect B").
class (AB)
 
Syntaxcsymdif 3209 Extend class notation to include the symmetric difference of two classes.
class (AB)
 
Theoremninjust 3210* Soundness theorem for df-nin 3211. (Contributed by SF, 10-Jan-2015.)
{x (x A x B)} = {y (y A y B)}
 
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.)
(AB) = {x (x A x B)}
 
Definitiondf-compl 3212 Define the complement of a class. Compare nic-dfneg 1435. (Contributed by SF, 10-Jan-2015.)
A = (AA)
 
Definitiondf-in 3213 Define the intersection of two classes. See elin 3219 for membership. (Contributed by SF, 10-Jan-2015.)
(AB) = ∼ (AB)
 
Definitiondf-un 3214 Define the union of two classes. See elun 3220 for membership. (Contributed by SF, 10-Jan-2015.)
(AB) = ( ∼ A ⩃ ∼ B)
 
Definitiondf-dif 3215 Define the difference of two classes. See eldif 3221 for membership. (Contributed by SF, 10-Jan-2015.)
(A B) = (A ∩ ∼ B)
 
Definitiondf-symdif 3216 Define the symmetric difference of two classes. Definition IX.9.10, [Rosser] p. 238. (Contributed by SF, 10-Jan-2015.)
(AB) = ((A B) ∪ (B A))
 
Theoremelning 3217 Membership in anti-intersection. (Contributed by SF, 10-Jan-2015.)
(A V → (A (BC) ↔ (A B A C)))
 
Theoremelcomplg 3218 Membership in class complement. (Contributed by SF, 10-Jan-2015.)
(A V → (A B ↔ ¬ A B))
 
Theoremelin 3219 Membership in intersection. (Contributed by SF, 10-Jan-2015.)
(A (BC) ↔ (A B A C))
 
Theoremelun 3220 Membership in union. (Contributed by SF, 10-Jan-2015.)
(A (BC) ↔ (A B A C))
 
Theoremeldif 3221 Membership in difference. (Contributed by SF, 10-Jan-2015.)
(A (B C) ↔ (A B ¬ A C))
 
Theoremdfdif2 3222* Alternate definition of class difference. (Contributed by NM, 25-Mar-2004.)
(A B) = {x A ¬ x B}
 
Theoremelsymdif 3223 Membership in symmetric difference. (Contributed by SF, 10-Jan-2015.)
(A (BC) ↔ ¬ (A BA C))
 
Theoremelnin 3224 Membership in anti-intersection. (Contributed by SF, 10-Jan-2015.)
A V       (A (BC) ↔ (A B A C))
 
Theoremelcompl 3225 Membership in complement. (Contributed by SF, 10-Jan-2015.)
A V       (A B ↔ ¬ A B)
 
Theoremnincom 3226 Anti-intersection commutes. (Contributed by SF, 10-Jan-2015.)
(AB) = (BA)
 
Theoremdblcompl 3227 Double complement law. (Contributed by SF, 10-Jan-2015.)
∼ ∼ A = A
 
Theoremnfnin 3228 Hypothesis builder for anti-intersection. (Contributed by SF, 2-Jan-2018.)
xA    &   xB       x(AB)
 
Theoremnfcompl 3229 Hypothesis builder for complement. (Contributed by SF, 2-Jan-2018.)
xA       xA
 
Theoremnfin 3230 Hypothesis builder for intersection. (Contributed by SF, 2-Jan-2018.)
xA    &   xB       x(AB)
 
Theoremnfun 3231 Hypothesis builder for union. (Contributed by SF, 2-Jan-2018.)
xA    &   xB       x(AB)
 
Theoremnfdif 3232 Hypothesis builder for difference. (Contributed by SF, 2-Jan-2018.)
xA    &   xB       x(A B)
 
Theoremnfsymdif 3233 Hypothesis builder for symmetric difference. (Contributed by SF, 2-Jan-2018.)
xA    &   xB       x(AB)
 
Theoremnineq1 3234 Equality law for anti-intersection. (Contributed by SF, 11-Jan-2015.)
(A = B → (AC) = (BC))
 
Theoremnineq2 3235 Equality law for anti-intersection. (Contributed by SF, 11-Jan-2015.)
(A = B → (CA) = (CB))
 
Theoremnineq12 3236 Equality law for anti-intersection. (Contributed by SF, 11-Jan-2015.)
((A = B C = D) → (AC) = (BD))
 
Theoremnineq1i 3237 Equality inference for anti-intersection. (Contributed by SF, 11-Jan-2015.)
A = B       (AC) = (BC)
 
Theoremnineq2i 3238 Equality inference for anti-intersection. (Contributed by SF, 11-Jan-2015.)
A = B       (CA) = (CB)
 
Theoremnineq12i 3239 Equality inference for anti-intersection. (Contributed by SF, 11-Jan-2015.)
A = B    &   C = D       (AC) = (BD)
 
Theoremnineq1d 3240 Equality deduction for anti-intersection. (Contributed by SF, 11-Jan-2015.)
(φA = B)       (φ → (AC) = (BC))
 
Theoremnineq2d 3241 Equality deduction for anti-intersection. (Contributed by SF, 11-Jan-2015.)
(φA = B)       (φ → (CA) = (CB))
 
Theoremnineq12d 3242 Equality inference for anti-intersection. (Contributed by SF, 11-Jan-2015.)
(φA = B)    &   (φC = D)       (φ → (AC) = (BD))
 
Theoremcompleq 3243 Equality law for complement. (Contributed by SF, 11-Jan-2015.)
(A = B → ∼ A = ∼ B)
 
Theoremcompleqi 3244 Equality inference for complement. (Contributed by SF, 11-Jan-2015.)
A = B       A = ∼ B
 
Theoremcompleqd 3245 Equality deduction for complement. (Contributed by SF, 11-Jan-2015.)
(φA = B)       (φ → ∼ A = ∼ B)
 
Theoremdifeq1 3246 Equality theorem for class difference. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
(A = B → (A C) = (B C))
 
Theoremdifeq2 3247 Equality theorem for class difference. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
(A = B → (C A) = (C B))
 
Theoremsymdifeq1 3248 Equality law for intersection. (Contributed by SF, 11-Jan-2015.)
(A = B → (AC) = (BC))
 
Theoremsymdifeq2 3249 Equality law for intersection. (Contributed by SF, 11-Jan-2015.)
(A = B → (CA) = (CB))
 
Theoremsymdifeq12 3250 Equality law for intersection. (Contributed by SF, 11-Jan-2015.)
((A = B C = D) → (AC) = (BD))
 
Theoremsymdifeq1i 3251 Equality inference for symmetric difference. (Contributed by SF, 11-Jan-2015.)
A = B       (AC) = (BC)
 
Theoremsymdifeq2i 3252 Equality inference for symmetric difference. (Contributed by SF, 11-Jan-2015.)
A = B       (CA) = (CB)
 
Theoremsymdifeq12i 3253 Equality inference for symmetric difference. (Contributed by SF, 11-Jan-2015.)
A = B    &   C = D       (AC) = (BD)
 
Theoremsymdifeq1d 3254 Equality deduction for symmetric difference. (Contributed by SF, 11-Jan-2015.)
(φA = B)       (φ → (AC) = (BC))
 
Theoremsymdifeq2d 3255 Equality deduction for symmetric difference. (Contributed by SF, 11-Jan-2015.)
(φA = B)       (φ → (CA) = (CB))
 
Theoremsymdifeq12d 3256 Equality inference for symmetric difference. (Contributed by SF, 11-Jan-2015.)
(φA = B)    &   (φC = D)       (φ → (AC) = (BD))
 
2.1.11  Subclasses and subsets
 
Syntaxwss 3257 Extend wff notation to include the subclass relation. This is read "A is a subclass of B " or "B includes A." When A exists as a set, it is also read "A is a subset of B."
wff A B
 
Syntaxwpss 3258 Extend wff notation with proper subclass relation.
wff AB
 
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 A A (proved in ssid 3290). Contrast this relationship with the relationship AB (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.)
(A B ↔ (AB) = A)
 
Theoremdfss 3260 Variant of subclass definition df-ss 3259. (Contributed by NM, 3-Sep-2004.)
(A BA = (AB))
 
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 ¬ AA (proved in pssirr 3369). Contrast this relationship with the relationship A B (as defined in df-ss 3259). Other possible definitions are given by dfpss2 3354 and dfpss3 3355. (Contributed by NM, 7-Feb-1996.)
(AB ↔ (A B AB))
 
Theoremdfss2 3262* Alternate definition of the subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. (Contributed by NM, 8-Jan-2002.)
(A Bx(x Ax B))
 
Theoremdfss3 3263* Alternate definition of subclass relationship. (Contributed by NM, 14-Oct-1999.)
(A Bx A x B)
 
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.)
xA    &   xB       (A Bx(x Ax B))
 
Theoremdfss3f 3265 Equivalence for subclass relation, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 20-Mar-2004.)
xA    &   xB       (A Bx A x B)
 
Theoremnfss 3266 If x is not free in A and B, it is not free in A B. (Contributed by NM, 27-Dec-1996.)
xA    &   xB       x A B
 
Theoremssel 3267 Membership relationships follow from a subclass relationship. (Contributed by NM, 5-Aug-1993.)
(A B → (C AC B))
 
Theoremssel2 3268 Membership relationships follow from a subclass relationship. (Contributed by NM, 7-Jun-2004.)
((A B C A) → C B)
 
Theoremsseli 3269 Membership inference from subclass relationship. (Contributed by NM, 5-Aug-1993.)
A B       (C AC B)
 
Theoremsselii 3270 Membership inference from subclass relationship. (Contributed by NM, 31-May-1999.)
A B    &   C A       C B
 
Theoremsseldi 3271 Membership inference from subclass relationship. (Contributed by NM, 25-Jun-2014.)
A B    &   (φC A)       (φC B)
 
Theoremsseld 3272 Membership deduction from subclass relationship. (Contributed by NM, 15-Nov-1995.)
(φA B)       (φ → (C AC B))
 
Theoremsselda 3273 Membership deduction from subclass relationship. (Contributed by NM, 26-Jun-2014.)
(φA B)       ((φ C A) → C B)
 
Theoremsseldd 3274 Membership inference from subclass relationship. (Contributed by NM, 14-Dec-2004.)
(φA B)    &   (φC A)       (φC B)
 
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.)
(φA B)       (φ → (¬ C B → ¬ C A))
 
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.)
(φA B)    &   (φ → ¬ C B)       (φ → ¬ C A)
 
Theoremssriv 3277* Inference rule based on subclass definition. (Contributed by NM, 5-Aug-1993.)
(x Ax B)       A B
 
Theoremssrdv 3278* Deduction rule based on subclass definition. (Contributed by NM, 15-Nov-1995.)
(φ → (x Ax B))       (φA B)
 
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.)
(A B → (B CA C))
 
Theoremsstr 3280 Transitivity of subclasses. Theorem 6 of [Suppes] p. 23. (Contributed by NM, 5-Sep-2003.)
((A B B C) → A C)
 
Theoremsstri 3281 Subclass transitivity inference. (Contributed by NM, 5-May-2000.)
A B    &   B C       A C
 
Theoremsstrd 3282 Subclass transitivity deduction. (Contributed by NM, 2-Jun-2004.)
(φA B)    &   (φB C)       (φA C)
 
Theoremsyl5ss 3283 Subclass transitivity deduction. (Contributed by NM, 6-Feb-2014.)
A B    &   (φB C)       (φA C)
 
Theoremsyl6ss 3284 Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
(φA B)    &   B C       (φA C)
 
Theoremsylan9ss 3285 A subclass transitivity deduction. (Contributed by NM, 27-Sep-2004.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
(φA B)    &   (ψB C)       ((φ ψ) → A C)
 
Theoremsylan9ssr 3286 A subclass transitivity deduction. (Contributed by NM, 27-Sep-2004.)
(φA B)    &   (ψB C)       ((ψ φ) → A C)
 
Theoremeqss 3287 The subclass relationship is antisymmetric. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 5-Aug-1993.)
(A = B ↔ (A B B A))
 
Theoremeqssi 3288 Infer equality from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 9-Sep-1993.)
A B    &   B A       A = B
 
Theoremeqssd 3289 Equality deduction from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 27-Jun-2004.)
(φA B)    &   (φB A)       (φA = B)
 
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.)
A A
 
Theoremssv 3291 Any class is a subclass of the universal class. (Contributed by NM, 31-Oct-1995.)
A V
 
Theoremsseq1 3292 Equality theorem for subclasses. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)
(A = B → (A CB C))
 
Theoremsseq2 3293 Equality theorem for the subclass relationship. (Contributed by NM, 25-Jun-1998.)
(A = B → (C AC B))
 
Theoremsseq12 3294 Equality theorem for the subclass relationship. (Contributed by NM, 31-May-1999.)
((A = B C = D) → (A CB D))
 
Theoremsseq1i 3295 An equality inference for the subclass relationship. (Contributed by NM, 18-Aug-1993.)
A = B       (A CB C)
 
Theoremsseq2i 3296 An equality inference for the subclass relationship. (Contributed by NM, 30-Aug-1993.)
A = B       (C AC B)
 
Theoremsseq12i 3297 An equality inference for the subclass relationship. (Contributed by NM, 31-May-1999.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)
A = B    &   C = D       (A CB D)
 
Theoremsseq1d 3298 An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.)
(φA = B)       (φ → (A CB C))
 
Theoremsseq2d 3299 An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.)
(φA = B)       (φ → (C AC B))
 
Theoremsseq12d 3300 An equality deduction for the subclass relationship. (Contributed by NM, 31-May-1999.)
(φA = B)    &   (φC = D)       (φ → (A CB D))
    < 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-6336
  Copyright terms: Public domain < Previous  Next >