Type  Label  Description 
Statement 

Theorem  elxp 4801* 
Membership in a cross product. (Contributed by NM, 4Jul1994.)



Theorem  elxp2 4802* 
Membership in a cross product. (Contributed by NM, 23Feb2004.)



Theorem  xpeq12 4803 
Equality theorem for cross product. (Contributed by FL, 31Aug2009.)



Theorem  xpeq1i 4804 
Equality inference for cross product. (Contributed by NM,
21Dec2008.)



Theorem  xpeq2i 4805 
Equality inference for cross product. (Contributed by NM,
21Dec2008.)



Theorem  xpeq12i 4806 
Equality inference for cross product. (Contributed by FL,
31Aug2009.)



Theorem  xpeq1d 4807 
Equality deduction for cross product. (Contributed by Jeff Madsen,
17Jun2010.)



Theorem  xpeq2d 4808 
Equality deduction for cross product. (Contributed by Jeff Madsen,
17Jun2010.)



Theorem  xpeq12d 4809 
Equality deduction for cross product. (Contributed by NM,
8Dec2013.)



Theorem  nfxp 4810 
Boundvariable hypothesis builder for cross product. (Contributed by
NM, 15Sep2003.) (Revised by Mario Carneiro, 15Oct2016.)



Theorem  opelxp 4811 
Ordered pair membership in a cross product. (The proof was shortened by
Andrew Salmon, 12Aug2011.) (Contributed by NM, 15Nov1994.)
(Revised by set.mm contributors, 12Aug2011.)



Theorem  brxp 4812 
Binary relation on a cross product. (Contributed by NM,
22Apr2004.)



Theorem  csbxpg 4813 
Distribute proper substitution through the cross product of two
classes. (Contributed by Alan Sare, 10Nov2012.)



Theorem  rabxp 4814* 
Membership in a class builder restricted to a cross product.
(Contributed by NM, 20Feb2014.)



Theorem  fconstopab 4815* 
Representation of a constant function using ordered pairs. (Contributed
by NM, 12Oct1999.)



Theorem  vtoclr 4816* 
Variable to class conversion of transitive relation. (Contributed by
NM, 9Jun1998.)



Theorem  xpiundi 4817* 
Distributive law for cross product over indexed union. (Contributed by
set.mm contributors, 26Apr2014.) (Revised by Mario Carneiro,
27Apr2014.)



Theorem  xpiundir 4818* 
Distributive law for cross product over indexed union. (Contributed by
set.mm contributors, 26Apr2014.) (Revised by Mario Carneiro,
27Apr2014.)



Theorem  iunxpconst 4819* 
Membership in a union of cross products when the second factor is
constant. (Contributed by Mario Carneiro, 29Dec2014.)



Theorem  opeliunxp 4820 
Membership in a union of Cartesian products. (Contributed by Mario
Carneiro, 29Dec2014.) (Revised by Mario Carneiro, 1Jan2017.)



Theorem  eliunxp 4821* 
Membership in a union of Cartesian products. Analogue of elxp 4801
for
nonconstant . (Contributed by Mario Carneiro,
29Dec2014.)



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



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



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



Theorem  ralxp 4825* 
Universal quantification restricted to a Cartesian 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 4826* 
Existential quantification restricted to a Cartesian product is
equivalent to a double restricted quantification. (Contributed by NM,
11Nov1995.) (Revised by Mario Carneiro, 14Feb2015.)



Theorem  ralxpf 4827* 
Version of ralxp 4825 with boundvariable hypotheses. (Contributed
by NM,
18Aug2006.) (Revised by set.mm contributors, 20Dec2008.)



Theorem  rexxpf 4828* 
Version of rexxp 4826 with boundvariable hypotheses. (Contributed
by NM,
19Dec2008.)



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



Theorem  brel 4830 
Two things in a binary relation belong to the relation's domain.
(Contributed by NM, 17May1996.)



Theorem  elxp3 4831* 
Membership in a cross product. (Contributed by NM, 5Mar1995.)



Theorem  xpundi 4832 
Distributive law for cross product over union. Theorem 103 of [Suppes]
p. 52. (Contributed by NM, 12Aug2004.)



Theorem  xpundir 4833 
Distributive law for cross product over union. Similar to Theorem 103
of [Suppes] p. 52. (Contributed by NM,
30Sep2002.)



Theorem  xpun 4834 
The cross product of two unions. (Contributed by NM, 12Aug2004.)



Theorem  brinxp2 4835 
Intersection of binary relation with cross product. (Contributed by NM,
3Mar2007.)



Theorem  brinxp 4836 
Intersection of binary relation with cross product. (Contributed by NM,
9Mar1997.)



Theorem  opabssxp 4837* 
An abstraction relation is a subset of a related cross product.
(Contributed by NM, 16Jul1995.)



Theorem  optocl 4838* 
Implicit substitution of class for ordered pair. (Contributed by NM,
5Mar1995.)



Theorem  2optocl 4839* 
Implicit substitution of classes for ordered pairs. (Contributed by NM,
12Mar1995.)



Theorem  3optocl 4840* 
Implicit substitution of classes for ordered pairs. (Contributed by NM,
12Mar1995.)



Theorem  opbrop 4841* 
Ordered pair membership in a relation. Special case. (Contributed by
NM, 5Aug1995.)



Theorem  xp0r 4842 
The cross product with the empty set is empty. Part of Theorem 3.13(ii)
of [Monk1] p. 37. (Contributed by NM,
4Jul1994.)



Theorem  xpvv 4843 
The cross product of the universe with itself is the universe.
(Contributed by Scott Fenton, 14Apr2021.)



Theorem  ssrel 4844* 
A subclass relationship depends only on a relation's ordered pairs.
Theorem 3.2(i) of [Monk1] p. 33. (The
proof was shortened by Andrew
Salmon, 27Aug2011.) (Contributed by NM, 2Aug1994.) (Revised by
set.mm contributors, 27Aug2011.)



Theorem  eqrel 4845* 
Extensionality principle for relations. Theorem 3.2(ii) of [Monk1]
p. 33. (Contributed by NM, 2Aug1994.) (Revised by Scott Fenton,
14Apr2021.)



Theorem  ssopr 4846* 
Subclass principle for operators. (Contributed by Scott Fenton,
19Apr2021.)



Theorem  eqopr 4847* 
Extensionality principle for operators. (Contributed by Scott Fenton,
19Apr2021.)



Theorem  relssi 4848* 
Inference from subclass principle for relations. (Contributed by NM,
31Mar1998.) (Revised by Scott Fenton, 15Apr2021.)



Theorem  relssdv 4849* 
Deduction from subclass principle for relations. (Contributed by set.mm
contributors, 11Sep2004.) (Revised by Scott Fenton, 16Apr2021.)



Theorem  eqrelriv 4850* 
Inference from extensionality principle for relations. (Contributed by
FL, 15Oct2012.) (Revised by Scott Fenton, 16Apr2021.)



Theorem  eqbrriv 4851* 
Inference from extensionality principle for relations. (Contributed by
NM, 12Dec2006.) (Revised by Scott Fenton, 16Apr2021.)



Theorem  eqrelrdv 4852* 
Deduce equality of relations from equivalence of membership.
(Contributed by Rodolfo Medina, 10Oct2010.) (Revised by Scott Fenton,
16Apr2021.)



Theorem  eqoprriv 4853* 
Equality inference for operators. (Contributed by Scott Fenton,
19Apr2021.)



Theorem  eqoprrdv 4854* 
Equality deduction for operators. (Contributed by Scott Fenton,
19Apr2021.)



Theorem  xpss12 4855 
Subset theorem for cross product. Generalization of Theorem 101 of
[Suppes] p. 52. (The proof was shortened
by Andrew Salmon,
27Aug2011.) (Contributed by NM, 26Aug1995.) (Revised by set.mm
contributors, 27Aug2011.)



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



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



Theorem  br1st 4858* 
Binary relationship equivalence for the function. (Contributed
by set.mm contributors, 8Jan2015.)



Theorem  br2nd 4859* 
Binary relationship equivalence for the function. (Contributed
by set.mm contributors, 8Jan2015.)



Theorem  brswap2 4860 
Binary relationship equivalence for the Swap
function.
(Contributed by set.mm contributors, 8Jan2015.)

Swap 

Theorem  opabid2 4861* 
A relation expressed as an ordered pair abstraction. (Contributed by
set.mm contributors, 11Dec2006.)



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



Theorem  inxp 4863 
The intersection of two cross products. Exercise 9 of [TakeutiZaring]
p. 25. (The proof was shortened by Andrew Salmon, 27Aug2011.)
(Contributed by NM, 3Aug1994.) (Revised by set.mm contributors,
27Aug2011.)



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



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



Theorem  opabbi2i 4866* 
Equality of a class variable and an ordered pair abstractions
(inference rule). Compare abbi2i 2464. (Contributed by Scott Fenton,
18Apr2021.)



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



Theorem  ideqg 4868 
For sets, the identity relation is the same as equality. (Contributed
by NM, 30Apr2004.) (Revised by set.mm contributors, 27Aug2011.)



Theorem  ideqg2 4869 
For sets, the identity relation is the same as equality. (Contributed
by SF, 8Jan2015.)



Theorem  ideq 4870 
For sets, the identity relation is the same as equality. (Contributed
by NM, 13Aug1995.) (Revised by set.mm contributors, 1Jun2008.)



Theorem  ididg 4871 
A set is identical to itself. (The proof was shortened by Andrew Salmon,
27Aug2011.) (Contributed by NM, 28May2008.) (Revised by set.mm
contributors, 27Aug2011.)



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



Theorem  coss2 4873 
Subclass theorem for composition. (Contributed by set.mm contributors,
5Apr2013.)



Theorem  coeq1 4874 
Equality theorem for composition of two classes. (Contributed by set.mm
contributors, 3Jan1997.)



Theorem  coeq2 4875 
Equality theorem for composition of two classes. (Contributed by set.mm
contributors, 3Jan1997.)



Theorem  coeq1i 4876 
Equality inference for composition of two classes. (Contributed by
set.mm contributors, 16Nov2000.)



Theorem  coeq2i 4877 
Equality inference for composition of two classes. (Contributed by
set.mm contributors, 16Nov2000.)



Theorem  coeq1d 4878 
Equality deduction for composition of two classes. (Contributed by
set.mm contributors, 16Nov2000.)



Theorem  coeq2d 4879 
Equality deduction for composition of two classes. (Contributed by
set.mm contributors, 16Nov2000.)



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



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



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



Theorem  brco 4883* 
Binary relation on a composition. (Contributed by set.mm contributors,
21Sep2004.)



Theorem  opelco 4884* 
Ordered pair membership in a composition. (The proof was shortened by
Andrew Salmon, 27Aug2011.) (Contributed by set.mm contributors,
27Dec1996.) (Revised by set.mm contributors, 27Aug2011.)



Theorem  cnvss 4885 
Subset theorem for converse. (Contributed by set.mm contributors,
22Mar1998.)



Theorem  cnveq 4886 
Equality theorem for converse. (Contributed by set.mm contributors,
13Aug1995.)



Theorem  cnveqi 4887 
Equality inference for converse. (Contributed by set.mm contributors,
23Dec2008.)



Theorem  cnveqd 4888 
Equality deduction for converse. (Contributed by set.mm contributors,
6Dec2013.)



Theorem  elcnv 4889* 
Membership in a converse. Equation 5 of [Suppes] p. 62. (Contributed
by set.mm contributors, 24Mar1998.)



Theorem  elcnv2 4890* 
Membership in a converse. Equation 5 of [Suppes] p. 62. (Contributed
by set.mm contributors, 11Aug2004.)



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



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



Theorem  opelcnv 4893 
Orderedpair membership in converse. (Contributed by set.mm
contributors, 13Aug1995.)



Theorem  cnvco 4894 
Distributive law of converse over class composition. Theorem 26 of
[Suppes] p. 64. (The proof was shortened
by Andrew Salmon,
27Aug2011.) (Contributed by set.mm contributors, 19Mar1998.)
(Revised by set.mm contributors, 27Aug2011.)



Theorem  cnvuni 4895* 
The converse of a class union is the (indexed) union of the converses of
its members. (Contributed by set.mm contributors, 11Aug2004.)



Theorem  elrn 4896* 
Membership in a range. (Contributed by set.mm contributors,
2Apr2004.)



Theorem  elrn2 4897* 
Membership in a range. (Contributed by set.mm contributors,
10Jul1994.)



Theorem  eldm 4898* 
Membership in a domain. Theorem 4 of [Suppes]
p. 59. (Contributed by
set.mm contributors, 2Apr2004.)



Theorem  eldm2 4899* 
Membership in a domain. Theorem 4 of [Suppes]
p. 59. (Contributed by
set.mm contributors, 1Aug1994.)



Theorem  dfdm2 4900* 
Alternate definition of domain. (Contributed by set.mm contributors,
5Feb2015.)

