Theorem List for Intuitionistic Logic Explorer - 4601-4700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | elxp3 4601* |
Membership in a cross product. (Contributed by NM, 5-Mar-1995.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![(
(](lp.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | opeliunxp 4602 |
Membership in a union of cross products. (Contributed by Mario
Carneiro, 29-Dec-2014.) (Revised by Mario Carneiro, 1-Jan-2017.)
|
![( (](lp.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![C C](_cc.gif) ![U_ U_](_cupbar.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![B B](_cb.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | xpundi 4603 |
Distributive law for cross product over union. Theorem 103 of [Suppes]
p. 52. (Contributed by NM, 12-Aug-2004.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | xpundir 4604 |
Distributive law for cross product over union. Similar to Theorem 103
of [Suppes] p. 52. (Contributed by NM,
30-Sep-2002.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | xpiundi 4605* |
Distributive law for cross product over indexed union. (Contributed by
Mario Carneiro, 27-Apr-2014.)
|
![( (](lp.gif) ![U_ U_](_cupbar.gif)
![B B](_cb.gif)
![U_ U_](_cupbar.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | xpiundir 4606* |
Distributive law for cross product over indexed union. (Contributed by
Mario Carneiro, 27-Apr-2014.)
|
![( (](lp.gif) ![U_ U_](_cupbar.gif) ![C C](_cc.gif)
![U_ U_](_cupbar.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | iunxpconst 4607* |
Membership in a union of cross products when the second factor is
constant. (Contributed by Mario Carneiro, 29-Dec-2014.)
|
![U_ U_](_cupbar.gif)
![( (](lp.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![B B](_cb.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | xpun 4608 |
The cross product of two unions. (Contributed by NM, 12-Aug-2004.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif)
![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | elvv 4609* |
Membership in universal class of ordered pairs. (Contributed by NM,
4-Jul-1994.)
|
![( (](lp.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![E. E.](exists.gif)
![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![) )](rp.gif) |
|
Theorem | elvvv 4610* |
Membership in universal class of ordered triples. (Contributed by NM,
17-Dec-2008.)
|
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![_V _V](rmcv.gif) ![_V _V](rmcv.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![E. E.](exists.gif)
![<. <.](langle.gif) ![<.
<.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![z z](_z.gif) ![>. >.](rangle.gif) ![) )](rp.gif) |
|
Theorem | elvvuni 4611 |
An ordered pair contains its union. (Contributed by NM,
16-Sep-2006.)
|
![( (](lp.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![U. U.](bigcup.gif)
![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | mosubopt 4612* |
"At most one" remains true inside ordered pair quantification.
(Contributed by NM, 28-Aug-2007.)
|
![( (](lp.gif) ![A. A.](forall.gif) ![y y](_y.gif) ![A. A.](forall.gif) ![z z](_z.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![E. E.](exists.gif) ![z z](_z.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![y y](_y.gif) ![z z](_z.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | mosubop 4613* |
"At most one" remains true inside ordered pair quantification.
(Contributed by NM, 28-May-1995.)
|
![E*
E*](_em1.gif) ![x x](_x.gif) ![E*
E*](_em1.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![E. E.](exists.gif) ![z z](_z.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![y y](_y.gif) ![z z](_z.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
|
Theorem | brinxp2 4614 |
Intersection of binary relation with cross product. (Contributed by NM,
3-Mar-2007.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | brinxp 4615 |
Intersection of binary relation with cross product. (Contributed by NM,
9-Mar-1997.)
|
![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif)
![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | poinxp 4616 |
Intersection of partial order with cross product of its field.
(Contributed by Mario Carneiro, 10-Jul-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | soinxp 4617 |
Intersection of linear order with cross product of its field.
(Contributed by Mario Carneiro, 10-Jul-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | seinxp 4618 |
Intersection of set-like relation with cross product of its field.
(Contributed by Mario Carneiro, 22-Jun-2015.)
|
![( (](lp.gif) Se ![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif) Se ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | posng 4619 |
Partial ordering of a singleton. (Contributed by Jim Kingdon,
5-Dec-2018.)
|
![( (](lp.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![A A](_ca.gif)
![A A](_ca.gif) ![R R](_cr.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sosng 4620 |
Strict linear ordering on a singleton. (Contributed by Jim Kingdon,
5-Dec-2018.)
|
![( (](lp.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![A A](_ca.gif)
![A A](_ca.gif) ![R R](_cr.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | opabssxp 4621* |
An abstraction relation is a subset of a related cross product.
(Contributed by NM, 16-Jul-1995.)
|
![{
{](lbrace.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | brab2ga 4622* |
The law of concretion for a binary relation. See brab2a 4600 for alternate
proof. TODO: should one of them be deleted? (Contributed by Mario
Carneiro, 28-Apr-2015.) (Proof modification is discouraged.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | optocl 4623* |
Implicit substitution of class for ordered pair. (Contributed by NM,
5-Mar-1995.)
|
![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif)
![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![ph ph](_varphi.gif) ![( (](lp.gif)
![ps ps](_psi.gif) ![) )](rp.gif) |
|
Theorem | 2optocl 4624* |
Implicit substitution of classes for ordered pairs. (Contributed by NM,
12-Mar-1995.)
|
![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif)
![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif)
![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif)
![D D](_cd.gif) ![) )](rp.gif)
![ph ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![R R](_cr.gif) ![ch ch](_chi.gif) ![) )](rp.gif) |
|
Theorem | 3optocl 4625* |
Implicit substitution of classes for ordered pairs. (Contributed by NM,
12-Mar-1995.)
|
![( (](lp.gif) ![F F](_cf.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif)
![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif)
![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif)
![( (](lp.gif) ![th th](_theta.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![F F](_cf.gif) ![( (](lp.gif)
![F F](_cf.gif) ![( (](lp.gif) ![F F](_cf.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![R R](_cr.gif) ![th th](_theta.gif) ![) )](rp.gif) |
|
Theorem | opbrop 4626* |
Ordered pair membership in a relation. Special case. (Contributed by
NM, 5-Aug-1995.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif)
![D D](_cd.gif) ![) )](rp.gif)
![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![z z](_z.gif) ![E. E.](exists.gif) ![w w](_w.gif) ![E. E.](exists.gif) ![v v](_v.gif) ![E. E.](exists.gif) ![u u](_u.gif) ![( (](lp.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![<. <.](langle.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![>. >.](rangle.gif) ![R R](_cr.gif) ![<. <.](langle.gif) ![C C](_cc.gif) ![D D](_cd.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | 0xp 4627 |
The cross product with the empty set is empty. Part of Theorem 3.13(ii)
of [Monk1] p. 37. (Contributed by NM,
4-Jul-1994.)
|
![( (](lp.gif)
![A A](_ca.gif) ![(/) (/)](varnothing.gif) |
|
Theorem | csbxpg 4628 |
Distribute proper substitution through the cross product of two classes.
(Contributed by Alan Sare, 10-Nov-2012.)
|
![( (](lp.gif) ![[_
[_](_ulbrack.gif) ![x x](_x.gif) ![]_ ]_](_urbrack.gif) ![( (](lp.gif) ![C C](_cc.gif)
![( (](lp.gif) ![[_ [_](_ulbrack.gif) ![x x](_x.gif) ![]_ ]_](_urbrack.gif) ![[_ [_](_ulbrack.gif) ![x x](_x.gif) ![]_ ]_](_urbrack.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | releq 4629 |
Equality theorem for the relation predicate. (Contributed by NM,
1-Aug-1994.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | releqi 4630 |
Equality inference for the relation predicate. (Contributed by NM,
8-Dec-2006.)
|
![( (](lp.gif) ![B
B](_cb.gif) ![) )](rp.gif) |
|
Theorem | releqd 4631 |
Equality deduction for the relation predicate. (Contributed by NM,
8-Mar-2014.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | nfrel 4632 |
Bound-variable hypothesis builder for a relation. (Contributed by NM,
31-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
|
![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![F/
F/](finv.gif) ![x x](_x.gif) ![A A](_ca.gif) |
|
Theorem | sbcrel 4633 |
Distribute proper substitution through a relation predicate. (Contributed
by Alexander van der Vekens, 23-Jul-2017.)
|
![( (](lp.gif) ![( (](lp.gif) ![[. [.](_dlbrack.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![[_ [_](_ulbrack.gif) ![x x](_x.gif) ![]_ ]_](_urbrack.gif) ![R R](_cr.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | relss 4634 |
Subclass theorem for relation predicate. Theorem 2 of [Suppes] p. 58.
(Contributed by NM, 15-Aug-1994.)
|
![( (](lp.gif) ![( (](lp.gif) ![A
A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ssrel 4635* |
A subclass relationship depends only on a relation's ordered pairs.
Theorem 3.2(i) of [Monk1] p. 33.
(Contributed by NM, 2-Aug-1994.)
(Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
![( (](lp.gif) ![( (](lp.gif)
![A. A.](forall.gif) ![x x](_x.gif) ![A. A.](forall.gif) ![y y](_y.gif) ![(
(](lp.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | eqrel 4636* |
Extensionality principle for relations. Theorem 3.2(ii) of [Monk1]
p. 33. (Contributed by NM, 2-Aug-1994.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif)
![A. A.](forall.gif) ![x x](_x.gif) ![A. A.](forall.gif) ![y y](_y.gif) ![( (](lp.gif) ![<.
<.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ssrel2 4637* |
A subclass relationship depends only on a relation's ordered pairs.
This version of ssrel 4635 is restricted to the relation's domain.
(Contributed by Thierry Arnoux, 25-Jan-2018.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif)
![A. A.](forall.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![<.
<.](langle.gif) ![x x](_x.gif) ![y y](_y.gif)
![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![S S](_cs.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | relssi 4638* |
Inference from subclass principle for relations. (Contributed by NM,
31-Mar-1998.)
|
![( (](lp.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![<. <.](langle.gif) ![x x](_x.gif)
![y y](_y.gif) ![B B](_cb.gif)
![B B](_cb.gif) |
|
Theorem | relssdv 4639* |
Deduction from subclass principle for relations. (Contributed by NM,
11-Sep-2004.)
|
![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif)
![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | eqrelriv 4640* |
Inference from extensionality principle for relations. (Contributed by
FL, 15-Oct-2012.)
|
![( (](lp.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | eqrelriiv 4641* |
Inference from extensionality principle for relations. (Contributed by
NM, 17-Mar-1995.)
|
![( (](lp.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![B B](_cb.gif) ![B B](_cb.gif) |
|
Theorem | eqbrriv 4642* |
Inference from extensionality principle for relations. (Contributed by
NM, 12-Dec-2006.)
|
![( (](lp.gif) ![x x](_x.gif) ![A A](_ca.gif) ![x x](_x.gif) ![B B](_cb.gif) ![y y](_y.gif)
![B B](_cb.gif) |
|
Theorem | eqrelrdv 4643* |
Deduce equality of relations from equivalence of membership.
(Contributed by Rodolfo Medina, 10-Oct-2010.)
|
![( (](lp.gif) ![( (](lp.gif) ![<.
<.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | eqbrrdv 4644* |
Deduction from extensionality principle for relations. (Contributed by
Mario Carneiro, 3-Jan-2017.)
|
![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![A A](_ca.gif) ![x x](_x.gif) ![B B](_cb.gif) ![y y](_y.gif) ![) )](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | eqbrrdiv 4645* |
Deduction from extensionality principle for relations. (Contributed by
Rodolfo Medina, 10-Oct-2010.)
|
![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![A A](_ca.gif) ![x x](_x.gif) ![B B](_cb.gif) ![y y](_y.gif) ![) )](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | eqrelrdv2 4646* |
A version of eqrelrdv 4643. (Contributed by Rodolfo Medina,
10-Oct-2010.)
|
![( (](lp.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![ph ph](_varphi.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | ssrelrel 4647* |
A subclass relationship determined by ordered triples. Use relrelss 5073
to express the antecedent in terms of the relation predicate.
(Contributed by NM, 17-Dec-2008.) (Proof shortened by Andrew Salmon,
27-Aug-2011.)
|
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![_V _V](rmcv.gif) ![_V _V](rmcv.gif) ![( (](lp.gif)
![A. A.](forall.gif) ![x x](_x.gif) ![A. A.](forall.gif) ![y y](_y.gif) ![A. A.](forall.gif) ![z z](_z.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![z z](_z.gif)
![<. <.](langle.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![z z](_z.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | eqrelrel 4648* |
Extensionality principle for ordered triples, analogous to eqrel 4636.
Use relrelss 5073 to express the antecedent in terms of the
relation
predicate. (Contributed by NM, 17-Dec-2008.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![_V _V](rmcv.gif) ![( (](lp.gif)
![A. A.](forall.gif) ![x x](_x.gif) ![A. A.](forall.gif) ![y y](_y.gif) ![A. A.](forall.gif) ![z z](_z.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![z z](_z.gif) ![<. <.](langle.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![z z](_z.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | elrel 4649* |
A member of a relation is an ordered pair. (Contributed by NM,
17-Sep-2006.)
|
![( (](lp.gif) ![( (](lp.gif) ![R R](_cr.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![E. E.](exists.gif)
![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![) )](rp.gif) |
|
Theorem | relsng 4650 |
A singleton is a relation iff it is an ordered pair. (Contributed by NM,
24-Sep-2013.) (Revised by BJ, 12-Feb-2022.)
|
![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![A A](_ca.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | relsnopg 4651 |
A singleton of an ordered pair is a relation. (Contributed by NM,
17-May-1998.) (Revised by BJ, 12-Feb-2022.)
|
![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif)
![{ {](lbrace.gif) ![<. <.](langle.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
|
Theorem | relsn 4652 |
A singleton is a relation iff it is an ordered pair. (Contributed by
NM, 24-Sep-2013.)
|
![( (](lp.gif) ![{ {](lbrace.gif) ![A A](_ca.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | relsnop 4653 |
A singleton of an ordered pair is a relation. (Contributed by NM,
17-May-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
![{ {](lbrace.gif) ![<. <.](langle.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) |
|
Theorem | xpss12 4654 |
Subset theorem for cross product. Generalization of Theorem 101 of
[Suppes] p. 52. (Contributed by NM,
26-Aug-1995.) (Proof shortened by
Andrew Salmon, 27-Aug-2011.)
|
![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![C C](_cc.gif)
![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | xpss 4655 |
A cross product is included in the ordered pair universe. Exercise 3 of
[TakeutiZaring] p. 25. (Contributed
by NM, 2-Aug-1994.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) |
|
Theorem | relxp 4656 |
A cross product is a relation. Theorem 3.13(i) of [Monk1] p. 37.
(Contributed by NM, 2-Aug-1994.)
|
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | xpss1 4657 |
Subset relation for cross product. (Contributed by Jeff Hankins,
30-Aug-2009.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | xpss2 4658 |
Subset relation for cross product. (Contributed by Jeff Hankins,
30-Aug-2009.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | xpsspw 4659 |
A cross product is included in the power of the power of the union of
its arguments. (Contributed by NM, 13-Sep-2006.)
|
![( (](lp.gif) ![B B](_cb.gif) ![~P ~P](scrp.gif) ![~P ~P](scrp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | unixpss 4660 |
The double class union of a cross product is included in the union of its
arguments. (Contributed by NM, 16-Sep-2006.)
|
![U.
U.](bigcup.gif) ![U. U.](bigcup.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | xpexg 4661 |
The cross product of two sets is a set. Proposition 6.2 of
[TakeutiZaring] p. 23. (Contributed
by NM, 14-Aug-1994.)
|
![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![B B](_cb.gif)
![_V _V](rmcv.gif) ![) )](rp.gif) |
|
Theorem | xpex 4662 |
The cross product of two sets is a set. Proposition 6.2 of
[TakeutiZaring] p. 23.
(Contributed by NM, 14-Aug-1994.)
|
![( (](lp.gif) ![B B](_cb.gif)
![_V _V](rmcv.gif) |
|
Theorem | sqxpexg 4663 |
The Cartesian square of a set is a set. (Contributed by AV,
13-Jan-2020.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif)
![_V _V](rmcv.gif) ![) )](rp.gif) |
|
Theorem | relun 4664 |
The union of two relations is a relation. Compare Exercise 5 of
[TakeutiZaring] p. 25. (Contributed
by NM, 12-Aug-1994.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | relin1 4665 |
The intersection with a relation is a relation. (Contributed by NM,
16-Aug-1994.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | relin2 4666 |
The intersection with a relation is a relation. (Contributed by NM,
17-Jan-2006.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | reldif 4667 |
A difference cutting down a relation is a relation. (Contributed by NM,
31-Mar-1998.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | reliun 4668 |
An indexed union is a relation iff each member of its indexed family is
a relation. (Contributed by NM, 19-Dec-2008.)
|
![( (](lp.gif) ![U_ U_](_cupbar.gif) ![A. A.](forall.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | reliin 4669 |
An indexed intersection is a relation if at least one of the member of the
indexed family is a relation. (Contributed by NM, 8-Mar-2014.)
|
![( (](lp.gif) ![E. E.](exists.gif) ![|^|_ |^|_](_capbar.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | reluni 4670* |
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, 13-Aug-2004.)
|
![( (](lp.gif) ![U. U.](bigcup.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![) )](rp.gif) |
|
Theorem | relint 4671* |
The intersection of a class is a relation if at least one member is a
relation. (Contributed by NM, 8-Mar-2014.)
|
![( (](lp.gif) ![E. E.](exists.gif) ![|^| |^|](bigcap.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | rel0 4672 |
The empty set is a relation. (Contributed by NM, 26-Apr-1998.)
|
![(/) (/)](varnothing.gif) |
|
Theorem | relopabi 4673 |
A class of ordered pairs is a relation. (Contributed by Mario Carneiro,
21-Dec-2013.)
|
![{ {](lbrace.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![ph ph](_varphi.gif) ![A
A](_ca.gif) |
|
Theorem | relopab 4674 |
A class of ordered pairs is a relation. (Contributed by NM, 8-Mar-1995.)
(Unnecessary distinct variable restrictions were removed by Alan Sare,
9-Jul-2013.) (Proof shortened by Mario Carneiro, 21-Dec-2013.)
|
![{ {](lbrace.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![ph ph](_varphi.gif) ![} }](rbrace.gif) |
|
Theorem | mptrel 4675 |
The maps-to notation always describes a relationship. (Contributed by
Scott Fenton, 16-Apr-2012.)
|
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | reli 4676 |
The identity relation is a relation. Part of Exercise 4.12(p) of
[Mendelson] p. 235. (Contributed by
NM, 26-Apr-1998.) (Revised by
Mario Carneiro, 21-Dec-2013.)
|
![_I _I](rmci.gif) |
|
Theorem | rele 4677 |
The membership relation is a relation. (Contributed by NM,
26-Apr-1998.) (Revised by Mario Carneiro, 21-Dec-2013.)
|
![_E _E](rmce.gif) |
|
Theorem | opabid2 4678* |
A relation expressed as an ordered pair abstraction. (Contributed by
NM, 11-Dec-2006.)
|
![( (](lp.gif) ![{ {](lbrace.gif) ![<.
<.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![<.
<.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![A A](_ca.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | inopab 4679* |
Intersection of two ordered pair class abstractions. (Contributed by
NM, 30-Sep-2002.)
|
![( (](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![ph ph](_varphi.gif) ![{ {](lbrace.gif) ![<.
<.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![ps ps](_psi.gif) ![} }](rbrace.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![} }](rbrace.gif) |
|
Theorem | difopab 4680* |
The difference of two ordered-pair abstractions. (Contributed by Stefan
O'Rear, 17-Jan-2015.)
|
![( (](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![ph ph](_varphi.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![ps ps](_psi.gif) ![} }](rbrace.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![} }](rbrace.gif) |
|
Theorem | inxp 4681 |
The intersection of two cross products. Exercise 9 of [TakeutiZaring]
p. 25. (Contributed by NM, 3-Aug-1994.) (Proof shortened by Andrew
Salmon, 27-Aug-2011.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif)
![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | xpindi 4682 |
Distributive law for cross product over intersection. Theorem 102 of
[Suppes] p. 52. (Contributed by NM,
26-Sep-2004.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | xpindir 4683 |
Distributive law for cross product over intersection. Similar to
Theorem 102 of [Suppes] p. 52.
(Contributed by NM, 26-Sep-2004.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | xpiindim 4684* |
Distributive law for cross product over indexed intersection.
(Contributed by Jim Kingdon, 7-Dec-2018.)
|
![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![|^|_ |^|_](_capbar.gif) ![B B](_cb.gif)
![|^|_ |^|_](_capbar.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | xpriindim 4685* |
Distributive law for cross product over relativized indexed
intersection. (Contributed by Jim Kingdon, 7-Dec-2018.)
|
![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![( (](lp.gif) ![|^|_ |^|_](_capbar.gif) ![B B](_cb.gif) ![) )](rp.gif)
![( (](lp.gif) ![(
(](lp.gif) ![D D](_cd.gif) ![|^|_ |^|_](_capbar.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | eliunxp 4686* |
Membership in a union of cross products. Analogue of elxp 4564
for
nonconstant ![B B](_cb.gif) ![( (](lp.gif) ![x x](_x.gif) . (Contributed by Mario Carneiro,
29-Dec-2014.)
|
![( (](lp.gif) ![U_ U_](_cupbar.gif)
![( (](lp.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![B B](_cb.gif) ![E.
E.](exists.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![(
(](lp.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
|
Theorem | opeliunxp2 4687* |
Membership in a union of cross products. (Contributed by Mario
Carneiro, 14-Feb-2015.)
|
![( (](lp.gif) ![E E](_ce.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![C C](_cc.gif) ![D D](_cd.gif) ![U_ U_](_cupbar.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![B B](_cb.gif)
![( (](lp.gif) ![E E](_ce.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | raliunxp 4688* |
Write a double restricted quantification as one universal quantifier.
In this version of ralxp 4690, ![B
B](_cb.gif) ![( (](lp.gif) ![y y](_y.gif) is not assumed to be constant.
(Contributed by Mario Carneiro, 29-Dec-2014.)
|
![( (](lp.gif) ![<. <.](langle.gif) ![y y](_y.gif) ![z z](_z.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![y y](_y.gif) ![B B](_cb.gif) ![) )](rp.gif) ![A. A.](forall.gif) ![A. A.](forall.gif) ![ps ps](_psi.gif) ![) )](rp.gif) |
|
Theorem | rexiunxp 4689* |
Write a double restricted quantification as one universal quantifier.
In this version of rexxp 4691, ![B
B](_cb.gif) ![( (](lp.gif) ![y y](_y.gif) is not assumed to be constant.
(Contributed by Mario Carneiro, 14-Feb-2015.)
|
![( (](lp.gif) ![<. <.](langle.gif) ![y y](_y.gif) ![z z](_z.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![y y](_y.gif) ![B B](_cb.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![E. E.](exists.gif)
![ps ps](_psi.gif) ![) )](rp.gif) |
|
Theorem | ralxp 4690* |
Universal quantification restricted to a cross product is equivalent to
a double restricted quantification. The hypothesis specifies an
implicit substitution. (Contributed by NM, 7-Feb-2004.) (Revised by
Mario Carneiro, 29-Dec-2014.)
|
![( (](lp.gif) ![<. <.](langle.gif) ![y y](_y.gif) ![z z](_z.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![A. A.](forall.gif) ![A. A.](forall.gif) ![ps ps](_psi.gif) ![) )](rp.gif) |
|
Theorem | rexxp 4691* |
Existential quantification restricted to a cross product is equivalent
to a double restricted quantification. (Contributed by NM,
11-Nov-1995.) (Revised by Mario Carneiro, 14-Feb-2015.)
|
![( (](lp.gif) ![<. <.](langle.gif) ![y y](_y.gif) ![z z](_z.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![E. E.](exists.gif)
![ps ps](_psi.gif) ![) )](rp.gif) |
|
Theorem | djussxp 4692* |
Disjoint union is a subset of a cross product. (Contributed by Stefan
O'Rear, 21-Nov-2014.)
|
![U_ U_](_cupbar.gif)
![( (](lp.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![B B](_cb.gif)
![( (](lp.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) |
|
Theorem | ralxpf 4693* |
Version of ralxp 4690 with bound-variable hypotheses. (Contributed
by NM,
18-Aug-2006.) (Revised by Mario Carneiro, 15-Oct-2016.)
|
![F/
F/](finv.gif) ![y y](_y.gif) ![F/ F/](finv.gif) ![z z](_z.gif) ![F/ F/](finv.gif) ![x x](_x.gif) ![( (](lp.gif) ![<.
<.](langle.gif) ![y y](_y.gif) ![z z](_z.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![A. A.](forall.gif) ![A. A.](forall.gif) ![ps ps](_psi.gif) ![) )](rp.gif) |
|
Theorem | rexxpf 4694* |
Version of rexxp 4691 with bound-variable hypotheses. (Contributed
by NM,
19-Dec-2008.) (Revised by Mario Carneiro, 15-Oct-2016.)
|
![F/
F/](finv.gif) ![y y](_y.gif) ![F/ F/](finv.gif) ![z z](_z.gif) ![F/ F/](finv.gif) ![x x](_x.gif) ![( (](lp.gif) ![<.
<.](langle.gif) ![y y](_y.gif) ![z z](_z.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![E. E.](exists.gif)
![ps ps](_psi.gif) ![) )](rp.gif) |
|
Theorem | iunxpf 4695* |
Indexed union on a cross product is equals a double indexed union. The
hypothesis specifies an implicit substitution. (Contributed by NM,
19-Dec-2008.)
|
![F/_ F/_](_finvbar.gif) ![y y](_y.gif) ![F/_ F/_](_finvbar.gif) ![z z](_z.gif) ![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![y y](_y.gif) ![z z](_z.gif) ![D D](_cd.gif) ![U_ U_](_cupbar.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![U_ U_](_cupbar.gif) ![U_ U_](_cupbar.gif) ![D D](_cd.gif) |
|
Theorem | opabbi2dv 4696* |
Deduce equality of a relation and an ordered-pair class builder.
Compare abbi2dv 2259. (Contributed by NM, 24-Feb-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![<.
<.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![ps ps](_psi.gif) ![} }](rbrace.gif) ![)
)](rp.gif) |
|
Theorem | relop 4697* |
A necessary and sufficient condition for a Kuratowski ordered pair to be
a relation. (Contributed by NM, 3-Jun-2008.) (Avoid depending on this
detail.)
|
![( (](lp.gif) ![<. <.](langle.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![E.
E.](exists.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![(
(](lp.gif) ![{ {](lbrace.gif) ![x x](_x.gif)
![{ {](lbrace.gif) ![x x](_x.gif) ![y y](_y.gif) ![} }](rbrace.gif) ![)
)](rp.gif) ![) )](rp.gif) |
|
Theorem | ideqg 4698 |
For sets, the identity relation is the same as equality. (Contributed
by NM, 30-Apr-2004.) (Proof shortened by Andrew Salmon,
27-Aug-2011.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ideq 4699 |
For sets, the identity relation is the same as equality. (Contributed
by NM, 13-Aug-1995.)
|
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | ididg 4700 |
A set is identical to itself. (Contributed by NM, 28-May-2008.) (Proof
shortened by Andrew Salmon, 27-Aug-2011.)
|
![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) |