HomeHome New Foundations Explorer
Theorem List (p. 43 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 - 4201-4300   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremxpkeq1i 4201 Equality inference for Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
A = B       (A ×k C) = (B ×k C)
 
Theoremxpkeq2i 4202 Equality inference for Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
A = B       (C ×k A) = (C ×k B)
 
Theoremxpkeq12i 4203 Equality inference for Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
A = B    &   C = D       (A ×k C) = (B ×k D)
 
Theoremxpkeq1d 4204 Equality deduction for Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
(φA = B)       (φ → (A ×k C) = (B ×k C))
 
Theoremxpkeq2d 4205 Equality deduction for Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
(φA = B)       (φ → (C ×k A) = (C ×k B))
 
Theoremxpkeq12d 4206 Equality deduction for Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
(φA = B)    &   (φC = D)       (φ → (A ×k C) = (B ×k D))
 
Theoremelvvk 4207* Membership in (V ×k V) (Contributed by SF, 13-Jan-2015.)
(A (V ×k V) ↔ xy A = ⟪x, y⟫)
 
Theoremopkabssvvk 4208* Any Kuratowski ordered pair abstraction is a subset of (V ×k V). (Contributed by SF, 13-Jan-2015.)
{x yz(x = ⟪y, z φ)} (V ×k V)
 
Theoremopkabssvvki 4209* Any Kuratowski ordered pair abstraction is a subset of (V ×k V). (Contributed by SF, 13-Jan-2015.)
A = {x yz(x = ⟪y, z φ)}       A (V ×k V)
 
Theoremxpkssvvk 4210 Any Kuratowski cross product is a subset of (V ×k V). (Contributed by SF, 13-Jan-2015.)
(A ×k B) (V ×k V)
 
Theoremssrelk 4211* Subset for Kuratowski relationships. (Contributed by SF, 13-Jan-2015.)
(A (V ×k V) → (A Bxy(⟪x, y A → ⟪x, y B)))
 
Theoremeqrelk 4212* Equality for two Kuratowski relationships. (Contributed by SF, 13-Jan-2015.)
((A (V ×k V) B (V ×k V)) → (A = Bxy(⟪x, y A ↔ ⟪x, y B)))
 
Theoremeqrelkriiv 4213* Equality for two Kuratowski relationships. (Contributed by SF, 13-Jan-2015.)
A (V ×k V)    &   B (V ×k V)    &   (⟪x, y A ↔ ⟪x, y B)       A = B
 
Theoremeqrelkrdv 4214* Equality for two Kuratowski relationships. (Contributed by SF, 13-Jan-2015.)
A (V ×k V)    &   B (V ×k V)    &   (φ → (⟪x, y A ↔ ⟪x, y B))       (φA = B)
 
Theoremcnvkeq 4215 Equality theorem for Kuratowski converse. (Contributed by SF, 12-Jan-2015.)
(A = BkA = kB)
 
Theoremcnvkeqi 4216 Equality inference for Kuratowski converse. (Contributed by SF, 12-Jan-2015.)
A = B       kA = kB
 
Theoremcnvkeqd 4217 Equality deduction for Kuratowski converse. (Contributed by SF, 12-Jan-2015.)
(φA = B)       (φkA = kB)
 
Theoremins2keq 4218 Equality theorem for the Kuratowski insert two operator. (Contributed by SF, 12-Jan-2015.)
(A = BIns2k A = Ins2k B)
 
Theoremins3keq 4219 Equality theorem for the Kuratowski insert three operator. (Contributed by SF, 12-Jan-2015.)
(A = BIns3k A = Ins3k B)
 
Theoremins2keqi 4220 Equality inference for Kuratowski insert two operator. (Contributed by SF, 12-Jan-2015.)
A = B        Ins2k A = Ins2k B
 
Theoremins3keqi 4221 Equality inference for Kuratowski insert three operator. (Contributed by SF, 12-Jan-2015.)
A = B        Ins3k A = Ins3k B
 
Theoremins2keqd 4222 Equality deduction for Kuratowski insert two operator. (Contributed by SF, 12-Jan-2015.)
(φA = B)       (φIns2k A = Ins2k B)
 
Theoremins3keqd 4223 Equality deduction for Kuratowski insert three operator. (Contributed by SF, 12-Jan-2015.)
(φA = B)       (φIns3k A = Ins3k B)
 
Theoremimakeq1 4224 Equality theorem for Kuratowski image. (Contributed by SF, 12-Jan-2015.)
(A = B → (Ak C) = (Bk C))
 
Theoremimakeq2 4225 Equality theorem for Kuratowski image. (Contributed by SF, 12-Jan-2015.)
(A = B → (Ck A) = (Ck B))
 
Theoremimakeq1i 4226 Equality theorem for image. (Contributed by SF, 12-Jan-2015.)
A = B       (Ak C) = (Bk C)
 
Theoremimakeq2i 4227 Equality theorem for Kuratowski image. (Contributed by SF, 12-Jan-2015.)
A = B       (Ck A) = (Ck B)
 
Theoremimakeq1d 4228 Equality theorem for Kuratowski image. (Contributed by SF, 12-Jan-2015.)
(φA = B)       (φ → (Ak C) = (Bk C))
 
Theoremimakeq2d 4229 Equality theorem for Kuratowski image. (Contributed by SF, 12-Jan-2015.)
(φA = B)       (φ → (Ck A) = (Ck B))
 
Theoremcokeq1 4230 Equality theorem for Kuratowski composition of two classes. (Contributed by SF, 12-Jan-2015.)
(A = B → (A k C) = (B k C))
 
Theoremcokeq2 4231 Equality theorem for Kuratowski composition of two classes. (Contributed by SF, 12-Jan-2015.)
(A = B → (C k A) = (C k B))
 
Theoremcokeq1i 4232 Equality inference for Kuratowski composition of two classes. (Contributed by SF, 12-Jan-2015.)
A = B       (A k C) = (B k C)
 
Theoremcokeq2i 4233 Equality inference for Kuratowski composition of two classes. (Contributed by SF, 12-Jan-2015.)
A = B       (C k A) = (C k B)
 
Theoremcokeq1d 4234 Equality deduction for Kuratowski composition of two classes. (Contributed by SF, 12-Jan-2015.)
(φA = B)       (φ → (A k C) = (B k C))
 
Theoremcokeq2d 4235 Equality deduction for Kuratowski composition of two classes. (Contributed by SF, 12-Jan-2015.)
(φA = B)       (φ → (C k A) = (C k B))
 
Theoremcokeq12i 4236 Equality inference for Kuratowski composition of two classes. (Contributed by SF, 12-Jan-2015.)
A = B    &   C = D       (A k C) = (B k D)
 
Theoremcokeq12d 4237 Equality deduction for Kuratowski composition of two classes. (Contributed by SF, 12-Jan-2015.)
(φA = B)    &   (φC = D)       (φ → (A k C) = (B k D))
 
Theoremp6eq 4238 Equality theorem for P6 operation. (Contributed by SF, 12-Jan-2015.)
(A = BP6 A = P6 B)
 
Theoremp6eqi 4239 Equality inference for the P6 operation. (Contributed by SF, 12-Jan-2015.)
A = B        P6 A = P6 B
 
Theoremp6eqd 4240 Equality deduction for the P6 operation. (Contributed by SF, 12-Jan-2015.)
(φA = B)       (φP6 A = P6 B)
 
Theoremsikeq 4241 Equality theorem for Kuratowski singleton image. (Contributed by SF, 12-Jan-2015.)
(A = BSIk A = SIk B)
 
Theoremsikeqi 4242 Equality inference for Kuratowski singleton image. (Contributed by SF, 12-Jan-2015.)
A = B        SIk A = SIk B
 
Theoremsikeqd 4243 Equality deduction for Kuratowski singleton image. (Contributed by SF, 12-Jan-2015.)
(φA = B)       (φSIk A = SIk B)
 
Theoremimagekeq 4244 Equality theorem for image operation. (Contributed by SF, 12-Jan-2015.)
(A = B → ImagekA = ImagekB)
 
Theoremopkelopkabg 4245* Kuratowski ordered pair membership in an abstraction of Kuratowski ordered pairs. (Contributed by SF, 12-Jan-2015.)
A = {x yz(x = ⟪y, z φ)}    &   (y = B → (φψ))    &   (z = C → (ψχ))       ((B V C W) → (⟪B, C Aχ))
 
Theoremopkelopkab 4246* Kuratowski ordered pair membership in an abstraction of Kuratowski ordered pairs. (Contributed by SF, 12-Jan-2015.)
A = {x yz(x = ⟪y, z φ)}    &   (y = B → (φψ))    &   (z = C → (ψχ))    &   B V    &   C V       (⟪B, C Aχ)
 
Theoremopkelxpkg 4247 Kuratowski ordered pair membership in a Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
((A V B W) → (⟪A, B (C ×k D) ↔ (A C B D)))
 
Theoremopkelxpk 4248 Kuratowski ordered pair membership in a Kuratowski cross product. (Contributed by SF, 13-Jan-2015.)
A V    &   B V       (⟪A, B (C ×k D) ↔ (A C B D))
 
Theoremopkelcnvkg 4249 Kuratowski ordered pair membership in a Kuratowski converse. (Contributed by SF, 12-Jan-2015.)
((A V B W) → (⟪A, B kC ↔ ⟪B, A C))
 
Theoremopkelcnvk 4250 Kuratowski ordered pair membership in a Kuratowski converse. (Contributed by SF, 14-Jan-2015.)
A V    &   B V       (⟪A, B kC ↔ ⟪B, A C)
 
Theoremopkelins2kg 4251* Kuratowski ordered pair membership in Kuratowski insertion operator. (Contributed by SF, 12-Jan-2015.)
((A V B W) → (⟪A, B Ins2k Cxyz(A = {{x}} B = ⟪y, zx, z C)))
 
Theoremopkelins3kg 4252* Kuratowski ordered pair membership in Kuratowski insertion operator. (Contributed by SF, 12-Jan-2015.)
((A V B W) → (⟪A, B Ins3k Cxyz(A = {{x}} B = ⟪y, zx, y C)))
 
Theoremotkelins2kg 4253 Kuratowski ordered triple membership in Kuratowski insertion operator. (Contributed by SF, 12-Jan-2015.)
((A V B W C T) → (⟪{{A}}, ⟪B, C⟫⟫ Ins2k D ↔ ⟪A, C D))
 
Theoremotkelins3kg 4254 Kuratowski ordered triple membership in Kuratowski insertion operator. (Contributed by SF, 12-Jan-2015.)
((A V B W C T) → (⟪{{A}}, ⟪B, C⟫⟫ Ins3k D ↔ ⟪A, B D))
 
Theoremotkelins2k 4255 Kuratowski ordered triple membership in Kuratowski insertion operator. (Contributed by SF, 12-Jan-2015.)
A V    &   B V    &   C V       (⟪{{A}}, ⟪B, C⟫⟫ Ins2k D ↔ ⟪A, C D)
 
Theoremotkelins3k 4256 Kuratowski ordered triple membership in Kuratowski insertion operator. (Contributed by SF, 12-Jan-2015.)
A V    &   B V    &   C V       (⟪{{A}}, ⟪B, C⟫⟫ Ins3k D ↔ ⟪A, B D)
 
Theoremelimakg 4257* Membership in a Kuratowski image. (Contributed by SF, 13-Jan-2015.)
(C V → (C (Ak B) ↔ y By, C A))
 
Theoremelimakvg 4258* Membership in a Kuratowski image under V. (Contributed by SF, 13-Jan-2015.)
(C V → (C (Ak V) ↔ yy, C A))
 
Theoremelimak 4259* Membership in a Kuratowski image. (Contributed by SF, 13-Jan-2015.)
C V       (C (Ak B) ↔ y By, C A)
 
Theoremelimakv 4260* Membership in a Kuratowski image under V. (Contributed by SF, 13-Jan-2015.)
C V       (C (Ak V) ↔ yy, C A)
 
Theoremopkelcokg 4261* Membership in a Kuratowski composition. (Contributed by SF, 13-Jan-2015.)
((A V B W) → (⟪A, B (C k D) ↔ x(⟪A, x D x, B C)))
 
Theoremopkelcok 4262* Membership in a Kuratowski composition. (Contributed by SF, 13-Jan-2015.)
A V    &   B V       (⟪A, B (C k D) ↔ x(⟪A, x D x, B C))
 
Theoremelp6 4263* Membership in the P6 operator. (Contributed by SF, 13-Jan-2015.)
(A V → (A P6 Bxx, {A}⟫ B))
 
Theoremopkelsikg 4264* Membership in Kuratowski singleton image. (Contributed by SF, 13-Jan-2015.)
((A V B W) → (⟪A, B SIk Cxy(A = {x} B = {y} x, y C)))
 
Theoremopksnelsik 4265 Membership of an ordered pair of singletons in a Kuratowski singleton image. (Contributed by SF, 13-Jan-2015.)
A V    &   B V       (⟪{A}, {B}⟫ SIk C ↔ ⟪A, B C)
 
Theoremsikssvvk 4266 A Kuratowski singleton image is a Kuratowski relationship. (Contributed by SF, 13-Jan-2015.)
SIk A (V ×k V)
 
Theoremsikss1c1c 4267 A Kuratowski singleton image is a subset of (1c ×k 1c). (Contributed by SF, 13-Jan-2015.)
SIk A (1c ×k 1c)
 
Theoremopkelssetkg 4268 Membership in the Kuratowski subset relationship. (Contributed by SF, 13-Jan-2015.)
((A V B W) → (⟪A, B SkA B))
 
Theoremelssetkg 4269 Membership via the Kuratowski subset relationship. (Contributed by SF, 13-Jan-2015.)
((A V B W) → (⟪{A}, B SkA B))
 
Theoremelssetk 4270 Membership via the Kuratowski subset relationship. (Contributed by SF, 13-Jan-2015.)
A V    &   B V       (⟪{A}, B SkA B)
 
Theoremopkelimagekg 4271 Membership in the Kuratowski image functor. (Contributed by SF, 13-Jan-2015.)
((A V B W) → (⟪A, B ImagekCB = (Ck A)))
 
Theoremopkelimagek 4272 Membership in the Kuratowski image functor. (Contributed by SF, 20-Jan-2015.)
A V    &   B V       (⟪A, B ImagekCB = (Ck A))
 
Theoremimagekrelk 4273 The Kuratowski image functor is a relationship. (Contributed by SF, 14-Jan-2015.)
ImagekA (V ×k V)
 
Theoremopkelidkg 4274 Membership in the Kuratowski identity relationship. (Contributed by SF, 13-Jan-2015.)
((A V B W) → (⟪A, B IkA = B))
 
Theoremcnvkssvvk 4275 A Kuratowski converse is a Kuratowski relationship. (Contributed by SF, 13-Jan-2015.)
kA (V ×k V)
 
Theoremcnvkxpk 4276 The converse of a Kuratowski cross product. (Contributed by SF, 13-Jan-2015.)
k(A ×k B) = (B ×k A)
 
Theoreminxpk 4277 The intersection of two Kuratowski cross products. (Contributed by SF, 13-Jan-2015.)
((A ×k B) ∩ (C ×k D)) = ((AC) ×k (BD))
 
Theoremssetkssvvk 4278 The Kuratowski subset relationship is a Kuratowski relationship. (Contributed by SF, 13-Jan-2015.)
Sk (V ×k V)
 
Theoremins2kss 4279 Subset law for Ins2k A. (Contributed by SF, 14-Jan-2015.)
Ins2k A (11c ×k (V ×k V))
 
Theoremins3kss 4280 Subset law for Ins3k A. (Contributed by SF, 14-Jan-2015.)
Ins3k A (11c ×k (V ×k V))
 
Theoremidkssvvk 4281 The Kuratowski identity relationship is a Kuratowski relationship. (Contributed by SF, 14-Jan-2015.)
Ik (V ×k V)
 
Theoremimacok 4282 Image under a composition. (Contributed by SF, 4-Feb-2015.)
((A k B) “k C) = (Ak (Bk C))
 
Theoremelimaksn 4283 Membership in a Kuratowski image of a singleton. (Contributed by SF, 4-Feb-2015.)
B V    &   C V       (C (Ak {B}) ↔ ⟪B, C A)
 
Theoremcokrelk 4284 A Kuratowski composition is a Kuratowski relationship. (Contributed by SF, 4-Feb-2015.)
(A k B) (V ×k V)
 
2.2.8  Kuratowski existence theorems
 
Theoremxpkvexg 4285 The Kuratowski cross product of V with a set is a set. (Contributed by SF, 13-Jan-2015.)
(A V → (V ×k A) V)
 
Theoremcnvkexg 4286 The Kuratowski converse of a set is a set. (Contributed by SF, 13-Jan-2015.)
(A VkA V)
 
Theoremcnvkex 4287 The Kuratowski converse of a set is a set. (Contributed by SF, 14-Jan-2015.)
A V       kA V
 
Theoremxpkexg 4288 The Kuratowski cross product of two sets is a set. (Contributed by SF, 13-Jan-2015.)
((A V B W) → (A ×k B) V)
 
Theoremxpkex 4289 The Kuratowski cross product of two sets is a set. (Contributed by SF, 14-Jan-2015.)
A V    &   B V       (A ×k B) V
 
Theoremp6exg 4290 The P6 operator applied to a set yields a set. (Contributed by SF, 13-Jan-2015.)
(A VP6 A V)
 
Theoremdfuni12 4291 Alternate definition of unit union. (Contributed by SF, 15-Mar-2015.)
1A = P6 (V ×k A)
 
Theoremuni1exg 4292 The unit union operator preserves sethood. (Contributed by SF, 13-Jan-2015.)
(A V → ⋃1A V)
 
Theoremuni1ex 4293 The unit union operator preserves sethood. (Contributed by SF, 14-Jan-2015.)
A V       1A V
 
Theoremssetkex 4294 The Kuratowski subset relationship is a set. (Contributed by SF, 13-Jan-2015.)
Sk V
 
Theoremsikexlem 4295* Lemma for sikexg 4296. Equality for two subsets of 1c squared . (Contributed by SF, 14-Jan-2015.)
A (1c ×k 1c)    &   B (1c ×k 1c)       (A = Bxy(⟪{x}, {y}⟫ A ↔ ⟪{x}, {y}⟫ B))
 
Theoremsikexg 4296 The Kuratowski singleton image of a set is a set. (Contributed by SF, 14-Jan-2015.)
(A VSIk A V)
 
Theoremsikex 4297 The Kuratowski singleton image of a set is a set. (Contributed by SF, 14-Jan-2015.)
A V        SIk A V
 
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.)
(Ak B) = ∼ P6 ( ∼ (1c ×k V) ∪ SIk ∼ (A ∩ (B ×k V)))
 
Theoremimakexg 4299 The image of a set under a set is a set. (Contributed by SF, 14-Jan-2015.)
((A V B W) → (Ak B) V)
 
Theoremimakex 4300 The image of a set under a set is a set. (Contributed by SF, 14-Jan-2015.)
A V    &   B V       (Ak B) V
    < 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-6329
  Copyright terms: Public domain < Previous  Next >