Type  Label  Description 
Statement 

Theorem  elovmpt2 5701* 
Utility lemma for twoparameter classes. (Contributed by Stefan O'Rear,
21Jan2015.)



Theorem  f1ocnvd 5702* 
Describe an implicit onetoone onto function. (Contributed by Mario
Carneiro, 30Apr2015.)



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



Theorem  f1ocnv2d 5704* 
Describe an implicit onetoone onto function. (Contributed by Mario
Carneiro, 30Apr2015.)



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



Theorem  f1opw2 5706* 
A onetoone mapping induces a onetoone mapping on power sets. This
version of f1opw 5707 avoids the Axiom of Replacement.
(Contributed by
Mario Carneiro, 26Jun2015.)



Theorem  f1opw 5707* 
A onetoone mapping induces a onetoone mapping on power sets.
(Contributed by Stefan O'Rear, 18Nov2014.) (Revised by Mario
Carneiro, 26Jun2015.)



Theorem  suppssfv 5708* 
Formula building theorem for support restriction, on a function which
preserves zero. (Contributed by Stefan O'Rear, 9Mar2015.)



Theorem  suppssov1 5709* 
Formula building theorem for support restrictions: operator with left
annihilator. (Contributed by Stefan O'Rear, 9Mar2015.)



2.6.12 Function operation


Syntax  cof 5710 
Extend class notation to include mapping of an operation to a function
operation.



Syntax  cofr 5711 
Extend class notation to include mapping of a binary relation to a
function relation.



Definition  dfof 5712* 
Define the function operation map. The definition is designed so that
if is a binary
operation, then is the analogous operation
on functions which corresponds to applying pointwise to the values
of the functions. (Contributed by Mario Carneiro, 20Jul2014.)



Definition  dfofr 5713* 
Define the function relation map. The definition is designed so that if
is a binary
relation, then is the analogous relation on
functions which is true when each element of the left function relates
to the corresponding element of the right function. (Contributed by
Mario Carneiro, 28Jul2014.)



Theorem  ofeq 5714 
Equality theorem for function operation. (Contributed by Mario
Carneiro, 20Jul2014.)



Theorem  ofreq 5715 
Equality theorem for function relation. (Contributed by Mario Carneiro,
28Jul2014.)



Theorem  ofexg 5716 
A function operation restricted to a set is a set. (Contributed by NM,
28Jul2014.)



Theorem  nfof 5717* 
Hypothesis builder for function operation. (Contributed by Mario
Carneiro, 20Jul2014.)



Theorem  nfofr 5718* 
Hypothesis builder for function relation. (Contributed by Mario
Carneiro, 28Jul2014.)



Theorem  offval 5719* 
Value of an operation applied to two functions. (Contributed by Mario
Carneiro, 20Jul2014.)



Theorem  ofrfval 5720* 
Value of a relation applied to two functions. (Contributed by Mario
Carneiro, 28Jul2014.)



Theorem  fnofval 5721 
Evaluate a function operation at a point. (Contributed by Mario
Carneiro, 20Jul2014.)



Theorem  ofrval 5722 
Exhibit a function relation at a point. (Contributed by Mario
Carneiro, 28Jul2014.)



Theorem  ofmresval 5723 
Value of a restriction of the function operation map. (Contributed by
NM, 20Oct2014.)



Theorem  off 5724* 
The function operation produces a function. (Contributed by Mario
Carneiro, 20Jul2014.)



Theorem  ofres 5725 
Restrict the operands of a function operation to the same domain as that
of the operation itself. (Contributed by Mario Carneiro,
15Sep2014.)



Theorem  offval2 5726* 
The function operation expressed as a mapping. (Contributed by Mario
Carneiro, 20Jul2014.)



Theorem  ofrfval2 5727* 
The function relation acting on maps. (Contributed by Mario Carneiro,
20Jul2014.)



Theorem  suppssof1 5728* 
Formula building theorem for support restrictions: vector operation with
left annihilator. (Contributed by Stefan O'Rear, 9Mar2015.)



Theorem  ofco 5729 
The composition of a function operation with another function.
(Contributed by Mario Carneiro, 19Dec2014.)



Theorem  offveqb 5730* 
Equivalent expressions for equality with a function operation.
(Contributed by NM, 9Oct2014.) (Proof shortened by Mario Carneiro,
5Dec2016.)



Theorem  ofc12 5731 
Function operation on two constant functions. (Contributed by Mario
Carneiro, 28Jul2014.)



Theorem  caofref 5732* 
Transfer a reflexive law to the function relation. (Contributed by
Mario Carneiro, 28Jul2014.)



Theorem  caofinvl 5733* 
Transfer a left inverse law to the function operation. (Contributed
by NM, 22Oct2014.)



Theorem  caofcom 5734* 
Transfer a commutative law to the function operation. (Contributed by
Mario Carneiro, 26Jul2014.)



Theorem  caofrss 5735* 
Transfer a relation subset law to the function relation. (Contributed
by Mario Carneiro, 28Jul2014.)



Theorem  caoftrn 5736* 
Transfer a transitivity law to the function relation. (Contributed by
Mario Carneiro, 28Jul2014.)



2.6.13 Functions (continued)


Theorem  resfunexgALT 5737 
The restriction of a function to a set exists. Compare Proposition 6.17
of [TakeutiZaring] p. 28. This
version has a shorter proof than
resfunexg 5382 but requires axpow 3927 and axun 4170. (Contributed by NM,
7Apr1995.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  cofunexg 5738 
Existence of a composition when the first member is a function.
(Contributed by NM, 8Oct2007.)



Theorem  cofunex2g 5739 
Existence of a composition when the second member is onetoone.
(Contributed by NM, 8Oct2007.)



Theorem  fnexALT 5740 
If the domain of a function is a set, the function is a set. Theorem
6.16(1) of [TakeutiZaring] p. 28.
This theorem is derived using the Axiom
of Replacement in the form of funimaexg 4983. This version of fnex 5383
uses
axpow 3927 and axun 4170, whereas fnex 5383
does not. (Contributed by NM,
14Aug1994.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  funrnex 5741 
If the domain of a function exists, so does its range. Part of Theorem
4.15(v) of [Monk1] p. 46. This theorem is
derived using the Axiom of
Replacement in the form of funex 5384. (Contributed by NM, 11Nov1995.)



Theorem  fornex 5742 
If the domain of an onto function exists, so does its codomain.
(Contributed by NM, 23Jul2004.)



Theorem  f1dmex 5743 
If the codomain of a onetoone function exists, so does its domain. This
can be thought of as a form of the Axiom of Replacement. (Contributed by
NM, 4Sep2004.)



Theorem  abrexex 5744* 
Existence of a class abstraction of existentially restricted sets.
is normally a freevariable parameter in the class expression
substituted for , which can be thought of as . This
simplelooking theorem is actually quite powerful and appears to involve
the Axiom of Replacement in an intrinsic way, as can be seen by tracing
back through the path mptexg 5386, funex 5384, fnex 5383, resfunexg 5382, and
funimaexg 4983. See also abrexex2 5751. (Contributed by NM, 16Oct2003.)
(Proof shortened by Mario Carneiro, 31Aug2015.)



Theorem  abrexexg 5745* 
Existence of a class abstraction of existentially restricted sets.
is normally a freevariable parameter in . The antecedent assures
us that is a
set. (Contributed by NM, 3Nov2003.)



Theorem  iunexg 5746* 
The existence of an indexed union. is normally a freevariable
parameter in .
(Contributed by NM, 23Mar2006.)



Theorem  abrexex2g 5747* 
Existence of an existentially restricted class abstraction.
(Contributed by Jeff Madsen, 2Sep2009.)



Theorem  opabex3d 5748* 
Existence of an ordered pair abstraction, deduction version.
(Contributed by Alexander van der Vekens, 19Oct2017.)



Theorem  opabex3 5749* 
Existence of an ordered pair abstraction. (Contributed by Jeff Madsen,
2Sep2009.)



Theorem  iunex 5750* 
The existence of an indexed union. is normally a freevariable
parameter in the class expression substituted for , which can be
read informally as . (Contributed by NM, 13Oct2003.)



Theorem  abrexex2 5751* 
Existence of an existentially restricted class abstraction. is
normally has freevariable parameters and . See also
abrexex 5744. (Contributed by NM, 12Sep2004.)



Theorem  abexssex 5752* 
Existence of a class abstraction with an existentially quantified
expression. Both and can be
free in .
(Contributed
by NM, 29Jul2006.)



Theorem  abexex 5753* 
A condition where a class builder continues to exist after its wff is
existentially quantified. (Contributed by NM, 4Mar2007.)



Theorem  oprabexd 5754* 
Existence of an operator abstraction. (Contributed by Jeff Madsen,
2Sep2009.)



Theorem  oprabex 5755* 
Existence of an operation class abstraction. (Contributed by NM,
19Oct2004.)



Theorem  oprabex3 5756* 
Existence of an operation class abstraction (special case).
(Contributed by NM, 19Oct2004.)



Theorem  oprabrexex2 5757* 
Existence of an existentially restricted operation abstraction.
(Contributed by Jeff Madsen, 11Jun2010.)



Theorem  ab2rexex 5758* 
Existence of a class abstraction of existentially restricted sets.
Variables and
are normally
freevariable parameters in the
class expression substituted for , which can be thought of as
. See comments for abrexex 5744. (Contributed by NM,
20Sep2011.)



Theorem  ab2rexex2 5759* 
Existence of an existentially restricted class abstraction.
normally has freevariable parameters , , and .
Compare abrexex2 5751. (Contributed by NM, 20Sep2011.)



Theorem  xpexgALT 5760 
The cross product of two sets is a set. Proposition 6.2 of
[TakeutiZaring] p. 23. This
version is proven using Replacement; see
xpexg 4452 for a version that uses the Power Set axiom
instead.
(Contributed by Mario Carneiro, 20May2013.)
(Proof modification is discouraged.) (New usage is discouraged.)



Theorem  offval3 5761* 
General value of with no assumptions on functionality
of and . (Contributed by Stefan
O'Rear, 24Jan2015.)



Theorem  offres 5762 
Pointwise combination commutes with restriction. (Contributed by Stefan
O'Rear, 24Jan2015.)



Theorem  ofmres 5763* 
Equivalent expressions for a restriction of the function operation map.
Unlike which is a proper class,
can be a set by ofmresex 5764, allowing it to be used as a function or
structure argument. By ofmresval 5723, the restricted operation map
values are the same as the original values, allowing theorems for
to be reused. (Contributed by NM, 20Oct2014.)



Theorem  ofmresex 5764 
Existence of a restriction of the function operation map. (Contributed
by NM, 20Oct2014.)



2.6.14 First and second members of an ordered
pair


Syntax  c1st 5765 
Extend the definition of a class to include the first member an ordered
pair function.



Syntax  c2nd 5766 
Extend the definition of a class to include the second member an ordered
pair function.



Definition  df1st 5767 
Define a function that extracts the first member, or abscissa, of an
ordered pair. Theorem op1st 5773 proves that it does this. For example,
( 3 , 4 ) = 3 . Equivalent to Definition
5.13 (i) of
[Monk1] p. 52 (compare op1sta 4802 and op1stb 4209). The notation is the same
as Monk's. (Contributed by NM, 9Oct2004.)



Definition  df2nd 5768 
Define a function that extracts the second member, or ordinate, of an
ordered pair. Theorem op2nd 5774 proves that it does this. For example,
3 , 4 ) = 4 . Equivalent to Definition 5.13 (ii)
of [Monk1] p. 52 (compare op2nda 4805 and op2ndb 4804). The notation is the
same as Monk's. (Contributed by NM, 9Oct2004.)



Theorem  1stvalg 5769 
The value of the function that extracts the first member of an ordered
pair. (Contributed by NM, 9Oct2004.) (Revised by Mario Carneiro,
8Sep2013.)



Theorem  2ndvalg 5770 
The value of the function that extracts the second member of an ordered
pair. (Contributed by NM, 9Oct2004.) (Revised by Mario Carneiro,
8Sep2013.)



Theorem  1st0 5771 
The value of the firstmember function at the empty set. (Contributed by
NM, 23Apr2007.)



Theorem  2nd0 5772 
The value of the secondmember function at the empty set. (Contributed by
NM, 23Apr2007.)



Theorem  op1st 5773 
Extract the first member of an ordered pair. (Contributed by NM,
5Oct2004.)



Theorem  op2nd 5774 
Extract the second member of an ordered pair. (Contributed by NM,
5Oct2004.)



Theorem  op1std 5775 
Extract the first member of an ordered pair. (Contributed by Mario
Carneiro, 31Aug2015.)



Theorem  op2ndd 5776 
Extract the second member of an ordered pair. (Contributed by Mario
Carneiro, 31Aug2015.)



Theorem  op1stg 5777 
Extract the first member of an ordered pair. (Contributed by NM,
19Jul2005.)



Theorem  op2ndg 5778 
Extract the second member of an ordered pair. (Contributed by NM,
19Jul2005.)



Theorem  ot1stg 5779 
Extract the first member of an ordered triple. (Due to infrequent
usage, it isn't worthwhile at this point to define special extractors
for triples, so we reuse the ordered pair extractors for ot1stg 5779,
ot2ndg 5780, ot3rdgg 5781.) (Contributed by NM, 3Apr2015.) (Revised
by
Mario Carneiro, 2May2015.)



Theorem  ot2ndg 5780 
Extract the second member of an ordered triple. (See ot1stg 5779 comment.)
(Contributed by NM, 3Apr2015.) (Revised by Mario Carneiro,
2May2015.)



Theorem  ot3rdgg 5781 
Extract the third member of an ordered triple. (See ot1stg 5779 comment.)
(Contributed by NM, 3Apr2015.)



Theorem  1stval2 5782 
Alternate value of the function that extracts the first member of an
ordered pair. Definition 5.13 (i) of [Monk1] p. 52. (Contributed by
NM, 18Aug2006.)



Theorem  2ndval2 5783 
Alternate value of the function that extracts the second member of an
ordered pair. Definition 5.13 (ii) of [Monk1] p. 52. (Contributed by
NM, 18Aug2006.)



Theorem  fo1st 5784 
The function
maps the universe onto the universe. (Contributed
by NM, 14Oct2004.) (Revised by Mario Carneiro, 8Sep2013.)



Theorem  fo2nd 5785 
The function
maps the universe onto the universe. (Contributed
by NM, 14Oct2004.) (Revised by Mario Carneiro, 8Sep2013.)



Theorem  f1stres 5786 
Mapping of a restriction of the (first member of an ordered
pair) function. (Contributed by NM, 11Oct2004.) (Revised by Mario
Carneiro, 8Sep2013.)



Theorem  f2ndres 5787 
Mapping of a restriction of the (second member of an ordered
pair) function. (Contributed by NM, 7Aug2006.) (Revised by Mario
Carneiro, 8Sep2013.)



Theorem  fo1stresm 5788* 
Onto mapping of a restriction of the (first member of an ordered
pair) function. (Contributed by Jim Kingdon, 24Jan2019.)



Theorem  fo2ndresm 5789* 
Onto mapping of a restriction of the (second member of an
ordered pair) function. (Contributed by Jim Kingdon, 24Jan2019.)



Theorem  1stcof 5790 
Composition of the first member function with another function.
(Contributed by NM, 12Oct2007.)



Theorem  2ndcof 5791 
Composition of the second member function with another function.
(Contributed by FL, 15Oct2012.)



Theorem  xp1st 5792 
Location of the first element of a Cartesian product. (Contributed by
Jeff Madsen, 2Sep2009.)



Theorem  xp2nd 5793 
Location of the second element of a Cartesian product. (Contributed by
Jeff Madsen, 2Sep2009.)



Theorem  1stexg 5794 
Existence of the first member of a set. (Contributed by Jim Kingdon,
26Jan2019.)



Theorem  2ndexg 5795 
Existence of the first member of a set. (Contributed by Jim Kingdon,
26Jan2019.)



Theorem  elxp6 5796 
Membership in a cross product. This version requires no quantifiers or
dummy variables. See also elxp4 4808. (Contributed by NM, 9Oct2004.)



Theorem  elxp7 5797 
Membership in a cross product. This version requires no quantifiers or
dummy variables. See also elxp4 4808. (Contributed by NM, 19Aug2006.)



Theorem  eqopi 5798 
Equality with an ordered pair. (Contributed by NM, 15Dec2008.)
(Revised by Mario Carneiro, 23Feb2014.)



Theorem  xp2 5799* 
Representation of cross product based on ordered pair component
functions. (Contributed by NM, 16Sep2006.)



Theorem  unielxp 5800 
The membership relation for a cross product is inherited by union.
(Contributed by NM, 16Sep2006.)

