P. 43 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 4201-4300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	xpkeq12 4201	Equality theorem for Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
⊢ ((A = B ∧ C = D) → (A ×k C) = (B ×k D))
Theorem	xpkeq1i 4202	Equality inference for Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
⊢ A = B    ⇒   ⊢ (A ×k C) = (B ×k C)
Theorem	xpkeq2i 4203	Equality inference for Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
⊢ A = B    ⇒   ⊢ (C ×k A) = (C ×k B)
Theorem	xpkeq12i 4204	Equality inference for Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
⊢ A = B    &   ⊢ C = D    ⇒   ⊢ (A ×k C) = (B ×k D)
Theorem	xpkeq1d 4205	Equality deduction for Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (A ×k C) = (B ×k C))
Theorem	xpkeq2d 4206	Equality deduction for Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (C ×k A) = (C ×k B))
Theorem	xpkeq12d 4207	Equality deduction for Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
⊢ (φ → A = B)    &   ⊢ (φ → C = D)    ⇒   ⊢ (φ → (A ×k C) = (B ×k D))
Theorem	elvvk 4208*	Membership in (V ×k V). (Contributed by SF, 13-Jan-2015.)
⊢ (A ∈ (V ×k V) ↔ ∃x∃y A = ⟪x, y⟫)
Theorem	opkabssvvk 4209*	Any Kuratowski ordered pair abstraction is a subset of (V ×k V). (Contributed by SF, 13-Jan-2015.)
⊢ {x ∣ ∃y∃z(x = ⟪y, z⟫ ∧ φ)} ⊆ (V ×k V)
Theorem	opkabssvvki 4210*	Any Kuratowski ordered pair abstraction is a subset of (V ×k V). (Contributed by SF, 13-Jan-2015.)
⊢ A = {x ∣ ∃y∃z(x = ⟪y, z⟫ ∧ φ)}    ⇒   ⊢ A ⊆ (V ×k V)
Theorem	xpkssvvk 4211	Any Kuratowski cross product is a subset of (V ×k V). (Contributed by SF, 13-Jan-2015.)
⊢ (A ×k B) ⊆ (V ×k V)
Theorem	ssrelk 4212*	Subset for Kuratowski relationships. (Contributed by SF, 13-Jan-2015.)
⊢ (A ⊆ (V ×k V) → (A ⊆ B ↔ ∀x∀y(⟪x, y⟫ ∈ A → ⟪x, y⟫ ∈ B)))
Theorem	eqrelk 4213*	Equality for two Kuratowski relationships. (Contributed by SF, 13-Jan-2015.)
⊢ ((A ⊆ (V ×k V) ∧ B ⊆ (V ×k V)) → (A = B ↔ ∀x∀y(⟪x, y⟫ ∈ A ↔ ⟪x, y⟫ ∈ B)))
Theorem	eqrelkriiv 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
Theorem	eqrelkrdv 4215*	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)
Theorem	cnvkeq 4216	Equality theorem for Kuratowski converse. (Contributed by SF, 12-Jan-2015.)
⊢ (A = B → ◡kA = ◡kB)
Theorem	cnvkeqi 4217	Equality inference for Kuratowski converse. (Contributed by SF, 12-Jan-2015.)
⊢ A = B    ⇒   ⊢ ◡kA = ◡kB
Theorem	cnvkeqd 4218	Equality deduction for Kuratowski converse. (Contributed by SF, 12-Jan-2015.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → ◡kA = ◡kB)
Theorem	ins2keq 4219	Equality theorem for the Kuratowski insert two operator. (Contributed by SF, 12-Jan-2015.)
⊢ (A = B → Ins2k A = Ins2k B)
Theorem	ins3keq 4220	Equality theorem for the Kuratowski insert three operator. (Contributed by SF, 12-Jan-2015.)
⊢ (A = B → Ins3k A = Ins3k B)
Theorem	ins2keqi 4221	Equality inference for Kuratowski insert two operator. (Contributed by SF, 12-Jan-2015.)
⊢ A = B    ⇒   ⊢ Ins2k A = Ins2k B
Theorem	ins3keqi 4222	Equality inference for Kuratowski insert three operator. (Contributed by SF, 12-Jan-2015.)
⊢ A = B    ⇒   ⊢ Ins3k A = Ins3k B
Theorem	ins2keqd 4223	Equality deduction for Kuratowski insert two operator. (Contributed by SF, 12-Jan-2015.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → Ins2k A = Ins2k B)
Theorem	ins3keqd 4224	Equality deduction for Kuratowski insert three operator. (Contributed by SF, 12-Jan-2015.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → Ins3k A = Ins3k B)
Theorem	imakeq1 4225	Equality theorem for Kuratowski image. (Contributed by SF, 12-Jan-2015.)
⊢ (A = B → (A “k C) = (B “k C))
Theorem	imakeq2 4226	Equality theorem for Kuratowski image. (Contributed by SF, 12-Jan-2015.)
⊢ (A = B → (C “k A) = (C “k B))
Theorem	imakeq1i 4227	Equality theorem for image. (Contributed by SF, 12-Jan-2015.)
⊢ A = B    ⇒   ⊢ (A “k C) = (B “k C)
Theorem	imakeq2i 4228	Equality theorem for Kuratowski image. (Contributed by SF, 12-Jan-2015.)
⊢ A = B    ⇒   ⊢ (C “k A) = (C “k B)
Theorem	imakeq1d 4229	Equality theorem for Kuratowski image. (Contributed by SF, 12-Jan-2015.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (A “k C) = (B “k C))
Theorem	imakeq2d 4230	Equality theorem for Kuratowski image. (Contributed by SF, 12-Jan-2015.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (C “k A) = (C “k B))
Theorem	cokeq1 4231	Equality theorem for Kuratowski composition of two classes. (Contributed by SF, 12-Jan-2015.)
⊢ (A = B → (A ∘k C) = (B ∘k C))
Theorem	cokeq2 4232	Equality theorem for Kuratowski composition of two classes. (Contributed by SF, 12-Jan-2015.)
⊢ (A = B → (C ∘k A) = (C ∘k B))
Theorem	cokeq1i 4233	Equality inference for Kuratowski composition of two classes. (Contributed by SF, 12-Jan-2015.)
⊢ A = B    ⇒   ⊢ (A ∘k C) = (B ∘k C)
Theorem	cokeq2i 4234	Equality inference for Kuratowski composition of two classes. (Contributed by SF, 12-Jan-2015.)
⊢ A = B    ⇒   ⊢ (C ∘k A) = (C ∘k B)
Theorem	cokeq1d 4235	Equality deduction for Kuratowski composition of two classes. (Contributed by SF, 12-Jan-2015.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (A ∘k C) = (B ∘k C))
Theorem	cokeq2d 4236	Equality deduction for Kuratowski composition of two classes. (Contributed by SF, 12-Jan-2015.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (C ∘k A) = (C ∘k B))
Theorem	cokeq12i 4237	Equality inference for Kuratowski composition of two classes. (Contributed by SF, 12-Jan-2015.)
⊢ A = B    &   ⊢ C = D    ⇒   ⊢ (A ∘k C) = (B ∘k D)
Theorem	cokeq12d 4238	Equality deduction for Kuratowski composition of two classes. (Contributed by SF, 12-Jan-2015.)
⊢ (φ → A = B)    &   ⊢ (φ → C = D)    ⇒   ⊢ (φ → (A ∘k C) = (B ∘k D))
Theorem	p6eq 4239	Equality theorem for P6 operation. (Contributed by SF, 12-Jan-2015.)
⊢ (A = B → P6 A = P6 B)
Theorem	p6eqi 4240	Equality inference for the P6 operation. (Contributed by SF, 12-Jan-2015.)
⊢ A = B    ⇒   ⊢ P6 A = P6 B
Theorem	p6eqd 4241	Equality deduction for the P6 operation. (Contributed by SF, 12-Jan-2015.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → P6 A = P6 B)
Theorem	sikeq 4242	Equality theorem for Kuratowski singleton image. (Contributed by SF, 12-Jan-2015.)
⊢ (A = B → SIk A = SIk B)
Theorem	sikeqi 4243	Equality inference for Kuratowski singleton image. (Contributed by SF, 12-Jan-2015.)
⊢ A = B    ⇒   ⊢ SIk A = SIk B
Theorem	sikeqd 4244	Equality deduction for Kuratowski singleton image. (Contributed by SF, 12-Jan-2015.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → SIk A = SIk B)
Theorem	imagekeq 4245	Equality theorem for image operation. (Contributed by SF, 12-Jan-2015.)
⊢ (A = B → ImagekA = ImagekB)
Theorem	opkelopkabg 4246*	Kuratowski ordered pair membership in an abstraction of Kuratowski ordered pairs. (Contributed by SF, 12-Jan-2015.)
⊢ A = {x ∣ ∃y∃z(x = ⟪y, z⟫ ∧ φ)}    &   ⊢ (y = B → (φ ↔ ψ))    &   ⊢ (z = C → (ψ ↔ χ))    ⇒   ⊢ ((B ∈ V ∧ C ∈ W) → (⟪B, C⟫ ∈ A ↔ χ))
Theorem	opkelopkab 4247*	Kuratowski ordered pair membership in an abstraction of Kuratowski ordered pairs. (Contributed by SF, 12-Jan-2015.)
⊢ A = {x ∣ ∃y∃z(x = ⟪y, z⟫ ∧ φ)}    &   ⊢ (y = B → (φ ↔ ψ))    &   ⊢ (z = C → (ψ ↔ χ))    &   ⊢ B ∈ V    &   ⊢ C ∈ V    ⇒   ⊢ (⟪B, C⟫ ∈ A ↔ χ)
Theorem	opkelxpkg 4248	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)))
Theorem	opkelxpk 4249	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))
Theorem	opkelcnvkg 4250	Kuratowski ordered pair membership in a Kuratowski converse. (Contributed by SF, 12-Jan-2015.)
⊢ ((A ∈ V ∧ B ∈ W) → (⟪A, B⟫ ∈ ◡kC ↔ ⟪B, A⟫ ∈ C))
Theorem	opkelcnvk 4251	Kuratowski ordered pair membership in a Kuratowski converse. (Contributed by SF, 14-Jan-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (⟪A, B⟫ ∈ ◡kC ↔ ⟪B, A⟫ ∈ C)
Theorem	opkelins2kg 4252*	Kuratowski ordered pair membership in Kuratowski insertion operator. (Contributed by SF, 12-Jan-2015.)
⊢ ((A ∈ V ∧ B ∈ W) → (⟪A, B⟫ ∈ Ins2k C ↔ ∃x∃y∃z(A = {{x}} ∧ B = ⟪y, z⟫ ∧ ⟪x, z⟫ ∈ C)))
Theorem	opkelins3kg 4253*	Kuratowski ordered pair membership in Kuratowski insertion operator. (Contributed by SF, 12-Jan-2015.)
⊢ ((A ∈ V ∧ B ∈ W) → (⟪A, B⟫ ∈ Ins3k C ↔ ∃x∃y∃z(A = {{x}} ∧ B = ⟪y, z⟫ ∧ ⟪x, y⟫ ∈ C)))
Theorem	otkelins2kg 4254	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))
Theorem	otkelins3kg 4255	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))
Theorem	otkelins2k 4256	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)
Theorem	otkelins3k 4257	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)
Theorem	elimakg 4258*	Membership in a Kuratowski image. (Contributed by SF, 13-Jan-2015.)
⊢ (C ∈ V → (C ∈ (A “k B) ↔ ∃y ∈ B ⟪y, C⟫ ∈ A))
Theorem	elimakvg 4259*	Membership in a Kuratowski image under V. (Contributed by SF, 13-Jan-2015.)
⊢ (C ∈ V → (C ∈ (A “k V) ↔ ∃y⟪y, C⟫ ∈ A))
Theorem	elimak 4260*	Membership in a Kuratowski image. (Contributed by SF, 13-Jan-2015.)
⊢ C ∈ V    ⇒   ⊢ (C ∈ (A “k B) ↔ ∃y ∈ B ⟪y, C⟫ ∈ A)
Theorem	elimakv 4261*	Membership in a Kuratowski image under V. (Contributed by SF, 13-Jan-2015.)
⊢ C ∈ V    ⇒   ⊢ (C ∈ (A “k V) ↔ ∃y⟪y, C⟫ ∈ A)
Theorem	opkelcokg 4262*	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)))
Theorem	opkelcok 4263*	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))
Theorem	elp6 4264*	Membership in the P6 operator. (Contributed by SF, 13-Jan-2015.)
⊢ (A ∈ V → (A ∈ P6 B ↔ ∀x⟪x, {A}⟫ ∈ B))
Theorem	opkelsikg 4265*	Membership in Kuratowski singleton image. (Contributed by SF, 13-Jan-2015.)
⊢ ((A ∈ V ∧ B ∈ W) → (⟪A, B⟫ ∈ SIk C ↔ ∃x∃y(A = {x} ∧ B = {y} ∧ ⟪x, y⟫ ∈ C)))
Theorem	opksnelsik 4266	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)
Theorem	sikssvvk 4267	A Kuratowski singleton image is a Kuratowski relationship. (Contributed by SF, 13-Jan-2015.)
⊢ SIk A ⊆ (V ×k V)
Theorem	sikss1c1c 4268	A Kuratowski singleton image is a subset of (1c ×k 1c). (Contributed by SF, 13-Jan-2015.)
⊢ SIk A ⊆ (1c ×k 1c)
Theorem	opkelssetkg 4269	Membership in the Kuratowski subset relationship. (Contributed by SF, 13-Jan-2015.)
⊢ ((A ∈ V ∧ B ∈ W) → (⟪A, B⟫ ∈ Sk ↔ A ⊆ B))
Theorem	elssetkg 4270	Membership via the Kuratowski subset relationship. (Contributed by SF, 13-Jan-2015.)
⊢ ((A ∈ V ∧ B ∈ W) → (⟪{A}, B⟫ ∈ Sk ↔ A ∈ B))
Theorem	elssetk 4271	Membership via the Kuratowski subset relationship. (Contributed by SF, 13-Jan-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (⟪{A}, B⟫ ∈ Sk ↔ A ∈ B)
Theorem	opkelimagekg 4272	Membership in the Kuratowski image functor. (Contributed by SF, 13-Jan-2015.)
⊢ ((A ∈ V ∧ B ∈ W) → (⟪A, B⟫ ∈ ImagekC ↔ B = (C “k A)))
Theorem	opkelimagek 4273	Membership in the Kuratowski image functor. (Contributed by SF, 20-Jan-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (⟪A, B⟫ ∈ ImagekC ↔ B = (C “k A))
Theorem	imagekrelk 4274	The Kuratowski image functor is a relationship. (Contributed by SF, 14-Jan-2015.)
⊢ ImagekA ⊆ (V ×k V)
Theorem	opkelidkg 4275	Membership in the Kuratowski identity relationship. (Contributed by SF, 13-Jan-2015.)
⊢ ((A ∈ V ∧ B ∈ W) → (⟪A, B⟫ ∈ Ik ↔ A = B))
Theorem	cnvkssvvk 4276	A Kuratowski converse is a Kuratowski relationship. (Contributed by SF, 13-Jan-2015.)
⊢ ◡kA ⊆ (V ×k V)
Theorem	cnvkxpk 4277	The converse of a Kuratowski cross product. (Contributed by SF, 13-Jan-2015.)
⊢ ◡k(A ×k B) = (B ×k A)
Theorem	inxpk 4278	The intersection of two Kuratowski cross products. (Contributed by SF, 13-Jan-2015.)
⊢ ((A ×k B) ∩ (C ×k D)) = ((A ∩ C) ×k (B ∩ D))
Theorem	ssetkssvvk 4279	The Kuratowski subset relationship is a Kuratowski relationship. (Contributed by SF, 13-Jan-2015.)
⊢ Sk ⊆ (V ×k V)
Theorem	ins2kss 4280	Subset law for Ins2k A. (Contributed by SF, 14-Jan-2015.)
⊢ Ins2k A ⊆ (℘11c ×k (V ×k V))
Theorem	ins3kss 4281	Subset law for Ins3k A. (Contributed by SF, 14-Jan-2015.)
⊢ Ins3k A ⊆ (℘11c ×k (V ×k V))
Theorem	idkssvvk 4282	The Kuratowski identity relationship is a Kuratowski relationship. (Contributed by SF, 14-Jan-2015.)
⊢ Ik ⊆ (V ×k V)
Theorem	imacok 4283	Image under a composition. (Contributed by SF, 4-Feb-2015.)
⊢ ((A ∘k B) “k C) = (A “k (B “k C))
Theorem	elimaksn 4284	Membership in a Kuratowski image of a singleton. (Contributed by SF, 4-Feb-2015.)
⊢ B ∈ V    &   ⊢ C ∈ V    ⇒   ⊢ (C ∈ (A “k {B}) ↔ ⟪B, C⟫ ∈ A)
Theorem	cokrelk 4285	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
Theorem	xpkvexg 4286	The Kuratowski cross product of V with a set is a set. (Contributed by SF, 13-Jan-2015.)
⊢ (A ∈ V → (V ×k A) ∈ V)
Theorem	cnvkexg 4287	The Kuratowski converse of a set is a set. (Contributed by SF, 13-Jan-2015.)
⊢ (A ∈ V → ◡kA ∈ V)
Theorem	cnvkex 4288	The Kuratowski converse of a set is a set. (Contributed by SF, 14-Jan-2015.)
⊢ A ∈ V    ⇒   ⊢ ◡kA ∈ V
Theorem	xpkexg 4289	The Kuratowski cross product of two sets is a set. (Contributed by SF, 13-Jan-2015.)
⊢ ((A ∈ V ∧ B ∈ W) → (A ×k B) ∈ V)
Theorem	xpkex 4290	The Kuratowski cross product of two sets is a set. (Contributed by SF, 14-Jan-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (A ×k B) ∈ V
Theorem	p6exg 4291	The P6 operator applied to a set yields a set. (Contributed by SF, 13-Jan-2015.)
⊢ (A ∈ V → P6 A ∈ V)
Theorem	dfuni12 4292	Alternate definition of unit union. (Contributed by SF, 15-Mar-2015.)
⊢ ⋃1A = P6 (V ×k A)
Theorem	uni1exg 4293	The unit union operator preserves sethood. (Contributed by SF, 13-Jan-2015.)
⊢ (A ∈ V → ⋃1A ∈ V)
Theorem	uni1ex 4294	The unit union operator preserves sethood. (Contributed by SF, 14-Jan-2015.)
⊢ A ∈ V    ⇒   ⊢ ⋃1A ∈ V
Theorem	ssetkex 4295	The Kuratowski subset relationship is a set. (Contributed by SF, 13-Jan-2015.)
⊢ Sk ∈ V
Theorem	sikexlem 4296*	Lemma for sikexg 4297. Equality for two subsets of 1c squared . (Contributed by SF, 14-Jan-2015.)
⊢ A ⊆ (1c ×k 1c)    &   ⊢ B ⊆ (1c ×k 1c)    ⇒   ⊢ (A = B ↔ ∀x∀y(⟪{x}, {y}⟫ ∈ A ↔ ⟪{x}, {y}⟫ ∈ B))
Theorem	sikexg 4297	The Kuratowski singleton image of a set is a set. (Contributed by SF, 14-Jan-2015.)
⊢ (A ∈ V → SIk A ∈ V)
Theorem	sikex 4298	The Kuratowski singleton image of a set is a set. (Contributed by SF, 14-Jan-2015.)
⊢ A ∈ V    ⇒   ⊢ SIk A ∈ V
Theorem	dfimak2 4299	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.)
⊢ (A “k B) = ∼ P6 ( ∼ (1c ×k V) ∪ SIk ∼ (A ∩ (B ×k V)))
Theorem	imakexg 4300	The image of a set under a set is a set. (Contributed by SF, 14-Jan-2015.)
⊢ ((A ∈ V ∧ B ∈ W) → (A “k B) ∈ V)