Type  Label  Description 
Statement 

Theorem  f1dmex 5901 
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 5902* 
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 5536, funex 5534, fnex 5533, resfunexg 5532, and
funimaexg 5111. See also abrexex2 5909. (Contributed by NM, 16Oct2003.)
(Proof shortened by Mario Carneiro, 31Aug2015.)



Theorem  abrexexg 5903* 
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 5904* 
The existence of an indexed union. is normally a freevariable
parameter in .
(Contributed by NM, 23Mar2006.)



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



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



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



Theorem  iunex 5908* 
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 5909* 
Existence of an existentially restricted class abstraction. is
normally has freevariable parameters and . See also
abrexex 5902. (Contributed by NM, 12Sep2004.)



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



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



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



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



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



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



Theorem  ab2rexex 5916* 
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 5902. (Contributed by NM,
20Sep2011.)



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



Theorem  xpexgALT 5918 
The cross product of two sets is a set. Proposition 6.2 of
[TakeutiZaring] p. 23. This
version is proven using Replacement; see
xpexg 4565 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 5919* 
General value of with no assumptions on functionality
of and . (Contributed by Stefan
O'Rear, 24Jan2015.)



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



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



Theorem  ofmresex 5922 
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 5923 
Extend the definition of a class to include the first member an ordered
pair function.



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



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



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



Theorem  1stvalg 5927 
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 5928 
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 5929 
The value of the firstmember function at the empty set. (Contributed by
NM, 23Apr2007.)



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



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



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



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



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



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



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



Theorem  ot1stg 5937 
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 5937,
ot2ndg 5938, ot3rdgg 5939.) (Contributed by NM, 3Apr2015.) (Revised
by
Mario Carneiro, 2May2015.)



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



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



Theorem  1stval2 5940 
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 5941 
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 5942 
The function
maps the universe onto the universe. (Contributed
by NM, 14Oct2004.) (Revised by Mario Carneiro, 8Sep2013.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  1st2nd2 5959 
Reconstruction of a member of a cross product in terms of its ordered pair
components. (Contributed by NM, 20Oct2013.)



Theorem  xpopth 5960 
An ordered pair theorem for members of cross products. (Contributed by
NM, 20Jun2007.)



Theorem  eqop 5961 
Two ways to express equality with an ordered pair. (Contributed by NM,
3Sep2007.) (Proof shortened by Mario Carneiro, 26Apr2015.)



Theorem  eqop2 5962 
Two ways to express equality with an ordered pair. (Contributed by NM,
25Feb2014.)



Theorem  op1steq 5963* 
Two ways of expressing that an element is the first member of an ordered
pair. (Contributed by NM, 22Sep2013.) (Revised by Mario Carneiro,
23Feb2014.)



Theorem  2nd1st 5964 
Swap the members of an ordered pair. (Contributed by NM, 31Dec2014.)



Theorem  1st2nd 5965 
Reconstruction of a member of a relation in terms of its ordered pair
components. (Contributed by NM, 29Aug2006.)



Theorem  1stdm 5966 
The first ordered pair component of a member of a relation belongs to the
domain of the relation. (Contributed by NM, 17Sep2006.)



Theorem  2ndrn 5967 
The second ordered pair component of a member of a relation belongs to the
range of the relation. (Contributed by NM, 17Sep2006.)



Theorem  1st2ndbr 5968 
Express an element of a relation as a relationship between first and
second components. (Contributed by Mario Carneiro, 22Jun2016.)



Theorem  releldm2 5969* 
Two ways of expressing membership in the domain of a relation.
(Contributed by NM, 22Sep2013.)



Theorem  reldm 5970* 
An expression for the domain of a relation. (Contributed by NM,
22Sep2013.)



Theorem  sbcopeq1a 5971 
Equality theorem for substitution of a class for an ordered pair (analog
of sbceq1a 2850 that avoids the existential quantifiers of copsexg 4080).
(Contributed by NM, 19Aug2006.) (Revised by Mario Carneiro,
31Aug2015.)



Theorem  csbopeq1a 5972 
Equality theorem for substitution of a class for an ordered pair
in (analog of csbeq1a 2942). (Contributed by NM,
19Aug2006.) (Revised by Mario Carneiro, 31Aug2015.)



Theorem  dfopab2 5973* 
A way to define an orderedpair class abstraction without using
existential quantifiers. (Contributed by NM, 18Aug2006.) (Revised by
Mario Carneiro, 31Aug2015.)



Theorem  dfoprab3s 5974* 
A way to define an operation class abstraction without using existential
quantifiers. (Contributed by NM, 18Aug2006.) (Revised by Mario
Carneiro, 31Aug2015.)



Theorem  dfoprab3 5975* 
Operation class abstraction expressed without existential quantifiers.
(Contributed by NM, 16Dec2008.)



Theorem  dfoprab4 5976* 
Operation class abstraction expressed without existential quantifiers.
(Contributed by NM, 3Sep2007.) (Revised by Mario Carneiro,
31Aug2015.)



Theorem  dfoprab4f 5977* 
Operation class abstraction expressed without existential quantifiers.
(Unnecessary distinct variable restrictions were removed by David
Abernethy, 19Jun2012.) (Contributed by NM, 20Dec2008.) (Revised by
Mario Carneiro, 31Aug2015.)



Theorem  dfxp3 5978* 
Define the cross product of three classes. Compare dfxp 4458.
(Contributed by FL, 6Nov2013.) (Proof shortened by Mario Carneiro,
3Nov2015.)



Theorem  elopabi 5979* 
A consequence of membership in an orderedpair class abstraction, using
ordered pair extractors. (Contributed by NM, 29Aug2006.)



Theorem  eloprabi 5980* 
A consequence of membership in an operation class abstraction, using
ordered pair extractors. (Contributed by NM, 6Nov2006.) (Revised by
David Abernethy, 19Jun2012.)



Theorem  mpt2mptsx 5981* 
Express a twoargument function as a oneargument function, or
viceversa. (Contributed by Mario Carneiro, 24Dec2016.)



Theorem  mpt2mpts 5982* 
Express a twoargument function as a oneargument function, or
viceversa. (Contributed by Mario Carneiro, 24Sep2015.)



Theorem  dmmpt2ssx 5983* 
The domain of a mapping is a subset of its base class. (Contributed by
Mario Carneiro, 9Feb2015.)



Theorem  fmpt2x 5984* 
Functionality, domain and codomain of a class given by the mapsto
notation, where is not constant but depends on .
(Contributed by NM, 29Dec2014.)



Theorem  fmpt2 5985* 
Functionality, domain and range of a class given by the mapsto
notation. (Contributed by FL, 17May2010.)



Theorem  fnmpt2 5986* 
Functionality and domain of a class given by the mapsto notation.
(Contributed by FL, 17May2010.)



Theorem  mpt2fvex 5987* 
Sufficient condition for an operation mapsto notation to be setlike.
(Contributed by Mario Carneiro, 3Jul2019.)



Theorem  fnmpt2i 5988* 
Functionality and domain of a class given by the mapsto notation.
(Contributed by FL, 17May2010.)



Theorem  dmmpt2 5989* 
Domain of a class given by the mapsto notation. (Contributed by FL,
17May2010.)



Theorem  mpt2fvexi 5990* 
Sufficient condition for an operation mapsto notation to be setlike.
(Contributed by Mario Carneiro, 3Jul2019.)



Theorem  mpt2exxg 5991* 
Existence of an operation class abstraction (version for dependent
domains). (Contributed by Mario Carneiro, 30Dec2016.)



Theorem  mpt2exg 5992* 
Existence of an operation class abstraction (special case).
(Contributed by FL, 17May2010.) (Revised by Mario Carneiro,
1Sep2015.)



Theorem  mpt2exga 5993* 
If the domain of a function given by mapsto notation is a set, the
function is a set. (Contributed by NM, 12Sep2011.)



Theorem  mpt2ex 5994* 
If the domain of a function given by mapsto notation is a set, the
function is a set. (Contributed by Mario Carneiro, 20Dec2013.)



Theorem  fmpt2co 5995* 
Composition of two functions. Variation of fmptco 5478 when the second
function has two arguments. (Contributed by Mario Carneiro,
8Feb2015.)



Theorem  oprabco 5996* 
Composition of a function with an operator abstraction. (Contributed by
Jeff Madsen, 2Sep2009.) (Proof shortened by Mario Carneiro,
26Sep2015.)



Theorem  oprab2co 5997* 
Composition of operator abstractions. (Contributed by Jeff Madsen,
2Sep2009.) (Revised by David Abernethy, 23Apr2013.)



Theorem  df1st2 5998* 
An alternate possible definition of the function. (Contributed
by NM, 14Oct2004.) (Revised by Mario Carneiro, 31Aug2015.)



Theorem  df2nd2 5999* 
An alternate possible definition of the function. (Contributed
by NM, 10Aug2006.) (Revised by Mario Carneiro, 31Aug2015.)



Theorem  1stconst 6000 
The mapping of a restriction of the function to a constant
function. (Contributed by NM, 14Dec2008.)

