Type  Label  Description 
Statement 

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



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



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



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



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



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



Theorem  reliin 4707 
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 4708* 
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 4709* 
The intersection of a class is a relation if at least one member is a
relation. (Contributed by NM, 8Mar2014.)



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



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



Theorem  relopab 4712 
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 4713 
The mapsto notation always describes a relationship. (Contributed by
Scott Fenton, 16Apr2012.)



Theorem  reli 4714 
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 4715 
The membership relation is a relation. (Contributed by NM,
26Apr1998.) (Revised by Mario Carneiro, 21Dec2013.)



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  ralxp 4728* 
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 4729* 
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 4730* 
Disjoint union is a subset of a cross product. (Contributed by Stefan
O'Rear, 21Nov2014.)



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



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



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



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



Theorem  relop 4735* 
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 4736 
For sets, the identity relation is the same as equality. (Contributed
by NM, 30Apr2004.) (Proof shortened by Andrew Salmon,
27Aug2011.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  cnvco 4770 
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 4771* 
The converse of a class union is the (indexed) union of the converses of
its members. (Contributed by NM, 11Aug2004.)



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



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



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



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



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



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



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



Theorem  csbdmg 4779 
Distribute proper substitution through the domain of a class.
(Contributed by Jim Kingdon, 8Dec2018.)



Theorem  eldmg 4780* 
Domain membership. Theorem 4 of [Suppes] p. 59.
(Contributed by Mario
Carneiro, 9Jul2014.)



Theorem  eldm2g 4781* 
Domain membership. Theorem 4 of [Suppes] p. 59.
(Contributed by NM,
27Jan1997.) (Revised by Mario Carneiro, 9Jul2014.)



Theorem  eldm 4782* 
Membership in a domain. Theorem 4 of [Suppes]
p. 59. (Contributed by
NM, 2Apr2004.)



Theorem  eldm2 4783* 
Membership in a domain. Theorem 4 of [Suppes]
p. 59. (Contributed by
NM, 1Aug1994.)



Theorem  dmss 4784 
Subset theorem for domain. (Contributed by NM, 11Aug1994.)



Theorem  dmeq 4785 
Equality theorem for domain. (Contributed by NM, 11Aug1994.)



Theorem  dmeqi 4786 
Equality inference for domain. (Contributed by NM, 4Mar2004.)



Theorem  dmeqd 4787 
Equality deduction for domain. (Contributed by NM, 4Mar2004.)



Theorem  opeldm 4788 
Membership of first of an ordered pair in a domain. (Contributed by NM,
30Jul1995.)



Theorem  breldm 4789 
Membership of first of a binary relation in a domain. (Contributed by
NM, 30Jul1995.)



Theorem  opeldmg 4790 
Membership of first of an ordered pair in a domain. (Contributed by Jim
Kingdon, 9Jul2019.)



Theorem  breldmg 4791 
Membership of first of a binary relation in a domain. (Contributed by
NM, 21Mar2007.)



Theorem  dmun 4792 
The domain of a union is the union of domains. Exercise 56(a) of
[Enderton] p. 65. (Contributed by NM,
12Aug1994.) (Proof shortened
by Andrew Salmon, 27Aug2011.)



Theorem  dmin 4793 
The domain of an intersection belong to the intersection of domains.
Theorem 6 of [Suppes] p. 60.
(Contributed by NM, 15Sep2004.)



Theorem  dmiun 4794 
The domain of an indexed union. (Contributed by Mario Carneiro,
26Apr2016.)



Theorem  dmuni 4795* 
The domain of a union. Part of Exercise 8 of [Enderton] p. 41.
(Contributed by NM, 3Feb2004.)



Theorem  dmopab 4796* 
The domain of a class of ordered pairs. (Contributed by NM,
16May1995.) (Revised by Mario Carneiro, 4Dec2016.)



Theorem  dmopabss 4797* 
Upper bound for the domain of a restricted class of ordered pairs.
(Contributed by NM, 31Jan2004.)



Theorem  dmopab3 4798* 
The domain of a restricted class of ordered pairs. (Contributed by NM,
31Jan2004.)



Theorem  dm0 4799 
The domain of the empty set is empty. Part of Theorem 3.8(v) of [Monk1]
p. 36. (Contributed by NM, 4Jul1994.) (Proof shortened by Andrew
Salmon, 27Aug2011.)



Theorem  dmi 4800 
The domain of the identity relation is the universe. (Contributed by
NM, 30Apr1998.) (Proof shortened by Andrew Salmon, 27Aug2011.)

