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

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