Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  dmxpm 4583* 
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 4584* 
The domain of the intersection of two square cross products. Unlike
dmin 4571, equality holds. (Contributed by NM,
29Jan2008.)



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



Theorem  dmcnvcnv 4586 
The domain of the double converse of a class (which doesn't have to be a
relation as in dfrel2 4799). (Contributed by NM, 8Apr2007.)



Theorem  rncnvcnv 4587 
The range of the double converse of a class. (Contributed by NM,
8Apr2007.)



Theorem  elreldm 4588 
The first member of an ordered pair in a relation belongs to the domain
of the relation. (Contributed by NM, 28Jul2004.)



Theorem  rneq 4589 
Equality theorem for range. (Contributed by NM, 29Dec1996.)



Theorem  rneqi 4590 
Equality inference for range. (Contributed by NM, 4Mar2004.)



Theorem  rneqd 4591 
Equality deduction for range. (Contributed by NM, 4Mar2004.)



Theorem  rnss 4592 
Subset theorem for range. (Contributed by NM, 22Mar1998.)



Theorem  brelrng 4593 
The second argument of a binary relation belongs to its range.
(Contributed by NM, 29Jun2008.)



Theorem  opelrng 4594 
Membership of second member of an ordered pair in a range. (Contributed
by Jim Kingdon, 26Jan2019.)



Theorem  brelrn 4595 
The second argument of a binary relation belongs to its range.
(Contributed by NM, 13Aug2004.)



Theorem  opelrn 4596 
Membership of second member of an ordered pair in a range. (Contributed
by NM, 23Feb1997.)



Theorem  releldm 4597 
The first argument of a binary relation belongs to its domain.
(Contributed by NM, 2Jul2008.)



Theorem  relelrn 4598 
The second argument of a binary relation belongs to its range.
(Contributed by NM, 2Jul2008.)



Theorem  releldmb 4599* 
Membership in a domain. (Contributed by Mario Carneiro, 5Nov2015.)



Theorem  relelrnb 4600* 
Membership in a range. (Contributed by Mario Carneiro, 5Nov2015.)

