HomeHome New Foundations Explorer
Theorem List (p. 44 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 - 4301-4400   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremdfpw12 4301 Alternate expression for unit power classes. (Contributed by SF, 26-Jan-2015.)
1A = ( SIk (A ×k A) “k V)
 
Theorempw1exg 4302 The unit power class preserves sethood. (Contributed by SF, 14-Jan-2015.)
(A V1A V)
 
Theorempw1ex 4303 The unit power class preserves sethood. (Contributed by SF, 14-Jan-2015.)
A V       1A V
 
Theoreminsklem 4304* Lemma for ins2kexg 4305 and ins3kexg 4306. Equality for subsets of (11c ×k (V ×k V)). (Contributed by SF, 14-Jan-2015.)
A (11c ×k (V ×k V))    &   B (11c ×k (V ×k V))       (A = Bxyz(⟪{{x}}, ⟪y, z⟫⟫ A ↔ ⟪{{x}}, ⟪y, z⟫⟫ B))
 
Theoremins2kexg 4305 Ins2k preserves sethood. (Contributed by SF, 14-Jan-2015.)
(A VIns2k A V)
 
Theoremins3kexg 4306 Ins3k preserves sethood. (Contributed by SF, 14-Jan-2015.)
(A VIns3k A V)
 
Theoremins2kex 4307 Ins2k preserves sethood. (Contributed by SF, 14-Jan-2015.)
A V        Ins2k A V
 
Theoremins3kex 4308 Ins3k preserves sethood. (Contributed by SF, 14-Jan-2015.)
A V        Ins3k A V
 
Theoremcokexg 4309 The Kuratowski composition of two sets is a set. (Contributed by SF, 14-Jan-2015.)
((A V B W) → (A k B) V)
 
Theoremcokex 4310 The Kuratowski composition of two sets is a set. (Contributed by SF, 14-Jan-2015.)
A V    &   B V       (A k B) V
 
Theoremimagekexg 4311 The Kuratowski image functor preserves sethood. (Contributed by SF, 14-Jan-2015.)
(A V → ImagekA V)
 
Theoremimagekex 4312 The Kuratowski image functor preserves sethood. (Contributed by SF, 14-Jan-2015.)
A V       ImagekA V
 
Theoremdfidk2 4313 Definition of Ik in terms of Sk. (Contributed by SF, 14-Jan-2015.)
Ik = ( Skk Sk )
 
Theoremidkex 4314 The Kuratowski identity relationship is a set. (Contributed by SF, 14-Jan-2015.)
Ik V
 
Theoremdfuni3 4315 Alternate definition of class union for existence proof. (Contributed by SF, 14-Jan-2015.)
A = ⋃1(k Skk A)
 
Theoremuniexg 4316 The sum class of a set is a set. (Contributed by SF, 14-Jan-2015.)
(A VA V)
 
Theoremuniex 4317 The sum class of a set is a set. (Contributed by SF, 14-Jan-2015.)
A V       A V
 
Theoremdfint3 4318 Alternate definition of class intersection for the existence proof. (Contributed by SF, 14-Jan-2015.)
A = ∼ ⋃1(kSkk A)
 
Theoremintexg 4319 The intersection of a set is a set. (Contributed by SF, 14-Jan-2015.)
(A VA V)
 
Theoremintex 4320 The intersection of a set is a set. (Contributed by SF, 14-Jan-2015.)
A V       A V
 
Theoremsetswith 4321* Two ways to express the class of all sets that contain A. (Contributed by SF, 14-Jan-2015.)
{x A x} = if(A V, ( Skk {{A}}), )
 
Theoremsetswithex 4322* The class of all sets that contain A exist. (Contributed by SF, 14-Jan-2015.)
{x A x} V
 
Theoremndisjrelk 4323 Membership in a particular Kuratowski relationship is equivalent to non-disjointedness. (Contributed by SF, 15-Jan-2015.)
A V    &   B V       (⟪A, B (( Ins3k SkIns2k Sk ) “k 111c) ↔ (AB) ≠ )
 
Theoremabexv 4324* When x does not occur in φ, {x φ} is a set. (Contributed by SF, 17-Jan-2015.)
{x φ} V
 
Theoremunipw1 4325 The union of a unit power class is the original set. (Contributed by SF, 20-Jan-2015.)
1A = A
 
Theorempw1exb 4326 Biconditional existence for unit power class. (Contributed by SF, 20-Jan-2015.)
(1A V ↔ A V)
 
Theoremdfpw2 4327 Definition of power set for existence proof. (Contributed by SF, 21-Jan-2015.)
A = ∼ (( Sk (1A ×k V)) “k 1c)
 
Theorempwexg 4328 The power class of a set is a set. (Contributed by SF, 21-Jan-2015.)
(A VA V)
 
Theorempwex 4329 The power class of a set is a set. (Contributed by SF, 21-Jan-2015.)
A V       A V
 
Theoremeqpw1uni 4330 A class of singletons is equal to the unit power class of its union. (Contributed by SF, 26-Jan-2015.)
(A 1cA = 1A)
 
Theorempw1equn 4331* A condition for a unit power class to equal a union. (Contributed by SF, 26-Jan-2015.)
A V    &   B V       (1C = (AB) ↔ xy(C = (xy) A = 1x B = 1y))
 
Theorempw1eqadj 4332* A condition for a unit power class to work out to an adjunction. (Contributed by SF, 26-Jan-2015.)
A V    &   B V       (1C = (A ∪ {B}) ↔ xy(C = (x ∪ {y}) A = 1x B = {y}))
 
Theoremdfeu2 4333 Alternate definition of existential uniqueness in terms of abstraction. (Contributed by SF, 29-Jan-2015.)
(∃!xφ ↔ {x φ} 1c)
 
Theoremeuabex 4334 If there is a unique object satisfying a property φ, then the set of all elements that satisfy φ exists. (Contributed by SF, 16-Jan-2015.)
(∃!xφ → {x φ} V)
 
Theoremsspw1 4335* A condition for being a subclass of a unit power class. Corollary 2 of theorem IX.6.14 of [Rosser] p. 255. (Contributed by SF, 3-Feb-2015.)
A V       (A 1Bx(x B A = 1x))
 
Theoremsspw12 4336* A set is a subset of cardinal one iff it is the unit power class of some other set. (Contributed by SF, 17-Mar-2015.)
A V       (A 1cx A = 1x)
 
2.2.9  Definite description binder (inverted iota)
 
Syntaxcio 4337 Extend class notation with Russell's definition description binder (inverted iota).
class (℩xφ)
 
Theoremiotajust 4338* Soundness justification theorem for df-iota 4339. (Contributed by Andrew Salmon, 29-Jun-2011.)
{y {x φ} = {y}} = {z {x φ} = {z}}
 
Definitiondf-iota 4339* Define Russell's definition description binder, which can be read as "the unique x such that φ," where φ ordinarily contains x as a free variable. Our definition is meaningful only when there is exactly one x such that φ is true (see iotaval 4350); otherwise, it evaluates to the empty set (see iotanul 4354). Russell used the inverted iota symbol to represent the binder. (Contributed by SF, 12-Jan-2015.)
(℩xφ) = {y {x φ} = {y}}
 
Theoremdfiota2 4340* Alternate definition for descriptions. Definition 8.18 in [Quine] p. 56. (Contributed by Andrew Salmon, 30-Jun-2011.)
(℩xφ) = {y x(φx = y)}
 
Theoremnfiota1 4341 Bound-variable hypothesis builder for the class. (Contributed by Andrew Salmon, 11-Jul-2011.) (Revised by Mario Carneiro, 15-Oct-2016.)
x(℩xφ)
 
Theoremnfiotad 4342 Deduction version of nfiota 4343. (Contributed by NM, 18-Feb-2013.)
yφ    &   (φ → Ⅎxψ)       (φx(℩yψ))
 
Theoremnfiota 4343 Bound-variable hypothesis builder for the class. (Contributed by NM, 23-Aug-2011.)
xφ       x(℩yφ)
 
Theoremcbviota 4344 Change bound variables in a description binder. (Contributed by Andrew Salmon, 1-Aug-2011.)
(x = y → (φψ))    &   yφ    &   xψ       (℩xφ) = (℩yψ)
 
Theoremcbviotav 4345* Change bound variables in a description binder. (Contributed by Andrew Salmon, 1-Aug-2011.)
(x = y → (φψ))       (℩xφ) = (℩yψ)
 
Theoremsb8iota 4346 Variable substitution in description binder. Compare sb8eu 2222. (Contributed by NM, 18-Mar-2013.)
yφ       (℩xφ) = (℩y[y / x]φ)
 
Theoremiotaeq 4347 Equality theorem for descriptions. (Contributed by Andrew Salmon, 30-Jun-2011.)
(x x = y → (℩xφ) = (℩yφ))
 
Theoremiotabi 4348 Equivalence theorem for descriptions. (Contributed by Andrew Salmon, 30-Jun-2011.)
(x(φψ) → (℩xφ) = (℩xψ))
 
Theoremuniabio 4349* Part of Theorem 8.17 in [Quine] p. 56. This theorem serves as a lemma for the fundamental property of iota. (Contributed by Andrew Salmon, 11-Jul-2011.)
(x(φx = y) → {x φ} = y)
 
Theoremiotaval 4350* Theorem 8.19 in [Quine] p. 57. This theorem is the fundamental property of iota. (Contributed by Andrew Salmon, 11-Jul-2011.)
(x(φx = y) → (℩xφ) = y)
 
Theoremiotauni 4351 Equivalence between two different forms of . (Contributed by Andrew Salmon, 12-Jul-2011.)
(∃!xφ → (℩xφ) = {x φ})
 
Theoremiotaint 4352 Equivalence between two different forms of . (Contributed by Mario Carneiro, 24-Dec-2016.)
(∃!xφ → (℩xφ) = {x φ})
 
Theoremiota1 4353 Property of iota. (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 23-Dec-2016.)
(∃!xφ → (φ ↔ (℩xφ) = x))
 
Theoremiotanul 4354 Theorem 8.22 in [Quine] p. 57. This theorem is the result if there isn't exactly one x that satisfies φ. (Contributed by Andrew Salmon, 11-Jul-2011.)
∃!xφ → (℩xφ) = )
 
Theoremiotassuni 4355 The class is a subset of the union of all elements satisfying φ. (Contributed by Mario Carneiro, 24-Dec-2016.)
(℩xφ) {x φ}
 
Theoremiotaex 4356 Theorem 8.23 in [Quine] p. 58. This theorem proves the existence of the class under our definition. (Contributed by Andrew Salmon, 11-Jul-2011.)
(℩xφ) V
 
Theoremiota4 4357 Theorem *14.22 in [WhiteheadRussell] p. 190. (Contributed by Andrew Salmon, 12-Jul-2011.)
(∃!xφ → [̣(℩xφ) / xφ)
 
Theoremiota4an 4358 Theorem *14.23 in [WhiteheadRussell] p. 191. (Contributed by Andrew Salmon, 12-Jul-2011.)
(∃!x(φ ψ) → [̣(℩x(φ ψ)) / xφ)
 
Theoremiota5 4359* A method for computing iota. (Contributed by NM, 17-Sep-2013.)
((φ A V) → (ψx = A))       ((φ A V) → (℩xψ) = A)
 
Theoremiotabidv 4360* Formula-building deduction rule for iota. (Contributed by NM, 20-Aug-2011.)
(φ → (ψχ))       (φ → (℩xψ) = (℩xχ))
 
Theoremiotabii 4361 Formula-building deduction rule for iota. (Contributed by Mario Carneiro, 2-Oct-2015.)
(φψ)       (℩xφ) = (℩xψ)
 
Theoremiotacl 4362 Membership law for descriptions.

This can useful for expanding an unbounded iota-based definition (see df-iota 4339). If you have a bounded iota-based definition, riotacl2 in set.mm may be useful.

(Contributed by Andrew Salmon, 1-Aug-2011.)

(∃!xφ → (℩xφ) {x φ})
 
Theoremreiotacl2 4363 Membership law for descriptions. (Contributed by SF, 21-Aug-2011.)
(∃!x A φ → (℩x(x A φ)) {x A φ})
 
Theoremreiotacl 4364* Membership law for descriptions. (Contributed by SF, 21-Aug-2011.)
(∃!x A φ → (℩x(x A φ)) A)
 
Theoremiota2df 4365 A condition that allows us to represent "the unique element such that φ " with a class expression A. (Contributed by NM, 30-Dec-2014.)
(φB V)    &   (φ∃!xψ)    &   ((φ x = B) → (ψχ))    &   xφ    &   (φ → Ⅎxχ)    &   (φxB)       (φ → (χ ↔ (℩xψ) = B))
 
Theoremiota2d 4366* A condition that allows us to represent "the unique element such that φ " with a class expression A. (Contributed by NM, 30-Dec-2014.)
(φB V)    &   (φ∃!xψ)    &   ((φ x = B) → (ψχ))       (φ → (χ ↔ (℩xψ) = B))
 
Theoremiota2 4367* The unique element such that φ. (Contributed by Jeff Madsen, 1-Jun-2011.) (Revised by Mario Carneiro, 23-Dec-2016.)
(x = A → (φψ))       ((A B ∃!xφ) → (ψ ↔ (℩xφ) = A))
 
Theoremreiota2 4368* A condition allowing us to represent "the unique element in A such that φ " with a class expression B. (Contributed by Scott Fenton, 7-Jan-2018.)
(x = B → (φψ))       ((B A ∃!x A φ) → (ψ ↔ (℩x(x A φ)) = B))
 
Theoremsniota 4369 A class abstraction with a unique member can be expressed as a singleton. (Contributed by Mario Carneiro, 23-Dec-2016.)
(∃!xφ → {x φ} = {(℩xφ)})
 
Theoremdfiota3 4370 The operation using the if operator. (Contributed by Scott Fenton, 6-Oct-2017.)
(℩xφ) = if(∃!xφ, {x φ}, )
 
Theoremcsbiotag 4371* Class substitution within a description binder. (Contributed by Scott Fenton, 6-Oct-2017.)
(A V[A / x](℩yφ) = (℩yA / xφ))
 
Theoremdfiota4 4372 Alternate definition of iota in terms of 1c. (Contributed by SF, 29-Jan-2015.)
(℩xφ) = (1c ∩ {{x φ}})
 
2.2.10  Finite cardinals
 
Syntaxcnnc 4373 Extend the definition of a class to include the set of finite cardinals.
class Nn
 
Syntaxc0c 4374 Extend the definition of a class to include cardinal zero.
class 0c
 
Syntaxcplc 4375 Extend the definition of a class to include cardinal addition.
class (A +c B)
 
Syntaxcfin 4376 Extend the definition of a class to include the set of all finite sets.
class Fin
 
Definitiondf-0c 4377 Define cardinal zero. (Contributed by SF, 12-Jan-2015.)
0c = {}
 
Definitiondf-addc 4378* Define cardinal addition. Definition from [Rosser] p. 275. (Contributed by SF, 12-Jan-2015.)
(A +c B) = {x y A z B ((yz) = x = (yz))}
 
Definitiondf-nnc 4379* Define the finite cardinals. Definition from [Rosser] p. 275. (Contributed by SF, 12-Jan-2015.)
Nn = {b (0c b y b (y +c 1c) b)}
 
Definitiondf-fin 4380 Define the set of all finite sets. Definition from [Rosser], p. 417. (Contributed by SF, 12-Jan-2015.)
Fin = Nn
 
Theoremdfaddc2 4381 Alternate definition of cardinal addition to establish stratification. (Contributed by SF, 15-Jan-2015.)
(A +c B) = ((( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 11B) “k A)
 
Theoremaddcexlem 4382 The expression at the heart of dfaddc2 4381 is a set. (Contributed by SF, 17-Jan-2015.)
( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) V
 
Theoremaddceq1 4383 Equality law for cardinal addition. (Contributed by SF, 15-Jan-2015.)
(A = B → (A +c C) = (B +c C))
 
Theoremaddceq2 4384 Equality law for cardinal addition. (Contributed by SF, 15-Jan-2015.)
(A = B → (C +c A) = (C +c B))
 
Theoremaddceq12 4385 Equality law for cardinal addition. (Contributed by SF, 15-Jan-2015.)
((A = C B = D) → (A +c B) = (C +c D))
 
Theoremaddceq1i 4386 Equality inference for cardinal addition. (Contributed by SF, 3-Feb-2015.)
A = B       (A +c C) = (B +c C)
 
Theoremaddceq2i 4387 Equality inference for cardinal addition. (Contributed by SF, 3-Feb-2015.)
A = B       (C +c A) = (C +c B)
 
Theoremaddceq12i 4388 Equality inference for cardinal addition. (Contributed by SF, 3-Feb-2015.)
A = B    &   C = D       (A +c C) = (B +c D)
 
Theoremaddceq1d 4389 Equality deduction for cardinal addition. (Contributed by SF, 3-Feb-2015.)
(φA = B)       (φ → (A +c C) = (B +c C))
 
Theoremaddceq2d 4390 Equality deduction for cardinal addition. (Contributed by SF, 3-Feb-2015.)
(φA = B)       (φ → (C +c A) = (C +c B))
 
Theoremaddceq12d 4391 Equality deduction for cardinal addition. (Contributed by SF, 3-Feb-2015.)
(φA = B)    &   (φC = D)       (φ → (A +c C) = (B +c D))
 
Theorem0cex 4392 Cardinal zero is a set. (Contributed by SF, 14-Jan-2015.)
0c V
 
Theoremaddcexg 4393 The cardinal sum of two sets is a set. (Contributed by SF, 15-Jan-2015.)
((A V B W) → (A +c B) V)
 
Theoremaddcex 4394 The cardinal sum of two sets is a set. (Contributed by SF, 25-Jan-2015.)
A V    &   B V       (A +c B) V
 
Theoremdfnnc2 4395 Definition of the finite cardinals for existence theorem. (Contributed by SF, 14-Jan-2015.)
Nn = ({x 0c x} (( Sk ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))) “k 1c))
 
Theoremnncex 4396 The class of all finite cardinals is a set. (Contributed by SF, 14-Jan-2015.)
Nn V
 
Theoremfinex 4397 The class of all finite sets is a set. (Contributed by SF, 19-Jan-2015.)
Fin V
 
Theoremeladdc 4398* Membership in cardinal addition. Theorem X.1.1 of [Rosser] p. 275. (Contributed by SF, 16-Jan-2015.)
(A (M +c N) ↔ b M c N ((bc) = A = (bc)))
 
Theoremeladdci 4399 Inference form of membership in cardinal addition. (Contributed by SF, 26-Jan-2015.)
((A M B N (AB) = ) → (AB) (M +c N))
 
Theorem0nelsuc 4400 The empty class is not a member of a successor. (Contributed by SF, 14-Jan-2015.)
¬ (A +c 1c)
    < 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 >