P. 47 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 4601-4700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nnpredlt 4601	The predecessor (see nnpredcl 4600) of a nonzero natural number is less than (see df-iord 4344) that number. (Contributed by Jim Kingdon, 14-Sep-2024.)
|- ( ( A e. om /\ A =/= (/) ) -> U. A e. A )
2.6.6  Relations
Syntax	cxp 4602	Extend the definition of a class to include the cross product.
class ( A X. B )
Syntax	ccnv 4603	Extend the definition of a class to include the converse of a class.
class `' A
Syntax	cdm 4604	Extend the definition of a class to include the domain of a class.
class dom A
Syntax	crn 4605	Extend the definition of a class to include the range of a class.
class ran A
Syntax	cres 4606	Extend the definition of a class to include the restriction of a class. (Read: The restriction of A to B.)
class ( A |` B )
Syntax	cima 4607	Extend the definition of a class to include the image of a class. (Read: The image of B under A.)
class ( A " B )
Syntax	ccom 4608	Extend the definition of a class to include the composition of two classes. (Read: The composition of A and B.)
class ( A o. B )
Syntax	wrel 4609	Extend the definition of a wff to include the relation predicate. (Read: A is a relation.)
wff Rel A
Definition	df-xp 4610*	Define the Cartesian product of two classes. This is also sometimes called the "cross product" but that term also has other meanings; we intentionally choose a less ambiguous term. Definition 9.11 of [Quine] p. 64. For example, ( { 1 , 5 } X. { 2 , 7 } ) = ( { <. 1 , 2 >. , <. 1 , 7 >. } u. { <. 5 , 2 >. , <. 5 , 7 >. } ). Another example is that the set of rational numbers is defined using the Cartesian product as ( ZZ X. NN ); the left- and right-hand sides of the Cartesian product represent the top (integer) and bottom (natural) numbers of a fraction. (Contributed by NM, 4-Jul-1994.)
|- ( A X. B ) = { <. x , y >. | ( x e. A /\ y e. B ) }
Definition	df-rel 4611	Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5054 and dfrel3 5061. (Contributed by NM, 1-Aug-1994.)
|- ( Rel A <-> A C_ ( _V X. _V ) )
Definition	df-cnv 4612*	Define the converse of a class. Definition 9.12 of [Quine] p. 64. The converse of a binary relation swaps its arguments, i.e., if A e. _V and B e. _V then ( A `' R B <-> B R A ), as proven in brcnv 4787 (see df-br 3983 and df-rel 4611 for more on relations). For example, `' { <. 2 , 6 >. , <. 3 , 9 >. } = { <. 6 , 2 >. , <. 9 , 3 >. }. We use Quine's breve accent (smile) notation. Like Quine, we use it as a prefix, which eliminates the need for parentheses. "Converse" is Quine's terminology. Some authors use a "minus one" exponent and call it "inverse", especially when the argument is a function, although this is not in general a genuine inverse. (Contributed by NM, 4-Jul-1994.)
|- `' A = { <. x , y >. | y A x }
Definition	df-co 4613*	Define the composition of two classes. Definition 6.6(3) of [TakeutiZaring] p. 24. Note that Definition 7 of [Suppes] p. 63 reverses A and B, uses a slash instead of o., and calls the operation "relative product". (Contributed by NM, 4-Jul-1994.)
|- ( A o. B ) = { <. x , y >. | E. z ( x B z /\ z A y ) }
Definition	df-dm 4614*	Define the domain of a class. Definition 3 of [Suppes] p. 59. For example, F = { <. 2 , 6 >., <. 3 , 9 >. } -> dom F = { 2 , 3 } . Contrast with range (defined in df-rn 4615). For alternate definitions see dfdm2 5138, dfdm3 4791, and dfdm4 4796. The notation " dom " is used by Enderton; other authors sometimes use script D. (Contributed by NM, 1-Aug-1994.)
|- dom A = { x | E. y x A y }
Definition	df-rn 4615	Define the range of a class. For example, F = { <. 2 , 6 >., <. 3 , 9 >. } -> ran F = { 6 , 9 } . Contrast with domain (defined in df-dm 4614). For alternate definitions, see dfrn2 4792, dfrn3 4793, and dfrn4 5064. The notation " ran " is used by Enderton; other authors sometimes use script R or script W. (Contributed by NM, 1-Aug-1994.)
|- ran A = dom `' A
Definition	df-res 4616	Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, ( F = { <. 2 , 6 >. , <. 3 , 9 >. } /\ B = { 1 , 2 } ) -> ( F |` B ) = { <. 2 , 6 >. }. We do not introduce a special syntax for the corestriction of a class: it will be expressed either as the intersection ( A i^i ( _V X. B ) ) or as the converse of the restricted converse. (Contributed by NM, 2-Aug-1994.)
|- ( A |` B ) = ( A i^i ( B X. _V ) )
Definition	df-ima 4617	Define the image of a class (as restricted by another class). Definition 6.6(2) of [TakeutiZaring] p. 24. For example, ( F = { <. 2 , 6 >., <. 3 , 9 >. } /\ B = { 1 , 2 } ) -> ( F " B ) = { 6 } . Contrast with restriction (df-res 4616) and range (df-rn 4615). For an alternate definition, see dfima2 4948. (Contributed by NM, 2-Aug-1994.)
|- ( A " B ) = ran ( A |` B )
Theorem	xpeq1 4618	Equality theorem for cross product. (Contributed by NM, 4-Jul-1994.)
|- ( A = B -> ( A X. C ) = ( B X. C ) )
Theorem	xpeq2 4619	Equality theorem for cross product. (Contributed by NM, 5-Jul-1994.)
|- ( A = B -> ( C X. A ) = ( C X. B ) )
Theorem	elxpi 4620*	Membership in a cross product. Uses fewer axioms than elxp 4621. (Contributed by NM, 4-Jul-1994.)
|- ( A e. ( B X. C ) -> E. x E. y ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) )
Theorem	elxp 4621*	Membership in a cross product. (Contributed by NM, 4-Jul-1994.)
|- ( A e. ( B X. C ) <-> E. x E. y ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) )
Theorem	elxp2 4622*	Membership in a cross product. (Contributed by NM, 23-Feb-2004.)
|- ( A e. ( B X. C ) <-> E. x e. B E. y e. C A = <. x , y >. )
Theorem	xpeq12 4623	Equality theorem for cross product. (Contributed by FL, 31-Aug-2009.)
|- ( ( A = B /\ C = D ) -> ( A X. C ) = ( B X. D ) )
Theorem	xpeq1i 4624	Equality inference for cross product. (Contributed by NM, 21-Dec-2008.)
|- A = B   =>    |- ( A X. C ) = ( B X. C )
Theorem	xpeq2i 4625	Equality inference for cross product. (Contributed by NM, 21-Dec-2008.)
|- A = B   =>    |- ( C X. A ) = ( C X. B )
Theorem	xpeq12i 4626	Equality inference for cross product. (Contributed by FL, 31-Aug-2009.)
|- A = B   &    |- C = D   =>    |- ( A X. C ) = ( B X. D )
Theorem	xpeq1d 4627	Equality deduction for cross product. (Contributed by Jeff Madsen, 17-Jun-2010.)
|- ( ph -> A = B )   =>    |- ( ph -> ( A X. C ) = ( B X. C ) )
Theorem	xpeq2d 4628	Equality deduction for cross product. (Contributed by Jeff Madsen, 17-Jun-2010.)
|- ( ph -> A = B )   =>    |- ( ph -> ( C X. A ) = ( C X. B ) )
Theorem	xpeq12d 4629	Equality deduction for Cartesian product. (Contributed by NM, 8-Dec-2013.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> ( A X. C ) = ( B X. D ) )
Theorem	sqxpeqd 4630	Equality deduction for a Cartesian square, see Wikipedia "Cartesian product", https://en.wikipedia.org/wiki/Cartesian_product#n-ary_Cartesian_power. (Contributed by AV, 13-Jan-2020.)
|- ( ph -> A = B )   =>    |- ( ph -> ( A X. A ) = ( B X. B ) )
Theorem	nfxp 4631	Bound-variable hypothesis builder for cross product. (Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/_ x ( A X. B )
Theorem	0nelxp 4632	The empty set is not a member of a cross product. (Contributed by NM, 2-May-1996.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- -. (/) e. ( A X. B )
Theorem	0nelelxp 4633	A member of a cross product (ordered pair) doesn't contain the empty set. (Contributed by NM, 15-Dec-2008.)
|- ( C e. ( A X. B ) -> -. (/) e. C )
Theorem	opelxp 4634	Ordered pair membership in a cross product. (Contributed by NM, 15-Nov-1994.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- ( <. A , B >. e. ( C X. D ) <-> ( A e. C /\ B e. D ) )
Theorem	brxp 4635	Binary relation on a cross product. (Contributed by NM, 22-Apr-2004.)
|- ( A ( C X. D ) B <-> ( A e. C /\ B e. D ) )
Theorem	opelxpi 4636	Ordered pair membership in a cross product (implication). (Contributed by NM, 28-May-1995.)
|- ( ( A e. C /\ B e. D ) -> <. A , B >. e. ( C X. D ) )
Theorem	opelxpd 4637	Ordered pair membership in a Cartesian product, deduction form. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> A e. C )   &    |- ( ph -> B e. D )   =>    |- ( ph -> <. A , B >. e. ( C X. D ) )
Theorem	opelxp1 4638	The first member of an ordered pair of classes in a cross product belongs to first cross product argument. (Contributed by NM, 28-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- ( <. A , B >. e. ( C X. D ) -> A e. C )
Theorem	opelxp2 4639	The second member of an ordered pair of classes in a cross product belongs to second cross product argument. (Contributed by Mario Carneiro, 26-Apr-2015.)
|- ( <. A , B >. e. ( C X. D ) -> B e. D )
Theorem	otelxp1 4640	The first member of an ordered triple of classes in a cross product belongs to first cross product argument. (Contributed by NM, 28-May-2008.)
|- ( <. <. A , B >. , C >. e. ( ( R X. S ) X. T ) -> A e. R )
Theorem	rabxp 4641*	Membership in a class builder restricted to a cross product. (Contributed by NM, 20-Feb-2014.)
|- ( x = <. y , z >. -> ( ph <-> ps ) )   =>    |- { x e. ( A X. B ) | ph } = { <. y , z >. | ( y e. A /\ z e. B /\ ps ) }
Theorem	brrelex12 4642	A true binary relation on a relation implies the arguments are sets. (This is a property of our ordered pair definition.) (Contributed by Mario Carneiro, 26-Apr-2015.)
|- ( ( Rel R /\ A R B ) -> ( A e. _V /\ B e. _V ) )
Theorem	brrelex1 4643	A true binary relation on a relation implies the first argument is a set. (This is a property of our ordered pair definition.) (Contributed by NM, 18-May-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- ( ( Rel R /\ A R B ) -> A e. _V )
Theorem	brrelex 4644	A true binary relation on a relation implies the first argument is a set. (This is a property of our ordered pair definition.) (Contributed by NM, 18-May-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- ( ( Rel R /\ A R B ) -> A e. _V )
Theorem	brrelex2 4645	A true binary relation on a relation implies the second argument is a set. (This is a property of our ordered pair definition.) (Contributed by Mario Carneiro, 26-Apr-2015.)
|- ( ( Rel R /\ A R B ) -> B e. _V )
Theorem	brrelex12i 4646	Two classes that are related by a binary relation are sets. (An artifact of our ordered pair definition.) (Contributed by BJ, 3-Oct-2022.)
|- Rel R   =>    |- ( A R B -> ( A e. _V /\ B e. _V ) )
Theorem	brrelex1i 4647	The first argument of a binary relation exists. (An artifact of our ordered pair definition.) (Contributed by NM, 4-Jun-1998.)
|- Rel R   =>    |- ( A R B -> A e. _V )
Theorem	brrelex2i 4648	The second argument of a binary relation exists. (An artifact of our ordered pair definition.) (Contributed by Mario Carneiro, 26-Apr-2015.)
|- Rel R   =>    |- ( A R B -> B e. _V )
Theorem	nprrel 4649	No proper class is related to anything via any relation. (Contributed by Roy F. Longton, 30-Jul-2005.)
|- Rel R   &    |- -. A e. _V   =>    |- -. A R B
Theorem	0nelrel 4650	A binary relation does not contain the empty set. (Contributed by AV, 15-Nov-2021.)
|- ( Rel R -> (/) e/ R )
Theorem	fconstmpt 4651*	Representation of a constant function using the mapping operation. (Note that x cannot appear free in B.) (Contributed by NM, 12-Oct-1999.) (Revised by Mario Carneiro, 16-Nov-2013.)
|- ( A X. { B } ) = ( x e. A |-> B )
Theorem	vtoclr 4652*	Variable to class conversion of transitive relation. (Contributed by NM, 9-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- Rel R   &    |- ( ( x R y /\ y R z ) -> x R z )   =>    |- ( ( A R B /\ B R C ) -> A R C )
Theorem	opelvvg 4653	Ordered pair membership in the universal class of ordered pairs. (Contributed by Mario Carneiro, 3-May-2015.)
|- ( ( A e. V /\ B e. W ) -> <. A , B >. e. ( _V X. _V ) )
Theorem	opelvv 4654	Ordered pair membership in the universal class of ordered pairs. (Contributed by NM, 22-Aug-2013.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- A e. _V   &    |- B e. _V   =>    |- <. A , B >. e. ( _V X. _V )
Theorem	opthprc 4655	Justification theorem for an ordered pair definition that works for any classes, including proper classes. This is a possible definition implied by the footnote in [Jech] p. 78, which says, "The sophisticated reader will not object to our use of a pair of classes." (Contributed by NM, 28-Sep-2003.)
|- ( ( ( A X. { (/) } ) u. ( B X. { { (/) } } ) ) = ( ( C X. { (/) } ) u. ( D X. { { (/) } } ) ) <-> ( A = C /\ B = D ) )
Theorem	brel 4656	Two things in a binary relation belong to the relation's domain. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- R C_ ( C X. D )   =>    |- ( A R B -> ( A e. C /\ B e. D ) )
Theorem	brab2a 4657*	Ordered pair membership in an ordered pair class abstraction. (Contributed by Mario Carneiro, 9-Nov-2015.)
|- ( ( x = A /\ y = B ) -> ( ph <-> ps ) )   &    |- R = { <. x , y >. | ( ( x e. C /\ y e. D ) /\ ph ) }   =>    |- ( A R B <-> ( ( A e. C /\ B e. D ) /\ ps ) )
Theorem	elxp3 4658*	Membership in a cross product. (Contributed by NM, 5-Mar-1995.)
|- ( A e. ( B X. C ) <-> E. x E. y ( <. x , y >. = A /\ <. x , y >. e. ( B X. C ) ) )
Theorem	opeliunxp 4659	Membership in a union of cross products. (Contributed by Mario Carneiro, 29-Dec-2014.) (Revised by Mario Carneiro, 1-Jan-2017.)
|- ( <. x , C >. e. U_ x e. A ( { x } X. B ) <-> ( x e. A /\ C e. B ) )
Theorem	xpundi 4660	Distributive law for cross product over union. Theorem 103 of [Suppes] p. 52. (Contributed by NM, 12-Aug-2004.)
|- ( A X. ( B u. C ) ) = ( ( A X. B ) u. ( A X. C ) )
Theorem	xpundir 4661	Distributive law for cross product over union. Similar to Theorem 103 of [Suppes] p. 52. (Contributed by NM, 30-Sep-2002.)
|- ( ( A u. B ) X. C ) = ( ( A X. C ) u. ( B X. C ) )
Theorem	xpiundi 4662*	Distributive law for cross product over indexed union. (Contributed by Mario Carneiro, 27-Apr-2014.)
|- ( C X. U_ x e. A B ) = U_ x e. A ( C X. B )
Theorem	xpiundir 4663*	Distributive law for cross product over indexed union. (Contributed by Mario Carneiro, 27-Apr-2014.)
|- ( U_ x e. A B X. C ) = U_ x e. A ( B X. C )
Theorem	iunxpconst 4664*	Membership in a union of cross products when the second factor is constant. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- U_ x e. A ( { x } X. B ) = ( A X. B )
Theorem	xpun 4665	The cross product of two unions. (Contributed by NM, 12-Aug-2004.)
|- ( ( A u. B ) X. ( C u. D ) ) = ( ( ( A X. C ) u. ( A X. D ) ) u. ( ( B X. C ) u. ( B X. D ) ) )
Theorem	elvv 4666*	Membership in universal class of ordered pairs. (Contributed by NM, 4-Jul-1994.)
|- ( A e. ( _V X. _V ) <-> E. x E. y A = <. x , y >. )
Theorem	elvvv 4667*	Membership in universal class of ordered triples. (Contributed by NM, 17-Dec-2008.)
|- ( A e. ( ( _V X. _V ) X. _V ) <-> E. x E. y E. z A = <. <. x , y >. , z >. )
Theorem	elvvuni 4668	An ordered pair contains its union. (Contributed by NM, 16-Sep-2006.)
|- ( A e. ( _V X. _V ) -> U. A e. A )
Theorem	mosubopt 4669*	"At most one" remains true inside ordered pair quantification. (Contributed by NM, 28-Aug-2007.)
|- ( A. y A. z E* x ph -> E* x E. y E. z ( A = <. y , z >. /\ ph ) )
Theorem	mosubop 4670*	"At most one" remains true inside ordered pair quantification. (Contributed by NM, 28-May-1995.)
|- E* x ph   =>    |- E* x E. y E. z ( A = <. y , z >. /\ ph )
Theorem	brinxp2 4671	Intersection of binary relation with Cartesian product. (Contributed by NM, 3-Mar-2007.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- ( A ( R i^i ( C X. D ) ) B <-> ( A e. C /\ B e. D /\ A R B ) )
Theorem	brinxp 4672	Intersection of binary relation with Cartesian product. (Contributed by NM, 9-Mar-1997.)
|- ( ( A e. C /\ B e. D ) -> ( A R B <-> A ( R i^i ( C X. D ) ) B ) )
Theorem	poinxp 4673	Intersection of partial order with cross product of its field. (Contributed by Mario Carneiro, 10-Jul-2014.)
|- ( R Po A <-> ( R i^i ( A X. A ) ) Po A )
Theorem	soinxp 4674	Intersection of linear order with cross product of its field. (Contributed by Mario Carneiro, 10-Jul-2014.)
|- ( R Or A <-> ( R i^i ( A X. A ) ) Or A )
Theorem	seinxp 4675	Intersection of set-like relation with cross product of its field. (Contributed by Mario Carneiro, 22-Jun-2015.)
|- ( R Se A <-> ( R i^i ( A X. A ) ) Se A )
Theorem	posng 4676	Partial ordering of a singleton. (Contributed by Jim Kingdon, 5-Dec-2018.)
|- ( ( Rel R /\ A e. _V ) -> ( R Po { A } <-> -. A R A ) )
Theorem	sosng 4677	Strict linear ordering on a singleton. (Contributed by Jim Kingdon, 5-Dec-2018.)
|- ( ( Rel R /\ A e. _V ) -> ( R Or { A } <-> -. A R A ) )
Theorem	opabssxp 4678*	An abstraction relation is a subset of a related cross product. (Contributed by NM, 16-Jul-1995.)
|- { <. x , y >. | ( ( x e. A /\ y e. B ) /\ ph ) } C_ ( A X. B )
Theorem	brab2ga 4679*	The law of concretion for a binary relation. See brab2a 4657 for alternate proof. TODO: should one of them be deleted? (Contributed by Mario Carneiro, 28-Apr-2015.) (Proof modification is discouraged.)
|- ( ( x = A /\ y = B ) -> ( ph <-> ps ) )   &    |- R = { <. x , y >. | ( ( x e. C /\ y e. D ) /\ ph ) }   =>    |- ( A R B <-> ( ( A e. C /\ B e. D ) /\ ps ) )
Theorem	optocl 4680*	Implicit substitution of class for ordered pair. (Contributed by NM, 5-Mar-1995.)
|- D = ( B X. C )   &    |- ( <. x , y >. = A -> ( ph <-> ps ) )   &    |- ( ( x e. B /\ y e. C ) -> ph )   =>    |- ( A e. D -> ps )
Theorem	2optocl 4681*	Implicit substitution of classes for ordered pairs. (Contributed by NM, 12-Mar-1995.)
|- R = ( C X. D )   &    |- ( <. x , y >. = A -> ( ph <-> ps ) )   &    |- ( <. z , w >. = B -> ( ps <-> ch ) )   &    |- ( ( ( x e. C /\ y e. D ) /\ ( z e. C /\ w e. D ) ) -> ph )   =>    |- ( ( A e. R /\ B e. R ) -> ch )
Theorem	3optocl 4682*	Implicit substitution of classes for ordered pairs. (Contributed by NM, 12-Mar-1995.)
|- R = ( D X. F )   &    |- ( <. x , y >. = A -> ( ph <-> ps ) )   &    |- ( <. z , w >. = B -> ( ps <-> ch ) )   &    |- ( <. v , u >. = C -> ( ch <-> th ) )   &    |- ( ( ( x e. D /\ y e. F ) /\ ( z e. D /\ w e. F ) /\ ( v e. D /\ u e. F ) ) -> ph )   =>    |- ( ( A e. R /\ B e. R /\ C e. R ) -> th )
Theorem	opbrop 4683*	Ordered pair membership in a relation. Special case. (Contributed by NM, 5-Aug-1995.)
|- ( ( ( z = A /\ w = B ) /\ ( v = C /\ u = D ) ) -> ( ph <-> ps ) )   &    |- R = { <. x , y >. | ( ( x e. ( S X. S ) /\ y e. ( S X. S ) ) /\ E. z E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ph ) ) }   =>    |- ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> ( <. A , B >. R <. C , D >. <-> ps ) )
Theorem	0xp 4684	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.)
|- ( (/) X. A ) = (/)
Theorem	csbxpg 4685	Distribute proper substitution through the cross product of two classes. (Contributed by Alan Sare, 10-Nov-2012.)
|- ( A e. D -> [_ A / x ]_ ( B X. C ) = ( [_ A / x ]_ B X. [_ A / x ]_ C ) )
Theorem	releq 4686	Equality theorem for the relation predicate. (Contributed by NM, 1-Aug-1994.)
|- ( A = B -> ( Rel A <-> Rel B ) )
Theorem	releqi 4687	Equality inference for the relation predicate. (Contributed by NM, 8-Dec-2006.)
|- A = B   =>    |- ( Rel A <-> Rel B )
Theorem	releqd 4688	Equality deduction for the relation predicate. (Contributed by NM, 8-Mar-2014.)
|- ( ph -> A = B )   =>    |- ( ph -> ( Rel A <-> Rel B ) )
Theorem	nfrel 4689	Bound-variable hypothesis builder for a relation. (Contributed by NM, 31-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/_ x A   =>    |- F/ x Rel A
Theorem	sbcrel 4690	Distribute proper substitution through a relation predicate. (Contributed by Alexander van der Vekens, 23-Jul-2017.)
|- ( A e. V -> ( [. A / x ]. Rel R <-> Rel [_ A / x ]_ R ) )
Theorem	relss 4691	Subclass theorem for relation predicate. Theorem 2 of [Suppes] p. 58. (Contributed by NM, 15-Aug-1994.)
|- ( A C_ B -> ( Rel B -> Rel A ) )
Theorem	ssrel 4692*	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.)
|- ( Rel A -> ( A C_ B <-> A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) ) )
Theorem	eqrel 4693*	Extensionality principle for relations. Theorem 3.2(ii) of [Monk1] p. 33. (Contributed by NM, 2-Aug-1994.)
|- ( ( Rel A /\ Rel B ) -> ( A = B <-> A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. B ) ) )
Theorem	ssrel2 4694*	A subclass relationship depends only on a relation's ordered pairs. This version of ssrel 4692 is restricted to the relation's domain. (Contributed by Thierry Arnoux, 25-Jan-2018.)
|- ( R C_ ( A X. B ) -> ( R C_ S <-> A. x e. A A. y e. B ( <. x , y >. e. R -> <. x , y >. e. S ) ) )
Theorem	relssi 4695*	Inference from subclass principle for relations. (Contributed by NM, 31-Mar-1998.)
|- Rel A   &    |- ( <. x , y >. e. A -> <. x , y >. e. B )   =>    |- A C_ B
Theorem	relssdv 4696*	Deduction from subclass principle for relations. (Contributed by NM, 11-Sep-2004.)
|- ( ph -> Rel A )   &    |- ( ph -> ( <. x , y >. e. A -> <. x , y >. e. B ) )   =>    |- ( ph -> A C_ B )
Theorem	eqrelriv 4697*	Inference from extensionality principle for relations. (Contributed by FL, 15-Oct-2012.)
|- ( <. x , y >. e. A <-> <. x , y >. e. B )   =>    |- ( ( Rel A /\ Rel B ) -> A = B )
Theorem	eqrelriiv 4698*	Inference from extensionality principle for relations. (Contributed by NM, 17-Mar-1995.)
|- Rel A   &    |- Rel B   &    |- ( <. x , y >. e. A <-> <. x , y >. e. B )   =>    |- A = B
Theorem	eqbrriv 4699*	Inference from extensionality principle for relations. (Contributed by NM, 12-Dec-2006.)
|- Rel A   &    |- Rel B   &    |- ( x A y <-> x B y )   =>    |- A = B
Theorem	eqrelrdv 4700*	Deduce equality of relations from equivalence of membership. (Contributed by Rodolfo Medina, 10-Oct-2010.)
|- Rel A   &    |- Rel B   &    |- ( ph -> ( <. x , y >. e. A <-> <. x , y >. e. B ) )   =>    |- ( ph -> A = B )