Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  dmun 4485 
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 4486 
The domain of an intersection belong to the intersection of domains.
Theorem 6 of [Suppes] p. 60.
(Contributed by NM, 15Sep2004.)



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



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



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



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



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



Theorem  dm0 4492 
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 4493 
The domain of the identity relation is the universe. (Contributed by
NM, 30Apr1998.) (Proof shortened by Andrew Salmon, 27Aug2011.)



Theorem  dmv 4494 
The domain of the universe is the universe. (Contributed by NM,
8Aug2003.)



Theorem  dm0rn0 4495 
An empty domain implies an empty range. (Contributed by NM,
21May1998.)



Theorem  reldm0 4496 
A relation is empty iff its domain is empty. (Contributed by NM,
15Sep2004.)



Theorem  dmmrnm 4497* 
A domain is inhabited if and only if the range is inhabited.
(Contributed by Jim Kingdon, 15Dec2018.)



Theorem  dmxpm 4498* 
The domain of a cross product. Part of Theorem 3.13(x) of [Monk1]
p. 37. (Contributed by NM, 28Jul1995.) (Proof shortened by Andrew
Salmon, 27Aug2011.)



Theorem  dmxpinm 4499* 
The domain of the intersection of two square cross products. Unlike
dmin 4486, equality holds. (Contributed by NM,
29Jan2008.)



Theorem  xpid11m 4500* 
The cross product of a class with itself is onetoone. (Contributed by
Jim Kingdon, 8Dec2018.)

