P. 58 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 5701-5800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fvmpt 5701*	Value of a function given in maps-to notation. (Contributed by set.mm contributors, 17-Aug-2011.)
⊢ (x = A → B = C)    &   ⊢ F = (x ∈ D ↦ B)    &   ⊢ C ∈ V    ⇒   ⊢ (A ∈ D → (F ‘A) = C)
Theorem	fvmpts 5702*	Value of a function given in maps-to notation, using explicit class substitution. (Contributed by Scott Fenton, 17-Jul-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ F = (x ∈ C ↦ B)    ⇒   ⊢ ((A ∈ C ∧ [A / x]B ∈ V) → (F ‘A) = [A / x]B)
Theorem	fvmptd 5703*	Deduction version of fvmpt 5701. (Contributed by Scott Fenton, 18-Feb-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ (φ → F = (x ∈ D ↦ B))    &   ⊢ ((φ ∧ x = A) → B = C)    &   ⊢ (φ → A ∈ D)    &   ⊢ (φ → C ∈ V)    ⇒   ⊢ (φ → (F ‘A) = C)
Theorem	fvmpt2i 5704*	Value of a function given by the "maps to" notation. (Contributed by Mario Carneiro, 23-Apr-2014.)
⊢ F = (x ∈ A ↦ B)    ⇒   ⊢ (x ∈ A → (F ‘x) = ( I ‘B))
Theorem	fvmpt2 5705*	Value of a function given by the "maps to" notation. (Contributed by FL, 21-Jun-2010.)
⊢ F = (x ∈ A ↦ B)    ⇒   ⊢ ((x ∈ A ∧ B ∈ C) → (F ‘x) = B)
Theorem	fvmptss 5706*	If all the values of the mapping are subsets of a class C, then so is any evaluation of the mapping, even if D is not in the base set A. (Contributed by Mario Carneiro, 13-Feb-2015.)
⊢ F = (x ∈ A ↦ B)    ⇒   ⊢ (∀x ∈ A B ⊆ C → (F ‘D) ⊆ C)
Theorem	dffn5v 5707*	Representation of a function in terms of its values. (Contributed by FL, 14-Sep-2013.) (Revised by Mario Carneiro, 16-Dec-2013.)
⊢ (F Fn A ↔ F = (x ∈ A ↦ (F ‘x)))
Theorem	fnov2 5708*	Representation of a function in terms of its values. (Contributed by Mario Carneiro, 23-Dec-2013.)
⊢ (F Fn (A × B) ↔ F = (x ∈ A, y ∈ B ↦ (xFy)))
Theorem	mpt2mptx 5709*	Express a two-argument function as a one-argument function, or vice-versa. In this version B(x) is not assumed to be constant w.r.t x. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ (z = ⟨x, y⟩ → C = D)    ⇒   ⊢ (z ∈ ∪x ∈ A ({x} × B) ↦ C) = (x ∈ A, y ∈ B ↦ D)
Theorem	mpt2mpt 5710*	Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 17-Dec-2013.) (Revised by Mario Carneiro, 29-Dec-2014.)
⊢ (z = ⟨x, y⟩ → C = D)    ⇒   ⊢ (z ∈ (A × B) ↦ C) = (x ∈ A, y ∈ B ↦ D)
Theorem	ovmpt4g 5711*	Value of a function given by the "maps to" notation. (This is the operation analog of fvmpt2 5705.) (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro, 1-Sep-2015.)
⊢ F = (x ∈ A, y ∈ B ↦ C)    ⇒   ⊢ ((x ∈ A ∧ y ∈ B ∧ C ∈ V) → (xFy) = C)
Theorem	ov2gf 5712*	The value of an operation class abstraction. A version of ovmpt2g 5716 using bound-variable hypotheses. (Contributed by NM, 17-Aug-2006.) (Revised by Mario Carneiro, 19-Dec-2013.)
⊢ ℲxA    &   ⊢ ℲyA    &   ⊢ ℲyB    &   ⊢ ℲxG    &   ⊢ ℲyS    &   ⊢ (x = A → R = G)    &   ⊢ (y = B → G = S)    &   ⊢ F = (x ∈ C, y ∈ D ↦ R)    ⇒   ⊢ ((A ∈ C ∧ B ∈ D ∧ S ∈ H) → (AFB) = S)
Theorem	ovmpt2x 5713*	The value of an operation class abstraction. Variant of ovmpt2ga 5714 which does not require D and x to be distinct. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 20-Dec-2013.)
⊢ ((x = A ∧ y = B) → R = S)    &   ⊢ (x = A → D = L)    &   ⊢ F = (x ∈ C, y ∈ D ↦ R)    ⇒   ⊢ ((A ∈ C ∧ B ∈ L ∧ S ∈ H) → (AFB) = S)
Theorem	ovmpt2ga 5714*	Value of an operation given by a maps-to rule. Equivalent to ov2ag 5599. (Contributed by Mario Carneiro, 19-Dec-2013.)
⊢ ((x = A ∧ y = B) → R = S)    &   ⊢ F = (x ∈ C, y ∈ D ↦ R)    ⇒   ⊢ ((A ∈ C ∧ B ∈ D ∧ S ∈ H) → (AFB) = S)
Theorem	ovmpt2a 5715*	Value of an operation given by a maps-to rule. Equivalent to ov2ag 5599. (Contributed by set.mm contributors, 19-Dec-2013.)
⊢ ((x = A ∧ y = B) → R = S)    &   ⊢ F = (x ∈ C, y ∈ D ↦ R)    &   ⊢ S ∈ V    ⇒   ⊢ ((A ∈ C ∧ B ∈ D) → (AFB) = S)
Theorem	ovmpt2g 5716*	Value of an operation given by a maps-to rule. (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Contributed by set.mm contributors, 2-Oct-2007.) (Revised by set.mm contributors, 24-Jul-2012.)
⊢ (x = A → R = G)    &   ⊢ (y = B → G = S)    &   ⊢ F = (x ∈ C, y ∈ D ↦ R)    ⇒   ⊢ ((A ∈ C ∧ B ∈ D ∧ S ∈ H) → (AFB) = S)
Theorem	ovmpt2 5717*	Value of an operation given by a maps-to rule. Equivalent to ov2 in set.mm. (Contributed by set.mm contributors, 12-Sep-2011.)
⊢ (x = A → R = G)    &   ⊢ (y = B → G = S)    &   ⊢ F = (x ∈ C, y ∈ D ↦ R)    &   ⊢ S ∈ V    ⇒   ⊢ ((A ∈ C ∧ B ∈ D) → (AFB) = S)
Theorem	rnmpt2 5718*	The range of an operation given by the "maps to" notation. (Contributed by FL, 20-Jun-2011.)
⊢ F = (x ∈ A, y ∈ B ↦ C)    ⇒   ⊢ ran F = {z ∣ ∃x ∈ A ∃y ∈ B z = C}
Theorem	mptv 5719*	Function with universal domain in maps-to notation. (Contributed by set.mm contributors, 16-Aug-2013.)
⊢ (x ∈ V ↦ B) = {⟨x, y⟩ ∣ y = B}
Theorem	mpt2v 5720*	Operation with universal domain in maps-to notation. (Contributed by set.mm contributors, 16-Aug-2013.)
⊢ (x ∈ V, y ∈ V ↦ C) = {⟨⟨x, y⟩, z⟩ ∣ z = C}
Theorem	mptresid 5721*	The restricted identity expressed with the "maps to" notation. (Contributed by FL, 25-Apr-2012.)
⊢ (x ∈ A ↦ x) = ( I ↾ A)
Theorem	fvmptex 5722*	Express a function F whose value B may not always be a set in terms of another function G for which sethood is guaranteed. (Note that ( I ‘B) is just shorthand for if(B ∈ V, B, ∅), and it is always a set by fvex 5340.) Note also that these functions are not the same; wherever B(C) is not a set, C is not in the domain of F (so it evaluates to the empty set), but C is in the domain of G, and G(C) is defined to be the empty set. (Contributed by Mario Carneiro, 14-Jul-2013.) (Revised by Mario Carneiro, 23-Apr-2014.)
⊢ F = (x ∈ A ↦ B)    &   ⊢ G = (x ∈ A ↦ ( I ‘B))    ⇒   ⊢ (F ‘C) = (G ‘C)
Theorem	fvmptf 5723*	Value of a function given by an ordered-pair class abstraction. This version of fvmptg 5699 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 8-Nov-2005.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ ℲxA    &   ⊢ ℲxC    &   ⊢ (x = A → B = C)    &   ⊢ F = (x ∈ D ↦ B)    ⇒   ⊢ ((A ∈ D ∧ C ∈ V) → (F ‘A) = C)
Theorem	fvmptnf 5724*	The value of a function given by an ordered-pair class abstraction is the empty set when the class it would otherwise map to is a proper class. This version of fvmptn 5725 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 21-Oct-2003.) (Revised by Mario Carneiro, 11-Sep-2015.)
⊢ ℲxA    &   ⊢ ℲxC    &   ⊢ (x = A → B = C)    &   ⊢ F = (x ∈ D ↦ B)    ⇒   ⊢ (¬ C ∈ V → (F ‘A) = ∅)
Theorem	fvmptn 5725*	This somewhat non-intuitive theorem tells us the value of its function is the empty set when the class C it would otherwise map to is a proper class. This is a technical lemma that can help eliminate redundant sethood antecedents otherwise required by fvmptg 5699. (Contributed by NM, 21-Oct-2003.) (Revised by Mario Carneiro, 9-Sep-2013.)
⊢ (x = D → B = C)    &   ⊢ F = (x ∈ A ↦ B)    ⇒   ⊢ (¬ C ∈ V → (F ‘D) = ∅)
Theorem	fvmptss2 5726*	A mapping always evaluates to a subset of the substituted expression in the mapping, even if this is a proper class, or we are out of the domain. (Contributed by Mario Carneiro, 13-Feb-2015.)
⊢ (x = D → B = C)    &   ⊢ F = (x ∈ A ↦ B)    ⇒   ⊢ (F ‘D) ⊆ C
Theorem	f1od 5727*	Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 12-May-2014.)
⊢ F = (x ∈ A ↦ C)    &   ⊢ ((φ ∧ x ∈ A) → C ∈ W)    &   ⊢ ((φ ∧ y ∈ B) → D ∈ X)    &   ⊢ (φ → ((x ∈ A ∧ y = C) ↔ (y ∈ B ∧ x = D)))    ⇒   ⊢ (φ → F:A–1-1-onto→B)
Theorem	f1o2d 5728*	Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 12-May-2014.)
⊢ F = (x ∈ A ↦ C)    &   ⊢ ((φ ∧ x ∈ A) → C ∈ B)    &   ⊢ ((φ ∧ y ∈ B) → D ∈ A)    &   ⊢ ((φ ∧ (x ∈ A ∧ y ∈ B)) → (x = D ↔ y = C))    ⇒   ⊢ (φ → F:A–1-1-onto→B)
Theorem	dfswap3 5729*	Alternate definition of Swap as an operator abstraction. (Contributed by SF, 23-Feb-2015.)
⊢ Swap = {⟨⟨x, y⟩, z⟩ ∣ z = ⟨y, x⟩}
Theorem	dfswap4 5730*	Alternate definition of Swap as an operator mapping. (Contributed by SF, 23-Feb-2015.)
⊢ Swap = (x ∈ V, y ∈ V ↦ ⟨y, x⟩)
Theorem	fmpt2x 5731*	Functionality, domain and codomain of a class given by the "maps to" notation, where B(x) is not constant but depends on x. (Contributed by NM, 29-Dec-2014.)
⊢ F = (x ∈ A, y ∈ B ↦ C)    ⇒   ⊢ (∀x ∈ A ∀y ∈ B C ∈ D ↔ F:∪x ∈ A ({x} × B)–→D)
Theorem	fmpt2 5732*	Functionality, domain and range of a class given by the "maps to" notation. (Contributed by FL, 17-May-2010.)
⊢ F = (x ∈ A, y ∈ B ↦ C)    ⇒   ⊢ (∀x ∈ A ∀y ∈ B C ∈ D ↔ F:(A × B)–→D)
Theorem	fnmpt2 5733*	Functionality and domain of a class given by the "maps to" notation. (Contributed by FL, 17-May-2010.)
⊢ F = (x ∈ A, y ∈ B ↦ C)    ⇒   ⊢ (∀x ∈ A ∀y ∈ B C ∈ V → F Fn (A × B))
Theorem	fnmpt2i 5734*	Functionality and domain of a class given by the "maps to" notation. (Contributed by FL, 17-May-2010.)
⊢ F = (x ∈ A, y ∈ B ↦ C)    &   ⊢ C ∈ V    ⇒   ⊢ F Fn (A × B)
Theorem	dmmpt2 5735*	Domain of a class given by the "maps to" notation. (Contributed by FL, 17-May-2010.)
⊢ F = (x ∈ A, y ∈ B ↦ C)    &   ⊢ C ∈ V    ⇒   ⊢ dom F = (A × B)
2.3.10  Set construction lemmas
Syntax	ctxp 5736	Extend the definition of a class to include the tail cross product.
class (A ⊗ B)
Definition	df-txp 5737	Define the tail cross product of two classes. Definition from [Holmes] p. 40. See brtxp 5784 for membership. (Contributed by SF, 9-Feb-2015.)
⊢ (A ⊗ B) = ((◡1st ∘ A) ∩ (◡2nd ∘ B))
Syntax	cpprod 5738	Extend the definition of a class to include the parallel product operation.
class PProd (A, B)
Definition	df-pprod 5739	Define the parallel product operation. (Contributed by SF, 9-Feb-2015.)
⊢ PProd (A, B) = ((A ∘ 1st ) ⊗ (B ∘ 2nd ))
Syntax	cfix 5740	Extend the definition of a class to include the fixed points of a relationship.
class Fix A
Definition	df-fix 5741	Define the fixed points of a relationship. (Contributed by SF, 9-Feb-2015.)
⊢ Fix A = ran (A ∩ I )
Syntax	ccup 5742	Extend the definition of a class to include the cup function.
class Cup
Definition	df-cup 5743*	Define the cup function. (Contributed by SF, 9-Feb-2015.)
⊢ Cup = (x ∈ V, y ∈ V ↦ (x ∪ y))
Syntax	cdisj 5744	Extend the definition of a class to include the disjoint relationship.
class Disj
Definition	df-disj 5745*	Define the relationship of all disjoint sets. (Contributed by SF, 9-Feb-2015.)
⊢ Disj = {⟨x, y⟩ ∣ (x ∩ y) = ∅}
Syntax	caddcfn 5746	Extend the definition of a class to include the cardinal sum function.
class AddC
Definition	df-addcfn 5747*	Define the function representing cardinal sum. (Contributed by SF, 9-Feb-2015.)
⊢ AddC = (x ∈ V, y ∈ V ↦ (x +c y))
Syntax	ccompose 5748	Extend the definition of a class to include the compostion function.
class Compose
Definition	df-compose 5749*	Define the composition function. (Contributed by Scott Fenton, 19-Apr-2021.)
⊢ Compose = (x ∈ V, y ∈ V ↦ (x ∘ y))
Syntax	cins2 5750	Extend the definition of a class to include the second insertion operation.
class Ins2 A
Definition	df-ins2 5751	Define the second insertion operation. (Contributed by SF, 9-Feb-2015.)
⊢ Ins2 A = (V ⊗ A)
Syntax	cins3 5752	Extend the definition of a class to include the third insertion operation.
class Ins3 A
Definition	df-ins3 5753	Define the third insertion operation. (Contributed by SF, 9-Feb-2015.)
⊢ Ins3 A = (A ⊗ V)
Syntax	cimage 5754	Extend the definition of a class to include the image function.
class ImageA
Definition	df-image 5755	Define the image function of a class. (Contributed by SF, 9-Feb-2015.) (Revised by Scott Fenton, 19-Apr-2021.)
⊢ ImageA = ∼ (( Ins2 S ⊕ Ins3 ( S ∘ ◡ SI A)) “ 1c)
Syntax	cins4 5756	Extend the definition of a class to include the fourth insertion operation.
class Ins4 A
Definition	df-ins4 5757	Define the fourth insertion operation. (Contributed by SF, 9-Feb-2015.)
⊢ Ins4 A = (◡(1st ⊗ ((1st ∘ 2nd ) ⊗ ((1st ∘ 2nd ) ∘ 2nd ))) “ A)
Syntax	csi3 5758	Extend the definition of a class to include the triple singleton image.
class SI3 A
Definition	df-si3 5759	Define the triple singleton image. (Contributed by SF, 9-Feb-2015.)
⊢ SI3 A = (( SI 1st ⊗ ( SI (1st ∘ 2nd ) ⊗ SI (2nd ∘ 2nd ))) “ ℘1A)
Syntax	cfuns 5760	Extend the definition of a class to include the set of all functions.
class Funs
Definition	df-funs 5761	Define the class of all functions. (Contributed by SF, 9-Feb-2015.)
⊢ Funs = {f ∣ Fun f}
Syntax	cfns 5762	Extend the definition of a class to include the function with domain relationship.
class Fns
Definition	df-fns 5763*	Define the function with domain relationship. (Contributed by SF, 9-Feb-2015.)
⊢ Fns = {⟨f, a⟩ ∣ f Fn a}
Syntax	ccross 5764	Extend the definition of a class to include the cross product function.
class Cross
Definition	df-cross 5765*	Define the cross product function. (Contributed by SF, 9-Feb-2015.)
⊢ Cross = (x ∈ V, y ∈ V ↦ (x × y))
Syntax	cpw1fn 5766	Extend the definition of a class to include the unit power class function.
class Pw1Fn
Definition	df-pw1fn 5767	Define the function that takes a singleton to the unit power class of its member. This function is defined in such a way as to ensure stratification. (Contributed by SF, 9-Feb-2015.)
⊢ Pw1Fn = (x ∈ 1c ↦ ℘1∪x)
Syntax	cfullfun 5768	Extend the definition of a class to include the full function operation.
class FullFun F
Definition	df-fullfun 5769	Define the full function operator. This is a function over V that agrees with the function value of F at every point. (Contributed by SF, 9-Feb-2015.)
⊢ FullFun F = ((( I ∘ F) ∖ ( ∼ I ∘ F)) ∪ ( ∼ dom (( I ∘ F) ∖ ( ∼ I ∘ F)) × {∅}))
Syntax	cdomfn 5770	Extend the definition of a class to include the domain function.
class Dom
Definition	df-domfn 5771	Define the domain function. This is a function wrapper for the domain operator. (Contributed by Scott Fenton, 9-Aug-2019.)
⊢ Dom = (x ∈ V ↦ dom x)
Syntax	cranfn 5772	Extend the definition of a class to include the range function.
class Ran
Definition	df-ranfn 5773	Define the range function. This is a function wrapper for the range operator. (Contributed by Scott Fenton, 9-Aug-2019.)
⊢ Ran = (x ∈ V ↦ ran x)
Theorem	brsnsi 5774	Binary relationship of singletons in a singleton image. (Contributed by SF, 9-Feb-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ ({A} SI R{B} ↔ ARB)
Theorem	opsnelsi 5775	Ordered pair membership of singletons in a singleton image. (Contributed by SF, 9-Feb-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (⟨{A}, {B}⟩ ∈ SI R ↔ ⟨A, B⟩ ∈ R)
Theorem	brsnsi1 5776*	Binary relationship of a singleton to an arbitrary set in a singleton image. (Contributed by SF, 9-Mar-2015.)
⊢ A ∈ V    ⇒   ⊢ ({A} SI RB ↔ ∃x(B = {x} ∧ ARx))
Theorem	brsnsi2 5777*	Binary relationship of an arbitrary set to a singleton in a singleton image. (Contributed by SF, 9-Mar-2015.)
⊢ A ∈ V    ⇒   ⊢ (B SI R{A} ↔ ∃x(B = {x} ∧ xRA))
Theorem	brco1st 5778	Binary relationship of composition with 1st. (Contributed by SF, 9-Feb-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (⟨A, B⟩(R ∘ 1st )C ↔ ARC)
Theorem	brco2nd 5779	Binary relationship of composition with 2nd. (Contributed by SF, 9-Feb-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (⟨A, B⟩(R ∘ 2nd )C ↔ BRC)
Theorem	txpeq1 5780	Equality theorem for tail cross product. (Contributed by Scott Fenton, 31-Jul-2019.)
⊢ (A = B → (A ⊗ C) = (B ⊗ C))
Theorem	txpeq2 5781	Equality theorem for tail cross product. (Contributed by Scott Fenton, 31-Jul-2019.)
⊢ (A = B → (C ⊗ A) = (C ⊗ B))
Theorem	trtxp 5782	Trinary relationship over a tail cross product. (Contributed by SF, 13-Feb-2015.)
⊢ (A(R ⊗ S)⟨B, C⟩ ↔ (ARB ∧ ASC))
Theorem	oteltxp 5783	Ordered triple membership in a tail cross product. (Contributed by SF, 13-Feb-2015.)
⊢ (⟨A, ⟨B, C⟩⟩ ∈ (R ⊗ S) ↔ (⟨A, B⟩ ∈ R ∧ ⟨A, C⟩ ∈ S))
Theorem	brtxp 5784*	Binary relationship over a tail cross product. (Contributed by SF, 11-Feb-2015.)
⊢ (A(R ⊗ S)B ↔ ∃x∃y(B = ⟨x, y⟩ ∧ ARx ∧ ASy))
Theorem	txpexg 5785	The tail cross product of two sets is a set. (Contributed by SF, 9-Feb-2015.)
⊢ ((A ∈ V ∧ B ∈ W) → (A ⊗ B) ∈ V)
Theorem	txpex 5786	The tail cross product of two sets is a set. (Contributed by SF, 9-Feb-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (A ⊗ B) ∈ V
Theorem	restxp 5787	Restriction distributes over tail cross product. (Contributed by SF, 24-Feb-2015.)
⊢ ((A ⊗ B) ↾ C) = ((A ↾ C) ⊗ (B ↾ C))
Theorem	elfix 5788	Membership in the fixed points of a relationship. (Contributed by SF, 11-Feb-2015.)
⊢ (A ∈ Fix R ↔ ARA)
Theorem	fixexg 5789	The fixed points of a set form a set. (Contributed by SF, 11-Feb-2015.)
⊢ (R ∈ V → Fix R ∈ V)
Theorem	fixex 5790	The fixed points of a set form a set. (Contributed by SF, 11-Feb-2015.)
⊢ R ∈ V    ⇒   ⊢ Fix R ∈ V
Theorem	op1st2nd 5791	Express equality to an ordered pair via 1st and 2nd. (Contributed by SF, 12-Feb-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ ((C1st A ∧ C2nd B) ↔ C = ⟨A, B⟩)
Theorem	otelins2 5792	Ordered triple membership in Ins2. (Contributed by SF, 13-Feb-2015.)
⊢ B ∈ V    ⇒   ⊢ (⟨A, ⟨B, C⟩⟩ ∈ Ins2 R ↔ ⟨A, C⟩ ∈ R)
Theorem	otelins3 5793	Ordered triple membership in Ins3. (Contributed by SF, 13-Feb-2015.)
⊢ C ∈ V    ⇒   ⊢ (⟨A, ⟨B, C⟩⟩ ∈ Ins3 R ↔ ⟨A, B⟩ ∈ R)
Theorem	brimage 5794	Binary relationship over the image function. (Contributed by SF, 11-Feb-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (AImageRB ↔ B = (R “ A))
Theorem	oqelins4 5795	Ordered quadruple membership in Ins4. (Contributed by SF, 13-Feb-2015.)
⊢ D ∈ V    ⇒   ⊢ (⟨A, ⟨B, ⟨C, D⟩⟩⟩ ∈ Ins4 R ↔ ⟨A, ⟨B, C⟩⟩ ∈ R)
Theorem	ins2exg 5796	Ins2 preserves sethood. (Contributed by SF, 9-Mar-2015.)
⊢ (A ∈ V → Ins2 A ∈ V)
Theorem	ins3exg 5797	Ins3 preserves sethood. (Contributed by SF, 22-Feb-2015.)
⊢ (A ∈ V → Ins3 A ∈ V)
Theorem	ins2ex 5798	Ins2 preserves sethood. (Contributed by SF, 12-Feb-2015.)
⊢ A ∈ V    ⇒   ⊢ Ins2 A ∈ V
Theorem	ins3ex 5799	Ins3 preserves sethood. (Contributed by SF, 12-Feb-2015.)
⊢ A ∈ V    ⇒   ⊢ Ins3 A ∈ V
Theorem	ins4ex 5800	Ins4 preserves sethood. (Contributed by SF, 12-Feb-2015.)
⊢ A ∈ V    ⇒   ⊢ Ins4 A ∈ V