Type  Label  Description 
Statement 

Theorem  fvmpts 5701* 
Value of a function given in mapsto notation, using explicit class
substitution. (Contributed by Scott Fenton, 17Jul2013.) (Revised by
Mario Carneiro, 31Aug2015.)

⊢ F =
(x ∈
C ↦
B) ⇒ ⊢ ((A ∈ C ∧ [A /
x]B ∈ V) → (F
‘A) = [A / x]B) 

Theorem  fvmptd 5702* 
Deduction version of fvmpt 5700. (Contributed by Scott Fenton,
18Feb2013.) (Revised by Mario Carneiro, 31Aug2015.)

⊢ (φ
→ F = (x ∈ D ↦ B))
& ⊢ ((φ
∧ x =
A) → B = C)
& ⊢ (φ
→ A ∈ D)
& ⊢ (φ
→ C ∈ V) ⇒ ⊢ (φ
→ (F ‘A) = C) 

Theorem  fvmpt2i 5703* 
Value of a function given by the "maps to" notation. (Contributed by
Mario Carneiro, 23Apr2014.)

⊢ F =
(x ∈
A ↦
B) ⇒ ⊢ (x ∈ A →
(F ‘x) = ( I ‘B)) 

Theorem  fvmpt2 5704* 
Value of a function given by the "maps to" notation. (Contributed by
FL, 21Jun2010.)

⊢ F =
(x ∈
A ↦
B) ⇒ ⊢ ((x ∈ A ∧ B ∈ C) →
(F ‘x) = B) 

Theorem  fvmptss 5705* 
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, 13Feb2015.)

⊢ F =
(x ∈
A ↦
B) ⇒ ⊢ (∀x ∈ A B ⊆ C →
(F ‘D) ⊆ C) 

Theorem  dffn5v 5706* 
Representation of a function in terms of its values. (Contributed by
FL, 14Sep2013.) (Revised by Mario Carneiro, 16Dec2013.)

⊢ (F Fn
A ↔ F = (x ∈ A ↦ (F
‘x))) 

Theorem  fnov2 5707* 
Representation of a function in terms of its values. (Contributed by
Mario Carneiro, 23Dec2013.)

⊢ (F Fn
(A × B) ↔ F =
(x ∈
A, y
∈ B
↦ (xFy))) 

Theorem  mpt2mptx 5708* 
Express a twoargument function as a oneargument function, or
viceversa. In this version B(x) is
not assumed to be constant
w.r.t x. (Contributed
by Mario Carneiro, 29Dec2014.)

⊢ (z = ⟨x, y⟩ →
C = D) ⇒ ⊢ (z ∈ ∪x ∈ A ({x} ×
B) ↦
C) = (x ∈ A, y ∈ B ↦ D) 

Theorem  mpt2mpt 5709* 
Express a twoargument function as a oneargument function, or
viceversa. (Contributed by Mario Carneiro, 17Dec2013.) (Revised by
Mario Carneiro, 29Dec2014.)

⊢ (z = ⟨x, y⟩ →
C = D) ⇒ ⊢ (z ∈ (A ×
B) ↦
C) = (x ∈ A, y ∈ B ↦ D) 

Theorem  ovmpt4g 5710* 
Value of a function given by the "maps to" notation. (This is the
operation analog of fvmpt2 5704.) (Contributed by NM, 21Feb2004.)
(Revised by Mario Carneiro, 1Sep2015.)

⊢ F =
(x ∈
A, y
∈ B
↦ C) ⇒ ⊢ ((x ∈ A ∧ y ∈ B ∧ C ∈ V) →
(xFy) = C) 

Theorem  ov2gf 5711* 
The value of an operation class abstraction. A version of ovmpt2g 5715
using boundvariable hypotheses. (Contributed by NM, 17Aug2006.)
(Revised by Mario Carneiro, 19Dec2013.)

⊢ Ⅎ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 5712* 
The value of an operation class abstraction. Variant of ovmpt2ga 5713
which does not require D and x to be distinct. (Contributed by
Jeff Madsen, 10Jun2010.) (Revised by Mario Carneiro, 20Dec2013.)

⊢ ((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 5713* 
Value of an operation given by a mapsto rule. Equivalent to ov2ag 5598.
(Contributed by Mario Carneiro, 19Dec2013.)

⊢ ((x =
A ∧
y = B)
→ R = S)
& ⊢ F =
(x ∈
C, y
∈ D
↦ R) ⇒ ⊢ ((A ∈ C ∧ B ∈ D ∧ S ∈ H) →
(AFB) = S) 

Theorem  ovmpt2a 5714* 
Value of an operation given by a mapsto rule. Equivalent to
ov2ag 5598. (Contributed by set.mm contributors,
19Dec2013.)

⊢ ((x =
A ∧
y = B)
→ R = S)
& ⊢ F =
(x ∈
C, y
∈ D
↦ R)
& ⊢ S ∈ V ⇒ ⊢ ((A ∈ C ∧ B ∈ D) →
(AFB) = S) 

Theorem  ovmpt2g 5715* 
Value of an operation given by a mapsto rule. (Unnecessary distinct
variable restrictions were removed by David Abernethy, 19Jun2012.)
(Contributed by set.mm contributors, 2Oct2007.) (Revised by set.mm
contributors, 24Jul2012.)

⊢ (x =
A → R = G)
& ⊢ (y =
B → G = S)
& ⊢ F =
(x ∈
C, y
∈ D
↦ R) ⇒ ⊢ ((A ∈ C ∧ B ∈ D ∧ S ∈ H) →
(AFB) = S) 

Theorem  ovmpt2 5716* 
Value of an operation given by a mapsto rule. Equivalent to ov2 in
set.mm. (Contributed by set.mm contributors, 12Sep2011.)

⊢ (x =
A → R = G)
& ⊢ (y =
B → G = S)
& ⊢ F =
(x ∈
C, y
∈ D
↦ R)
& ⊢ S ∈ V ⇒ ⊢ ((A ∈ C ∧ B ∈ D) →
(AFB) = S) 

Theorem  rnmpt2 5717* 
The range of an operation given by the "maps to" notation.
(Contributed
by FL, 20Jun2011.)

⊢ F =
(x ∈
A, y
∈ B
↦ C) ⇒ ⊢ ran F =
{z ∣
∃x
∈ A
∃y
∈ B
z = C} 

Theorem  mptv 5718* 
Function with universal domain in mapsto notation. (Contributed by
set.mm contributors, 16Aug2013.)

⊢ (x ∈ V ↦ B) = {⟨x, y⟩ ∣ y = B} 

Theorem  mpt2v 5719* 
Operation with universal domain in mapsto notation. (Contributed by
set.mm contributors, 16Aug2013.)

⊢ (x ∈ V, y ∈ V ↦ C) = {⟨⟨x, y⟩, z⟩ ∣ z =
C} 

Theorem  mptresid 5720* 
The restricted identity expressed with the "maps to" notation.
(Contributed by FL, 25Apr2012.)

⊢ (x ∈ A ↦ x) = ( I
↾ A) 

Theorem  fvmptex 5721* 
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 5339.) 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, 14Jul2013.)
(Revised by Mario Carneiro, 23Apr2014.)

⊢ F =
(x ∈
A ↦
B)
& ⊢ G =
(x ∈
A ↦ ( I
‘B)) ⇒ ⊢ (F
‘C) = (G ‘C) 

Theorem  fvmptf 5722* 
Value of a function given by an orderedpair class abstraction. This
version of fvmptg 5698 uses boundvariable hypotheses instead of
distinct
variable conditions. (Contributed by NM, 8Nov2005.) (Revised by
Mario Carneiro, 15Oct2016.)

⊢ ℲxA & ⊢ ℲxC & ⊢ (x =
A → B = C)
& ⊢ F =
(x ∈
D ↦
B) ⇒ ⊢ ((A ∈ D ∧ C ∈ V) →
(F ‘A) = C) 

Theorem  fvmptnf 5723* 
The value of a function given by an orderedpair class abstraction is
the empty set when the class it would otherwise map to is a proper
class. This version of fvmptn 5724 uses boundvariable hypotheses
instead
of distinct variable conditions. (Contributed by NM, 21Oct2003.)
(Revised by Mario Carneiro, 11Sep2015.)

⊢ ℲxA & ⊢ ℲxC & ⊢ (x =
A → B = C)
& ⊢ F =
(x ∈
D ↦
B) ⇒ ⊢ (¬ C
∈ V → (F ‘A) =
∅) 

Theorem  fvmptn 5724* 
This somewhat nonintuitive 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 5698.
(Contributed by NM, 21Oct2003.) (Revised by Mario Carneiro,
9Sep2013.)

⊢ (x =
D → B = C)
& ⊢ F =
(x ∈
A ↦
B) ⇒ ⊢ (¬ C
∈ V → (F ‘D) =
∅) 

Theorem  fvmptss2 5725* 
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, 13Feb2015.)

⊢ (x =
D → B = C)
& ⊢ F =
(x ∈
A ↦
B) ⇒ ⊢ (F
‘D) ⊆ C 

Theorem  f1od 5726* 
Describe an implicit onetoone onto function. (Contributed by Mario
Carneiro, 12May2014.)

⊢ F =
(x ∈
A ↦
C)
& ⊢ ((φ
∧ x ∈ A) →
C ∈
W)
& ⊢ ((φ
∧ y ∈ B) →
D ∈
X)
& ⊢ (φ
→ ((x ∈ A ∧ y = C) ↔ (y
∈ B
∧ x =
D))) ⇒ ⊢ (φ
→ F:A–11onto→B) 

Theorem  f1o2d 5727* 
Describe an implicit onetoone onto function. (Contributed by Mario
Carneiro, 12May2014.)

⊢ F =
(x ∈
A ↦
C)
& ⊢ ((φ
∧ x ∈ A) →
C ∈
B)
& ⊢ ((φ
∧ y ∈ B) →
D ∈
A)
& ⊢ ((φ
∧ (x
∈ A
∧ y ∈ B)) →
(x = D
↔ y = C)) ⇒ ⊢ (φ
→ F:A–11onto→B) 

Theorem  dfswap3 5728* 
Alternate definition of Swap as an
operator abstraction.
(Contributed by SF, 23Feb2015.)

⊢ Swap = {⟨⟨x, y⟩, z⟩ ∣ z = ⟨y, x⟩} 

Theorem  dfswap4 5729* 
Alternate definition of Swap as an
operator mapping. (Contributed
by SF, 23Feb2015.)

⊢ Swap = (x ∈ V, y ∈ V ↦ ⟨y, x⟩) 

Theorem  fmpt2x 5730* 
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, 29Dec2014.)

⊢ F =
(x ∈
A, y
∈ B
↦ C) ⇒ ⊢ (∀x ∈ A ∀y ∈ B C ∈ D ↔
F:∪x ∈ A ({x} × B)–→D) 

Theorem  fmpt2 5731* 
Functionality, domain and range of a class given by the "maps to"
notation. (Contributed by FL, 17May2010.)

⊢ F =
(x ∈
A, y
∈ B
↦ C) ⇒ ⊢ (∀x ∈ A ∀y ∈ B C ∈ D ↔
F:(A
× B)–→D) 

Theorem  fnmpt2 5732* 
Functionality and domain of a class given by the "maps to" notation.
(Contributed by FL, 17May2010.)

⊢ F =
(x ∈
A, y
∈ B
↦ C) ⇒ ⊢ (∀x ∈ A ∀y ∈ B C ∈ V →
F Fn (A × B)) 

Theorem  fnmpt2i 5733* 
Functionality and domain of a class given by the "maps to" notation.
(Contributed by FL, 17May2010.)

⊢ F =
(x ∈
A, y
∈ B
↦ C)
& ⊢ C ∈ V ⇒ ⊢ F Fn
(A × B) 

Theorem  dmmpt2 5734* 
Domain of a class given by the "maps to" notation. (Contributed by
FL,
17May2010.)

⊢ F =
(x ∈
A, y
∈ B
↦ C)
& ⊢ C ∈ V ⇒ ⊢ dom F =
(A × B) 

2.3.10 Set construction lemmas


Syntax  ctxp 5735 
Extend the definition of a class to include the tail cross product.

class
(A ⊗ B) 

Definition  dftxp 5736 
Define the tail cross product of two classes. Definition from [Holmes]
p. 40. See brtxp 5783 for membership. (Contributed by SF,
9Feb2015.)

⊢ (A ⊗
B) = ((^{◡}1^{st} ∘ A) ∩
(^{◡}2^{nd} ∘ B)) 

Syntax  cpprod 5737 
Extend the definition of a class to include the parallel product
operation.

class
PProd (A, B) 

Definition  dfpprod 5738 
Define the parallel product operation. (Contributed by SF,
9Feb2015.)

⊢ PProd (A, B) =
((A ∘
1^{st} ) ⊗ (B ∘ 2^{nd} )) 

Syntax  cfix 5739 
Extend the definition of a class to include the fixed points of a
relationship.

class
Fix A 

Definition  dffix 5740 
Define the fixed points of a relationship. (Contributed by SF,
9Feb2015.)

⊢ Fix A = ran (A
∩ I ) 

Syntax  ccup 5741 
Extend the definition of a class to include the cup function.

class
Cup 

Definition  dfcup 5742* 
Define the cup function. (Contributed by SF, 9Feb2015.)

⊢ Cup = (x ∈ V, y ∈ V ↦ (x ∪
y)) 

Syntax  cdisj 5743 
Extend the definition of a class to include the disjoint relationship.

class
Disj 

Definition  dfdisj 5744* 
Define the relationship of all disjoint sets. (Contributed by SF,
9Feb2015.)

⊢ Disj = {⟨x, y⟩ ∣ (x ∩
y) = ∅} 

Syntax  caddcfn 5745 
Extend the definition of a class to include the cardinal sum function.

class
AddC 

Definition  dfaddcfn 5746* 
Define the function representing cardinal sum. (Contributed by SF,
9Feb2015.)

⊢ AddC = (x ∈ V, y ∈ V ↦ (x
+_{c} y)) 

Syntax  ccompose 5747 
Extend the definition of a class to include the compostion function.

class
Compose 

Definition  dfcompose 5748* 
Define the composition function. (Contributed by Scott Fenton,
19Apr2021.)

⊢ Compose =
(x ∈ V,
y ∈ V
↦ (x
∘ y)) 

Syntax  cins2 5749 
Extend the definition of a class to include the second insertion
operation.

class
Ins2 A 

Definition  dfins2 5750 
Define the second insertion operation. (Contributed by SF,
9Feb2015.)

⊢ Ins2 A = (V ⊗ A) 

Syntax  cins3 5751 
Extend the definition of a class to include the third insertion
operation.

class
Ins3 A 

Definition  dfins3 5752 
Define the third insertion operation. (Contributed by SF, 9Feb2015.)

⊢ Ins3 A = (A ⊗
V) 

Syntax  cimage 5753 
Extend the definition of a class to include the image function.

class
ImageA 

Definition  dfimage 5754 
Define the image function of a class. (Contributed by SF, 9Feb2015.)
(Revised by Scott Fenton, 19Apr2021.)

⊢ ImageA =
∼ (( Ins2 S
⊕ Ins3 ( S
∘ ^{◡} SI A)) “ 1_{c}) 

Syntax  cins4 5755 
Extend the definition of a class to include the fourth insertion
operation.

class
Ins4 A 

Definition  dfins4 5756 
Define the fourth insertion operation. (Contributed by SF,
9Feb2015.)

⊢ Ins4 A = (^{◡}(1^{st} ⊗ ((1^{st}
∘ 2^{nd} ) ⊗
((1^{st} ∘ 2^{nd} ) ∘ 2^{nd} ))) “ A) 

Syntax  csi3 5757 
Extend the definition of a class to include the triple singleton image.

class
SI_{3} A 

Definition  dfsi3 5758 
Define the triple singleton image. (Contributed by SF, 9Feb2015.)

⊢ SI_{3} A = (( SI
1^{st} ⊗ ( SI
(1^{st} ∘ 2^{nd} )
⊗ SI (2^{nd} ∘ 2^{nd} ))) “ ℘_{1}A) 

Syntax  cfuns 5759 
Extend the definition of a class to include the set of all functions.

class
Funs 

Definition  dffuns 5760 
Define the class of all functions. (Contributed by SF, 9Feb2015.)

⊢ Funs = {f ∣ Fun f} 

Syntax  cfns 5761 
Extend the definition of a class to include the function with domain
relationship.

class
Fns 

Definition  dffns 5762* 
Define the function with domain relationship. (Contributed by SF,
9Feb2015.)

⊢ Fns = {⟨f, a⟩ ∣ f Fn
a} 

Syntax  ccross 5763 
Extend the definition of a class to include the cross product function.

class
Cross 

Definition  dfcross 5764* 
Define the cross product function. (Contributed by SF, 9Feb2015.)

⊢ Cross = (x ∈ V, y ∈ V ↦ (x ×
y)) 

Syntax  cpw1fn 5765 
Extend the definition of a class to include the unit power class
function.

class
Pw1Fn 

Definition  dfpw1fn 5766 
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, 9Feb2015.)

⊢ Pw1Fn = (x ∈
1_{c} ↦ ℘_{1}∪x) 

Syntax  cfullfun 5767 
Extend the definition of a class to include the full function
operation.

class
FullFun F 

Definition  dffullfun 5768 
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, 9Feb2015.)

⊢ FullFun F = ((( I ∘
F) ∖ (
∼ I ∘ F)) ∪ ( ∼ dom (( I ∘ F) ∖ ( ∼ I ∘
F)) × {∅})) 

Syntax  cdomfn 5769 
Extend the definition of a class to include the domain function.

class
Dom 

Definition  dfdomfn 5770 
Define the domain function. This is a function wrapper for the domain
operator. (Contributed by Scott Fenton, 9Aug2019.)

⊢ Dom = (x ∈ V ↦ dom x) 

Syntax  cranfn 5771 
Extend the definition of a class to include the range function.

class
Ran 

Definition  dfranfn 5772 
Define the range function. This is a function wrapper for the range
operator. (Contributed by Scott Fenton, 9Aug2019.)

⊢ Ran = (x ∈ V ↦ ran x) 

Theorem  brsnsi 5773 
Binary relationship of singletons in a singleton image. (Contributed by
SF, 9Feb2015.)

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ ({A} SI R{B} ↔ ARB) 

Theorem  opsnelsi 5774 
Ordered pair membership of singletons in a singleton image.
(Contributed by SF, 9Feb2015.)

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (⟨{A}, {B}⟩ ∈ SI R ↔ ⟨A, B⟩ ∈ R) 

Theorem  brsnsi1 5775* 
Binary relationship of a singleton to an arbitrary set in a singleton
image. (Contributed by SF, 9Mar2015.)

⊢ A ∈ V ⇒ ⊢ ({A} SI RB ↔ ∃x(B = {x} ∧ ARx)) 

Theorem  brsnsi2 5776* 
Binary relationship of an arbitrary set to a singleton in a singleton
image. (Contributed by SF, 9Mar2015.)

⊢ A ∈ V ⇒ ⊢ (B SI R{A} ↔ ∃x(B = {x} ∧ xRA)) 

Theorem  brco1st 5777 
Binary relationship of composition with 1^{st}.
(Contributed by SF,
9Feb2015.)

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (⟨A, B⟩(R ∘ 1^{st} )C ↔ ARC) 

Theorem  brco2nd 5778 
Binary relationship of composition with 2^{nd}.
(Contributed by SF,
9Feb2015.)

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (⟨A, B⟩(R ∘ 2^{nd} )C ↔ BRC) 

Theorem  txpeq1 5779 
Equality theorem for tail cross product. (Contributed by Scott Fenton,
31Jul2019.)

⊢ (A =
B → (A ⊗ C) =
(B ⊗ C)) 

Theorem  txpeq2 5780 
Equality theorem for tail cross product. (Contributed by Scott Fenton,
31Jul2019.)

⊢ (A =
B → (C ⊗ A) =
(C ⊗ B)) 

Theorem  trtxp 5781 
Trinary relationship over a tail cross product. (Contributed by SF,
13Feb2015.)

⊢ (A(R ⊗ S)⟨B, C⟩ ↔ (ARB ∧ ASC)) 

Theorem  oteltxp 5782 
Ordered triple membership in a tail cross product. (Contributed by SF,
13Feb2015.)

⊢ (⟨A, ⟨B, C⟩⟩ ∈ (R ⊗
S) ↔ (⟨A, B⟩ ∈ R ∧ ⟨A, C⟩ ∈ S)) 

Theorem  brtxp 5783* 
Binary relationship over a tail cross product. (Contributed by SF,
11Feb2015.)

⊢ (A(R ⊗ S)B ↔
∃x∃y(B = ⟨x, y⟩ ∧ ARx ∧ ASy)) 

Theorem  txpexg 5784 
The tail cross product of two sets is a set. (Contributed by SF,
9Feb2015.)

⊢ ((A ∈ V ∧ B ∈ W) →
(A ⊗ B) ∈
V) 

Theorem  txpex 5785 
The tail cross product of two sets is a set. (Contributed by SF,
9Feb2015.)

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (A ⊗
B) ∈
V 

Theorem  restxp 5786 
Restriction distributes over tail cross product. (Contributed by SF,
24Feb2015.)

⊢ ((A
⊗ B) ↾ C) =
((A ↾
C) ⊗ (B ↾ C)) 

Theorem  elfix 5787 
Membership in the fixed points of a relationship. (Contributed by SF,
11Feb2015.)

⊢ (A ∈ Fix R ↔ ARA) 

Theorem  fixexg 5788 
The fixed points of a set form a set. (Contributed by SF,
11Feb2015.)

⊢ (R ∈ V →
Fix R ∈ V) 

Theorem  fixex 5789 
The fixed points of a set form a set. (Contributed by SF,
11Feb2015.)

⊢ R ∈ V ⇒ ⊢ Fix R ∈
V 

Theorem  op1st2nd 5790 
Express equality to an ordered pair via 1^{st} and 2^{nd}.
(Contributed by SF, 12Feb2015.)

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ ((C1^{st} A ∧ C2^{nd} B) ↔ C =
⟨A,
B⟩) 

Theorem  otelins2 5791 
Ordered triple membership in Ins2.
(Contributed by SF,
13Feb2015.)

⊢ B ∈ V ⇒ ⊢ (⟨A, ⟨B, C⟩⟩ ∈ Ins2 R ↔ ⟨A, C⟩ ∈ R) 

Theorem  otelins3 5792 
Ordered triple membership in Ins3.
(Contributed by SF,
13Feb2015.)

⊢ C ∈ V ⇒ ⊢ (⟨A, ⟨B, C⟩⟩ ∈ Ins3 R ↔ ⟨A, B⟩ ∈ R) 

Theorem  brimage 5793 
Binary relationship over the image function. (Contributed by SF,
11Feb2015.)

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (AImageRB ↔ B =
(R “ A)) 

Theorem  oqelins4 5794 
Ordered quadruple membership in Ins4. (Contributed by SF,
13Feb2015.)

⊢ D ∈ V ⇒ ⊢ (⟨A, ⟨B, ⟨C, D⟩⟩⟩ ∈ Ins4 R ↔ ⟨A, ⟨B, C⟩⟩ ∈ R) 

Theorem  ins2exg 5795 
Ins2 preserves sethood.
(Contributed by SF, 9Mar2015.)

⊢ (A ∈ V →
Ins2 A ∈ V) 

Theorem  ins3exg 5796 
Ins3 preserves sethood.
(Contributed by SF, 22Feb2015.)

⊢ (A ∈ V →
Ins3 A ∈ V) 

Theorem  ins2ex 5797 
Ins2 preserves sethood.
(Contributed by SF, 12Feb2015.)

⊢ A ∈ V ⇒ ⊢ Ins2 A ∈
V 

Theorem  ins3ex 5798 
Ins3 preserves sethood.
(Contributed by SF, 12Feb2015.)

⊢ A ∈ V ⇒ ⊢ Ins3 A ∈
V 

Theorem  ins4ex 5799 
Ins4 preserves sethood.
(Contributed by SF, 12Feb2015.)

⊢ A ∈ V ⇒ ⊢ Ins4 A ∈
V 

Theorem  imageexg 5800 
The image function of a set is a set. (Contributed by SF,
11Feb2015.)

⊢ (A ∈ V →
ImageA ∈
V) 