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	nnsucpred 4601	The successor of the precedessor of a nonzero natural number. (Contributed by Jim Kingdon, 31-Jul-2022.)
|- ( ( A e. om /\ A =/= (/) ) -> suc U. A = A )
Theorem	nndceq0 4602	A natural number is either zero or nonzero. Decidable equality for natural numbers is a special case of the law of the excluded middle which holds in most constructive set theories including ours. (Contributed by Jim Kingdon, 5-Jan-2019.)
|- ( A e. om -> DECID A = (/) )
Theorem	0elnn 4603	A natural number is either the empty set or has the empty set as an element. (Contributed by Jim Kingdon, 23-Aug-2019.)
|- ( A e. om -> ( A = (/) \/ (/) e. A ) )
Theorem	nn0eln0 4604	A natural number is nonempty iff it contains the empty set. Although in constructive mathematics it is generally more natural to work with inhabited sets and ignore the whole concept of nonempty sets, in the specific case of natural numbers this theorem may be helpful in converting proofs which were written assuming excluded middle. (Contributed by Jim Kingdon, 28-Aug-2019.)
|- ( A e. om -> ( (/) e. A <-> A =/= (/) ) )
Theorem	nnregexmid 4605*	If inhabited sets of natural numbers always have minimal elements, excluded middle follows. The argument is essentially the same as regexmid 4519 and the larger lesson is that although natural numbers may behave "non-constructively" even in a constructive set theory (for example see nndceq 6478 or nntri3or 6472), sets of natural numbers are a different animal. (Contributed by Jim Kingdon, 6-Sep-2019.)
|- ( ( x C_ om /\ E. y y e. x ) -> E. y ( y e. x /\ A. z ( z e. y -> -. z e. x ) ) )   =>    |- ( ph \/ -. ph )
Theorem	omsinds 4606*	Strong (or "total") induction principle over om. (Contributed by Scott Fenton, 17-Jul-2015.)
|- ( x = y -> ( ph <-> ps ) )   &    |- ( x = A -> ( ph <-> ch ) )   &    |- ( x e. om -> ( A. y e. x ps -> ph ) )   =>    |- ( A e. om -> ch )
Theorem	nnpredcl 4607	The predecessor of a natural number is a natural number. This theorem is most interesting when the natural number is a successor (as seen in theorems like onsucuni2 4548) but also holds when it is (/) by uni0 3823. (Contributed by Jim Kingdon, 31-Jul-2022.)
|- ( A e. om -> U. A e. om )
Theorem	nnpredlt 4608	The predecessor (see nnpredcl 4607) of a nonzero natural number is less than (see df-iord 4351) that number. (Contributed by Jim Kingdon, 14-Sep-2024.)
|- ( ( A e. om /\ A =/= (/) ) -> U. A e. A )
2.6.6  Relations
Syntax	cxp 4609	Extend the definition of a class to include the cross product.
class ( A X. B )
Syntax	ccnv 4610	Extend the definition of a class to include the converse of a class.
class `' A
Syntax	cdm 4611	Extend the definition of a class to include the domain of a class.
class dom A
Syntax	crn 4612	Extend the definition of a class to include the range of a class.
class ran A
Syntax	cres 4613	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 4614	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 4615	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 4616	Extend the definition of a wff to include the relation predicate. (Read: A is a relation.)
wff Rel A
Definition	df-xp 4617*	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 4618	Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5061 and dfrel3 5068. (Contributed by NM, 1-Aug-1994.)
|- ( Rel A <-> A C_ ( _V X. _V ) )
Definition	df-cnv 4619*	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 4794 (see df-br 3990 and df-rel 4618 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 4620*	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 4621*	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 4622). For alternate definitions see dfdm2 5145, dfdm3 4798, and dfdm4 4803. 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 4622	Define the range of a class. For example, F = { <. 2 , 6 >., <. 3 , 9 >. } -> ran F = { 6 , 9 } . Contrast with domain (defined in df-dm 4621). For alternate definitions, see dfrn2 4799, dfrn3 4800, and dfrn4 5071. 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 4623	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 4624	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 4623) and range (df-rn 4622). For an alternate definition, see dfima2 4955. (Contributed by NM, 2-Aug-1994.)
|- ( A " B ) = ran ( A |` B )
Theorem	xpeq1 4625	Equality theorem for cross product. (Contributed by NM, 4-Jul-1994.)
|- ( A = B -> ( A X. C ) = ( B X. C ) )
Theorem	xpeq2 4626	Equality theorem for cross product. (Contributed by NM, 5-Jul-1994.)
|- ( A = B -> ( C X. A ) = ( C X. B ) )
Theorem	elxpi 4627*	Membership in a cross product. Uses fewer axioms than elxp 4628. (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 4628*	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 4629*	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 4630	Equality theorem for cross product. (Contributed by FL, 31-Aug-2009.)
|- ( ( A = B /\ C = D ) -> ( A X. C ) = ( B X. D ) )
Theorem	xpeq1i 4631	Equality inference for cross product. (Contributed by NM, 21-Dec-2008.)
|- A = B   =>    |- ( A X. C ) = ( B X. C )
Theorem	xpeq2i 4632	Equality inference for cross product. (Contributed by NM, 21-Dec-2008.)
|- A = B   =>    |- ( C X. A ) = ( C X. B )
Theorem	xpeq12i 4633	Equality inference for cross product. (Contributed by FL, 31-Aug-2009.)
|- A = B   &    |- C = D   =>    |- ( A X. C ) = ( B X. D )
Theorem	xpeq1d 4634	Equality deduction for cross product. (Contributed by Jeff Madsen, 17-Jun-2010.)
|- ( ph -> A = B )   =>    |- ( ph -> ( A X. C ) = ( B X. C ) )
Theorem	xpeq2d 4635	Equality deduction for cross product. (Contributed by Jeff Madsen, 17-Jun-2010.)
|- ( ph -> A = B )   =>    |- ( ph -> ( C X. A ) = ( C X. B ) )
Theorem	xpeq12d 4636	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 4637	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 4638	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 4639	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 4640	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 4641	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 4642	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 4643	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 4644	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 4645	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 4646	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 4647	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 4648*	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 4649	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 4650	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 4651	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 4652	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 4653	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 4654	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 4655	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 4656	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 4657	A binary relation does not contain the empty set. (Contributed by AV, 15-Nov-2021.)
|- ( Rel R -> (/) e/ R )
Theorem	fconstmpt 4658*	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 4659*	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 4660	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 4661	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 4662	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 4663	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 4664*	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 4665*	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 4666	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 4667	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 4668	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 4669*	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 4670*	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 4671*	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 4672	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 4673*	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 4674*	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 4675	An ordered pair contains its union. (Contributed by NM, 16-Sep-2006.)
|- ( A e. ( _V X. _V ) -> U. A e. A )
Theorem	mosubopt 4676*	"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 4677*	"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 4678	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 4679	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 4680	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 4681	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 4682	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 4683	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 4684	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 4685*	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 4686*	The law of concretion for a binary relation. See brab2a 4664 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 4687*	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 4688*	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 4689*	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 4690*	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 4691	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 4692	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 4693	Equality theorem for the relation predicate. (Contributed by NM, 1-Aug-1994.)
|- ( A = B -> ( Rel A <-> Rel B ) )
Theorem	releqi 4694	Equality inference for the relation predicate. (Contributed by NM, 8-Dec-2006.)
|- A = B   =>    |- ( Rel A <-> Rel B )
Theorem	releqd 4695	Equality deduction for the relation predicate. (Contributed by NM, 8-Mar-2014.)
|- ( ph -> A = B )   =>    |- ( ph -> ( Rel A <-> Rel B ) )
Theorem	nfrel 4696	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 4697	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 4698	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 4699*	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 4700*	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 ) ) )