Home New Foundations ExplorerTheorem List (p. 43 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 - 4201-4300   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremxpkeq1i 4201 Equality inference for Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
k k

Theoremxpkeq2i 4202 Equality inference for Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
k k

Theoremxpkeq12i 4203 Equality inference for Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
k k

Theoremxpkeq1d 4204 Equality deduction for Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
k k

Theoremxpkeq2d 4205 Equality deduction for Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
k k

Theoremxpkeq12d 4206 Equality deduction for Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
k k

Theoremelvvk 4207* Membership in k (Contributed by SF, 13-Jan-2015.)
k

Theoremopkabssvvk 4208* Any Kuratowski ordered pair abstraction is a subset of k . (Contributed by SF, 13-Jan-2015.)
k

Theoremopkabssvvki 4209* Any Kuratowski ordered pair abstraction is a subset of k . (Contributed by SF, 13-Jan-2015.)
k

Theoremxpkssvvk 4210 Any Kuratowski cross product is a subset of k . (Contributed by SF, 13-Jan-2015.)
k k

Theoremssrelk 4211* Subset for Kuratowski relationships. (Contributed by SF, 13-Jan-2015.)
k

Theoremeqrelk 4212* Equality for two Kuratowski relationships. (Contributed by SF, 13-Jan-2015.)
k k

Theoremeqrelkriiv 4213* Equality for two Kuratowski relationships. (Contributed by SF, 13-Jan-2015.)
k        k

Theoremeqrelkrdv 4214* Equality for two Kuratowski relationships. (Contributed by SF, 13-Jan-2015.)
k        k

Theoremcnvkeq 4215 Equality theorem for Kuratowski converse. (Contributed by SF, 12-Jan-2015.)
k k

Theoremcnvkeqi 4216 Equality inference for Kuratowski converse. (Contributed by SF, 12-Jan-2015.)
k k

Theoremcnvkeqd 4217 Equality deduction for Kuratowski converse. (Contributed by SF, 12-Jan-2015.)
k k

Theoremins2keq 4218 Equality theorem for the Kuratowski insert two operator. (Contributed by SF, 12-Jan-2015.)
Ins2k Ins2k

Theoremins3keq 4219 Equality theorem for the Kuratowski insert three operator. (Contributed by SF, 12-Jan-2015.)
Ins3k Ins3k

Theoremins2keqi 4220 Equality inference for Kuratowski insert two operator. (Contributed by SF, 12-Jan-2015.)
Ins2k Ins2k

Theoremins3keqi 4221 Equality inference for Kuratowski insert three operator. (Contributed by SF, 12-Jan-2015.)
Ins3k Ins3k

Theoremins2keqd 4222 Equality deduction for Kuratowski insert two operator. (Contributed by SF, 12-Jan-2015.)
Ins2k Ins2k

Theoremins3keqd 4223 Equality deduction for Kuratowski insert three operator. (Contributed by SF, 12-Jan-2015.)
Ins3k Ins3k

Theoremimakeq1 4224 Equality theorem for Kuratowski image. (Contributed by SF, 12-Jan-2015.)
k k

Theoremimakeq2 4225 Equality theorem for Kuratowski image. (Contributed by SF, 12-Jan-2015.)
k k

Theoremimakeq1i 4226 Equality theorem for image. (Contributed by SF, 12-Jan-2015.)
k k

Theoremimakeq2i 4227 Equality theorem for Kuratowski image. (Contributed by SF, 12-Jan-2015.)
k k

Theoremimakeq1d 4228 Equality theorem for Kuratowski image. (Contributed by SF, 12-Jan-2015.)
k k

Theoremimakeq2d 4229 Equality theorem for Kuratowski image. (Contributed by SF, 12-Jan-2015.)
k k

Theoremcokeq1 4230 Equality theorem for Kuratowski composition of two classes. (Contributed by SF, 12-Jan-2015.)
k k

Theoremcokeq2 4231 Equality theorem for Kuratowski composition of two classes. (Contributed by SF, 12-Jan-2015.)
k k

Theoremcokeq1i 4232 Equality inference for Kuratowski composition of two classes. (Contributed by SF, 12-Jan-2015.)
k k

Theoremcokeq2i 4233 Equality inference for Kuratowski composition of two classes. (Contributed by SF, 12-Jan-2015.)
k k

Theoremcokeq1d 4234 Equality deduction for Kuratowski composition of two classes. (Contributed by SF, 12-Jan-2015.)
k k

Theoremcokeq2d 4235 Equality deduction for Kuratowski composition of two classes. (Contributed by SF, 12-Jan-2015.)
k k

Theoremcokeq12i 4236 Equality inference for Kuratowski composition of two classes. (Contributed by SF, 12-Jan-2015.)
k k

Theoremcokeq12d 4237 Equality deduction for Kuratowski composition of two classes. (Contributed by SF, 12-Jan-2015.)
k k

Theoremp6eq 4238 Equality theorem for P6 operation. (Contributed by SF, 12-Jan-2015.)
P6 P6

Theoremp6eqi 4239 Equality inference for the P6 operation. (Contributed by SF, 12-Jan-2015.)
P6 P6

Theoremp6eqd 4240 Equality deduction for the P6 operation. (Contributed by SF, 12-Jan-2015.)
P6 P6

Theoremsikeq 4241 Equality theorem for Kuratowski singleton image. (Contributed by SF, 12-Jan-2015.)
SIk SIk

Theoremsikeqi 4242 Equality inference for Kuratowski singleton image. (Contributed by SF, 12-Jan-2015.)
SIk SIk

Theoremsikeqd 4243 Equality deduction for Kuratowski singleton image. (Contributed by SF, 12-Jan-2015.)
SIk SIk

Theoremimagekeq 4244 Equality theorem for image operation. (Contributed by SF, 12-Jan-2015.)
Imagek Imagek

Theoremopkelopkabg 4245* Kuratowski ordered pair membership in an abstraction of Kuratowski ordered pairs. (Contributed by SF, 12-Jan-2015.)

Theoremopkelopkab 4246* Kuratowski ordered pair membership in an abstraction of Kuratowski ordered pairs. (Contributed by SF, 12-Jan-2015.)

Theoremopkelxpkg 4247 Kuratowski ordered pair membership in a Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
k

Theoremopkelxpk 4248 Kuratowski ordered pair membership in a Kuratowski cross product. (Contributed by SF, 13-Jan-2015.)
k

Theoremopkelcnvkg 4249 Kuratowski ordered pair membership in a Kuratowski converse. (Contributed by SF, 12-Jan-2015.)
k

Theoremopkelcnvk 4250 Kuratowski ordered pair membership in a Kuratowski converse. (Contributed by SF, 14-Jan-2015.)
k

Theoremopkelins2kg 4251* Kuratowski ordered pair membership in Kuratowski insertion operator. (Contributed by SF, 12-Jan-2015.)
Ins2k

Theoremopkelins3kg 4252* Kuratowski ordered pair membership in Kuratowski insertion operator. (Contributed by SF, 12-Jan-2015.)
Ins3k

Theoremotkelins2kg 4253 Kuratowski ordered triple membership in Kuratowski insertion operator. (Contributed by SF, 12-Jan-2015.)
Ins2k

Theoremotkelins3kg 4254 Kuratowski ordered triple membership in Kuratowski insertion operator. (Contributed by SF, 12-Jan-2015.)
Ins3k

Theoremotkelins2k 4255 Kuratowski ordered triple membership in Kuratowski insertion operator. (Contributed by SF, 12-Jan-2015.)
Ins2k

Theoremotkelins3k 4256 Kuratowski ordered triple membership in Kuratowski insertion operator. (Contributed by SF, 12-Jan-2015.)
Ins3k

Theoremelimakg 4257* Membership in a Kuratowski image. (Contributed by SF, 13-Jan-2015.)
k

Theoremelimakvg 4258* Membership in a Kuratowski image under . (Contributed by SF, 13-Jan-2015.)
k

Theoremelimak 4259* Membership in a Kuratowski image. (Contributed by SF, 13-Jan-2015.)
k

Theoremelimakv 4260* Membership in a Kuratowski image under . (Contributed by SF, 13-Jan-2015.)
k

Theoremopkelcokg 4261* Membership in a Kuratowski composition. (Contributed by SF, 13-Jan-2015.)
k

Theoremopkelcok 4262* Membership in a Kuratowski composition. (Contributed by SF, 13-Jan-2015.)
k

Theoremelp6 4263* Membership in the P6 operator. (Contributed by SF, 13-Jan-2015.)
P6

Theoremopkelsikg 4264* Membership in Kuratowski singleton image. (Contributed by SF, 13-Jan-2015.)
SIk

Theoremopksnelsik 4265 Membership of an ordered pair of singletons in a Kuratowski singleton image. (Contributed by SF, 13-Jan-2015.)
SIk

Theoremsikssvvk 4266 A Kuratowski singleton image is a Kuratowski relationship. (Contributed by SF, 13-Jan-2015.)
SIk k

Theoremsikss1c1c 4267 A Kuratowski singleton image is a subset of 1c k 1c. (Contributed by SF, 13-Jan-2015.)
SIk 1c k 1c

Theoremopkelssetkg 4268 Membership in the Kuratowski subset relationship. (Contributed by SF, 13-Jan-2015.)
Sk

Theoremelssetkg 4269 Membership via the Kuratowski subset relationship. (Contributed by SF, 13-Jan-2015.)
Sk

Theoremelssetk 4270 Membership via the Kuratowski subset relationship. (Contributed by SF, 13-Jan-2015.)
Sk

Theoremopkelimagekg 4271 Membership in the Kuratowski image functor. (Contributed by SF, 13-Jan-2015.)
Imagek k

Theoremopkelimagek 4272 Membership in the Kuratowski image functor. (Contributed by SF, 20-Jan-2015.)
Imagek k

Theoremimagekrelk 4273 The Kuratowski image functor is a relationship. (Contributed by SF, 14-Jan-2015.)
Imagek k

Theoremopkelidkg 4274 Membership in the Kuratowski identity relationship. (Contributed by SF, 13-Jan-2015.)
k

Theoremcnvkssvvk 4275 A Kuratowski converse is a Kuratowski relationship. (Contributed by SF, 13-Jan-2015.)
k k

Theoremcnvkxpk 4276 The converse of a Kuratowski cross product. (Contributed by SF, 13-Jan-2015.)
k k k

Theoreminxpk 4277 The intersection of two Kuratowski cross products. (Contributed by SF, 13-Jan-2015.)
k k k

Theoremssetkssvvk 4278 The Kuratowski subset relationship is a Kuratowski relationship. (Contributed by SF, 13-Jan-2015.)
Sk k

Theoremins2kss 4279 Subset law for Ins2k . (Contributed by SF, 14-Jan-2015.)
Ins2k 1 1c k k

Theoremins3kss 4280 Subset law for Ins3k . (Contributed by SF, 14-Jan-2015.)
Ins3k 1 1c k k

Theoremidkssvvk 4281 The Kuratowski identity relationship is a Kuratowski relationship. (Contributed by SF, 14-Jan-2015.)
k k

Theoremimacok 4282 Image under a composition. (Contributed by SF, 4-Feb-2015.)
k k kk

Theoremelimaksn 4283 Membership in a Kuratowski image of a singleton. (Contributed by SF, 4-Feb-2015.)
k

Theoremcokrelk 4284 A Kuratowski composition is a Kuratowski relationship. (Contributed by SF, 4-Feb-2015.)
k k

2.2.8  Kuratowski existence theorems

Theoremxpkvexg 4285 The Kuratowski cross product of with a set is a set. (Contributed by SF, 13-Jan-2015.)
k

Theoremcnvkexg 4286 The Kuratowski converse of a set is a set. (Contributed by SF, 13-Jan-2015.)
k

Theoremcnvkex 4287 The Kuratowski converse of a set is a set. (Contributed by SF, 14-Jan-2015.)
k

Theoremxpkexg 4288 The Kuratowski cross product of two sets is a set. (Contributed by SF, 13-Jan-2015.)
k

Theoremxpkex 4289 The Kuratowski cross product of two sets is a set. (Contributed by SF, 14-Jan-2015.)
k

Theoremp6exg 4290 The P6 operator applied to a set yields a set. (Contributed by SF, 13-Jan-2015.)
P6

Theoremdfuni12 4291 Alternate definition of unit union. (Contributed by SF, 15-Mar-2015.)
1 P6 k

Theoremuni1exg 4292 The unit union operator preserves sethood. (Contributed by SF, 13-Jan-2015.)
1

Theoremuni1ex 4293 The unit union operator preserves sethood. (Contributed by SF, 14-Jan-2015.)
1

Theoremssetkex 4294 The Kuratowski subset relationship is a set. (Contributed by SF, 13-Jan-2015.)
Sk

Theoremsikexlem 4295* Lemma for sikexg 4296. Equality for two subsets of 1c squared . (Contributed by SF, 14-Jan-2015.)
1c k 1c       1c k 1c

Theoremsikexg 4296 The Kuratowski singleton image of a set is a set. (Contributed by SF, 14-Jan-2015.)
SIk

Theoremsikex 4297 The Kuratowski singleton image of a set is a set. (Contributed by SF, 14-Jan-2015.)
SIk

Theoremdfimak2 4298 Alternate definition of Kuratowski image. This is the first of a series of definitions throughout the file designed to prove existence of various operations. (Contributed by SF, 14-Jan-2015.)
k P6 1c k SIk k

Theoremimakexg 4299 The image of a set under a set is a set. (Contributed by SF, 14-Jan-2015.)
k

Theoremimakex 4300 The image of a set under a set is a set. (Contributed by SF, 14-Jan-2015.)
k

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 >