Type  Label  Description 
Statement 

Theorem  eqrelriiv 4601* 
Inference from extensionality principle for relations. (Contributed by
NM, 17Mar1995.)



Theorem  eqbrriv 4602* 
Inference from extensionality principle for relations. (Contributed by
NM, 12Dec2006.)



Theorem  eqrelrdv 4603* 
Deduce equality of relations from equivalence of membership.
(Contributed by Rodolfo Medina, 10Oct2010.)



Theorem  eqbrrdv 4604* 
Deduction from extensionality principle for relations. (Contributed by
Mario Carneiro, 3Jan2017.)



Theorem  eqbrrdiv 4605* 
Deduction from extensionality principle for relations. (Contributed by
Rodolfo Medina, 10Oct2010.)



Theorem  eqrelrdv2 4606* 
A version of eqrelrdv 4603. (Contributed by Rodolfo Medina,
10Oct2010.)



Theorem  ssrelrel 4607* 
A subclass relationship determined by ordered triples. Use relrelss 5033
to express the antecedent in terms of the relation predicate.
(Contributed by NM, 17Dec2008.) (Proof shortened by Andrew Salmon,
27Aug2011.)



Theorem  eqrelrel 4608* 
Extensionality principle for ordered triples, analogous to eqrel 4596.
Use relrelss 5033 to express the antecedent in terms of the
relation
predicate. (Contributed by NM, 17Dec2008.)



Theorem  elrel 4609* 
A member of a relation is an ordered pair. (Contributed by NM,
17Sep2006.)



Theorem  relsng 4610 
A singleton is a relation iff it is an ordered pair. (Contributed by NM,
24Sep2013.) (Revised by BJ, 12Feb2022.)



Theorem  relsnopg 4611 
A singleton of an ordered pair is a relation. (Contributed by NM,
17May1998.) (Revised by BJ, 12Feb2022.)



Theorem  relsn 4612 
A singleton is a relation iff it is an ordered pair. (Contributed by
NM, 24Sep2013.)



Theorem  relsnop 4613 
A singleton of an ordered pair is a relation. (Contributed by NM,
17May1998.) (Revised by Mario Carneiro, 26Apr2015.)



Theorem  xpss12 4614 
Subset theorem for cross product. Generalization of Theorem 101 of
[Suppes] p. 52. (Contributed by NM,
26Aug1995.) (Proof shortened by
Andrew Salmon, 27Aug2011.)



Theorem  xpss 4615 
A cross product is included in the ordered pair universe. Exercise 3 of
[TakeutiZaring] p. 25. (Contributed
by NM, 2Aug1994.)



Theorem  relxp 4616 
A cross product is a relation. Theorem 3.13(i) of [Monk1] p. 37.
(Contributed by NM, 2Aug1994.)



Theorem  xpss1 4617 
Subset relation for cross product. (Contributed by Jeff Hankins,
30Aug2009.)



Theorem  xpss2 4618 
Subset relation for cross product. (Contributed by Jeff Hankins,
30Aug2009.)



Theorem  xpsspw 4619 
A cross product is included in the power of the power of the union of
its arguments. (Contributed by NM, 13Sep2006.)



Theorem  unixpss 4620 
The double class union of a cross product is included in the union of its
arguments. (Contributed by NM, 16Sep2006.)



Theorem  xpexg 4621 
The cross product of two sets is a set. Proposition 6.2 of
[TakeutiZaring] p. 23. (Contributed
by NM, 14Aug1994.)



Theorem  xpex 4622 
The cross product of two sets is a set. Proposition 6.2 of
[TakeutiZaring] p. 23.
(Contributed by NM, 14Aug1994.)



Theorem  sqxpexg 4623 
The Cartesian square of a set is a set. (Contributed by AV,
13Jan2020.)



Theorem  relun 4624 
The union of two relations is a relation. Compare Exercise 5 of
[TakeutiZaring] p. 25. (Contributed
by NM, 12Aug1994.)



Theorem  relin1 4625 
The intersection with a relation is a relation. (Contributed by NM,
16Aug1994.)



Theorem  relin2 4626 
The intersection with a relation is a relation. (Contributed by NM,
17Jan2006.)



Theorem  reldif 4627 
A difference cutting down a relation is a relation. (Contributed by NM,
31Mar1998.)



Theorem  reliun 4628 
An indexed union is a relation iff each member of its indexed family is
a relation. (Contributed by NM, 19Dec2008.)



Theorem  reliin 4629 
An indexed intersection is a relation if at least one of the member of the
indexed family is a relation. (Contributed by NM, 8Mar2014.)



Theorem  reluni 4630* 
The union of a class is a relation iff any member is a relation.
Exercise 6 of [TakeutiZaring] p.
25 and its converse. (Contributed by
NM, 13Aug2004.)



Theorem  relint 4631* 
The intersection of a class is a relation if at least one member is a
relation. (Contributed by NM, 8Mar2014.)



Theorem  rel0 4632 
The empty set is a relation. (Contributed by NM, 26Apr1998.)



Theorem  relopabi 4633 
A class of ordered pairs is a relation. (Contributed by Mario Carneiro,
21Dec2013.)



Theorem  relopab 4634 
A class of ordered pairs is a relation. (Contributed by NM, 8Mar1995.)
(Unnecessary distinct variable restrictions were removed by Alan Sare,
9Jul2013.) (Proof shortened by Mario Carneiro, 21Dec2013.)



Theorem  mptrel 4635 
The mapsto notation always describes a relationship. (Contributed by
Scott Fenton, 16Apr2012.)



Theorem  reli 4636 
The identity relation is a relation. Part of Exercise 4.12(p) of
[Mendelson] p. 235. (Contributed by
NM, 26Apr1998.) (Revised by
Mario Carneiro, 21Dec2013.)



Theorem  rele 4637 
The membership relation is a relation. (Contributed by NM,
26Apr1998.) (Revised by Mario Carneiro, 21Dec2013.)



Theorem  opabid2 4638* 
A relation expressed as an ordered pair abstraction. (Contributed by
NM, 11Dec2006.)



Theorem  inopab 4639* 
Intersection of two ordered pair class abstractions. (Contributed by
NM, 30Sep2002.)



Theorem  difopab 4640* 
The difference of two orderedpair abstractions. (Contributed by Stefan
O'Rear, 17Jan2015.)



Theorem  inxp 4641 
The intersection of two cross products. Exercise 9 of [TakeutiZaring]
p. 25. (Contributed by NM, 3Aug1994.) (Proof shortened by Andrew
Salmon, 27Aug2011.)



Theorem  xpindi 4642 
Distributive law for cross product over intersection. Theorem 102 of
[Suppes] p. 52. (Contributed by NM,
26Sep2004.)



Theorem  xpindir 4643 
Distributive law for cross product over intersection. Similar to
Theorem 102 of [Suppes] p. 52.
(Contributed by NM, 26Sep2004.)



Theorem  xpiindim 4644* 
Distributive law for cross product over indexed intersection.
(Contributed by Jim Kingdon, 7Dec2018.)



Theorem  xpriindim 4645* 
Distributive law for cross product over relativized indexed
intersection. (Contributed by Jim Kingdon, 7Dec2018.)



Theorem  eliunxp 4646* 
Membership in a union of cross products. Analogue of elxp 4524
for
nonconstant . (Contributed by Mario Carneiro,
29Dec2014.)



Theorem  opeliunxp2 4647* 
Membership in a union of cross products. (Contributed by Mario
Carneiro, 14Feb2015.)



Theorem  raliunxp 4648* 
Write a double restricted quantification as one universal quantifier.
In this version of ralxp 4650, is not assumed to be constant.
(Contributed by Mario Carneiro, 29Dec2014.)



Theorem  rexiunxp 4649* 
Write a double restricted quantification as one universal quantifier.
In this version of rexxp 4651, is not assumed to be constant.
(Contributed by Mario Carneiro, 14Feb2015.)



Theorem  ralxp 4650* 
Universal quantification restricted to a cross product is equivalent to
a double restricted quantification. The hypothesis specifies an
implicit substitution. (Contributed by NM, 7Feb2004.) (Revised by
Mario Carneiro, 29Dec2014.)



Theorem  rexxp 4651* 
Existential quantification restricted to a cross product is equivalent
to a double restricted quantification. (Contributed by NM,
11Nov1995.) (Revised by Mario Carneiro, 14Feb2015.)



Theorem  djussxp 4652* 
Disjoint union is a subset of a cross product. (Contributed by Stefan
O'Rear, 21Nov2014.)



Theorem  ralxpf 4653* 
Version of ralxp 4650 with boundvariable hypotheses. (Contributed
by NM,
18Aug2006.) (Revised by Mario Carneiro, 15Oct2016.)



Theorem  rexxpf 4654* 
Version of rexxp 4651 with boundvariable hypotheses. (Contributed
by NM,
19Dec2008.) (Revised by Mario Carneiro, 15Oct2016.)



Theorem  iunxpf 4655* 
Indexed union on a cross product is equals a double indexed union. The
hypothesis specifies an implicit substitution. (Contributed by NM,
19Dec2008.)



Theorem  opabbi2dv 4656* 
Deduce equality of a relation and an orderedpair class builder.
Compare abbi2dv 2234. (Contributed by NM, 24Feb2014.)



Theorem  relop 4657* 
A necessary and sufficient condition for a Kuratowski ordered pair to be
a relation. (Contributed by NM, 3Jun2008.) (Avoid depending on this
detail.)



Theorem  ideqg 4658 
For sets, the identity relation is the same as equality. (Contributed
by NM, 30Apr2004.) (Proof shortened by Andrew Salmon,
27Aug2011.)



Theorem  ideq 4659 
For sets, the identity relation is the same as equality. (Contributed
by NM, 13Aug1995.)



Theorem  ididg 4660 
A set is identical to itself. (Contributed by NM, 28May2008.) (Proof
shortened by Andrew Salmon, 27Aug2011.)



Theorem  issetid 4661 
Two ways of expressing set existence. (Contributed by NM, 16Feb2008.)
(Proof shortened by Andrew Salmon, 27Aug2011.) (Revised by Mario
Carneiro, 26Apr2015.)



Theorem  coss1 4662 
Subclass theorem for composition. (Contributed by FL, 30Dec2010.)



Theorem  coss2 4663 
Subclass theorem for composition. (Contributed by NM, 5Apr2013.)



Theorem  coeq1 4664 
Equality theorem for composition of two classes. (Contributed by NM,
3Jan1997.)



Theorem  coeq2 4665 
Equality theorem for composition of two classes. (Contributed by NM,
3Jan1997.)



Theorem  coeq1i 4666 
Equality inference for composition of two classes. (Contributed by NM,
16Nov2000.)



Theorem  coeq2i 4667 
Equality inference for composition of two classes. (Contributed by NM,
16Nov2000.)



Theorem  coeq1d 4668 
Equality deduction for composition of two classes. (Contributed by NM,
16Nov2000.)



Theorem  coeq2d 4669 
Equality deduction for composition of two classes. (Contributed by NM,
16Nov2000.)



Theorem  coeq12i 4670 
Equality inference for composition of two classes. (Contributed by FL,
7Jun2012.)



Theorem  coeq12d 4671 
Equality deduction for composition of two classes. (Contributed by FL,
7Jun2012.)



Theorem  nfco 4672 
Boundvariable hypothesis builder for function value. (Contributed by
NM, 1Sep1999.)



Theorem  elco 4673* 
Elements of a composed relation. (Contributed by BJ, 10Jul2022.)



Theorem  brcog 4674* 
Ordered pair membership in a composition. (Contributed by NM,
24Feb2015.)



Theorem  opelco2g 4675* 
Ordered pair membership in a composition. (Contributed by NM,
27Jan1997.) (Revised by Mario Carneiro, 24Feb2015.)



Theorem  brcogw 4676 
Ordered pair membership in a composition. (Contributed by Thierry
Arnoux, 14Jan2018.)



Theorem  eqbrrdva 4677* 
Deduction from extensionality principle for relations, given an
equivalence only on the relation's domain and range. (Contributed by
Thierry Arnoux, 28Nov2017.)



Theorem  brco 4678* 
Binary relation on a composition. (Contributed by NM, 21Sep2004.)
(Revised by Mario Carneiro, 24Feb2015.)



Theorem  opelco 4679* 
Ordered pair membership in a composition. (Contributed by NM,
27Dec1996.) (Revised by Mario Carneiro, 24Feb2015.)



Theorem  cnvss 4680 
Subset theorem for converse. (Contributed by NM, 22Mar1998.)



Theorem  cnveq 4681 
Equality theorem for converse. (Contributed by NM, 13Aug1995.)



Theorem  cnveqi 4682 
Equality inference for converse. (Contributed by NM, 23Dec2008.)



Theorem  cnveqd 4683 
Equality deduction for converse. (Contributed by NM, 6Dec2013.)



Theorem  elcnv 4684* 
Membership in a converse. Equation 5 of [Suppes] p. 62. (Contributed
by NM, 24Mar1998.)



Theorem  elcnv2 4685* 
Membership in a converse. Equation 5 of [Suppes] p. 62. (Contributed
by NM, 11Aug2004.)



Theorem  nfcnv 4686 
Boundvariable hypothesis builder for converse. (Contributed by NM,
31Jan2004.) (Revised by Mario Carneiro, 15Oct2016.)



Theorem  opelcnvg 4687 
Orderedpair membership in converse. (Contributed by NM, 13May1999.)
(Proof shortened by Andrew Salmon, 27Aug2011.)



Theorem  brcnvg 4688 
The converse of a binary relation swaps arguments. Theorem 11 of [Suppes]
p. 61. (Contributed by NM, 10Oct2005.)



Theorem  opelcnv 4689 
Orderedpair membership in converse. (Contributed by NM,
13Aug1995.)



Theorem  brcnv 4690 
The converse of a binary relation swaps arguments. Theorem 11 of
[Suppes] p. 61. (Contributed by NM,
13Aug1995.)



Theorem  csbcnvg 4691 
Move class substitution in and out of the converse of a function.
(Contributed by Thierry Arnoux, 8Feb2017.)



Theorem  cnvco 4692 
Distributive law of converse over class composition. Theorem 26 of
[Suppes] p. 64. (Contributed by NM,
19Mar1998.) (Proof shortened by
Andrew Salmon, 27Aug2011.)



Theorem  cnvuni 4693* 
The converse of a class union is the (indexed) union of the converses of
its members. (Contributed by NM, 11Aug2004.)



Theorem  dfdm3 4694* 
Alternate definition of domain. Definition 6.5(1) of [TakeutiZaring]
p. 24. (Contributed by NM, 28Dec1996.)



Theorem  dfrn2 4695* 
Alternate definition of range. Definition 4 of [Suppes] p. 60.
(Contributed by NM, 27Dec1996.)



Theorem  dfrn3 4696* 
Alternate definition of range. Definition 6.5(2) of [TakeutiZaring]
p. 24. (Contributed by NM, 28Dec1996.)



Theorem  elrn2g 4697* 
Membership in a range. (Contributed by Scott Fenton, 2Feb2011.)



Theorem  elrng 4698* 
Membership in a range. (Contributed by Scott Fenton, 2Feb2011.)



Theorem  dfdm4 4699 
Alternate definition of domain. (Contributed by NM, 28Dec1996.)



Theorem  dfdmf 4700* 
Definition of domain, using boundvariable hypotheses instead of
distinct variable conditions. (Contributed by NM, 8Mar1995.)
(Revised by Mario Carneiro, 15Oct2016.)

