P. 48 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 4701-4800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nnon 4701	A natural number is an ordinal number. (Contributed by NM, 27-Jun-1994.)
|- ( A e. om -> A e. On )
Theorem	nnoni 4702	A natural number is an ordinal number. (Contributed by NM, 27-Jun-1994.)
|- A e. om   =>    |- A e. On
Theorem	nnord 4703	A natural number is ordinal. (Contributed by NM, 17-Oct-1995.)
|- ( A e. om -> Ord A )
Theorem	omsson 4704	Omega is a subset of On. (Contributed by NM, 13-Jun-1994.)
|- om C_ On
Theorem	limom 4705	Omega is a limit ordinal. Theorem 2.8 of [BellMachover] p. 473. (Contributed by NM, 26-Mar-1995.) (Proof rewritten by Jim Kingdon, 5-Jan-2019.)
|- Lim om
Theorem	peano2b 4706	A class belongs to omega iff its successor does. (Contributed by NM, 3-Dec-1995.)
|- ( A e. om <-> suc A e. om )
Theorem	nnsuc 4707*	A nonzero natural number is a successor. (Contributed by NM, 18-Feb-2004.)
|- ( ( A e. om /\ A =/= (/) ) -> E. x e. om A = suc x )
Theorem	nnsucpred 4708	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 4709	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 4710	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 4711	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 4712*	If inhabited sets of natural numbers always have minimal elements, excluded middle follows. The argument is essentially the same as regexmid 4626 and the larger lesson is that although natural numbers may behave "non-constructively" even in a constructive set theory (for example see nndceq 6643 or nntri3or 6637), 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 4713*	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 4714	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 4655) but also holds when it is (/) by uni0 3914. (Contributed by Jim Kingdon, 31-Jul-2022.)
|- ( A e. om -> U. A e. om )
Theorem	nnpredlt 4715	The predecessor (see nnpredcl 4714) of a nonzero natural number is less than (see df-iord 4456) that number. (Contributed by Jim Kingdon, 14-Sep-2024.)
|- ( ( A e. om /\ A =/= (/) ) -> U. A e. A )
2.6.6  Relations
Syntax	cxp 4716	Extend the definition of a class to include the cross product.
class ( A X. B )
Syntax	ccnv 4717	Extend the definition of a class to include the converse of a class.
class `' A
Syntax	cdm 4718	Extend the definition of a class to include the domain of a class.
class dom A
Syntax	crn 4719	Extend the definition of a class to include the range of a class.
class ran A
Syntax	cres 4720	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 4721	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 4722	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 4723	Extend the definition of a wff to include the relation predicate. (Read: A is a relation.)
wff Rel A
Definition	df-xp 4724*	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 4725	Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5178 and dfrel3 5185. (Contributed by NM, 1-Aug-1994.)
|- ( Rel A <-> A C_ ( _V X. _V ) )
Definition	df-cnv 4726*	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 4904 (see df-br 4083 and df-rel 4725 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 4727*	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 4728*	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 4729). For alternate definitions see dfdm2 5262, dfdm3 4908, and dfdm4 4914. 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 4729	Define the range of a class. For example, F = { <. 2 , 6 >., <. 3 , 9 >. } -> ran F = { 6 , 9 } . Contrast with domain (defined in df-dm 4728). For alternate definitions, see dfrn2 4909, dfrn3 4910, and dfrn4 5188. 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 4730	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 4731	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 4730) and range (df-rn 4729). For an alternate definition, see dfima2 5069. (Contributed by NM, 2-Aug-1994.)
|- ( A " B ) = ran ( A |` B )
Theorem	xpeq1 4732	Equality theorem for cross product. (Contributed by NM, 4-Jul-1994.)
|- ( A = B -> ( A X. C ) = ( B X. C ) )
Theorem	xpeq2 4733	Equality theorem for cross product. (Contributed by NM, 5-Jul-1994.)
|- ( A = B -> ( C X. A ) = ( C X. B ) )
Theorem	elxpi 4734*	Membership in a cross product. Uses fewer axioms than elxp 4735. (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 4735*	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 4736*	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 4737	Equality theorem for cross product. (Contributed by FL, 31-Aug-2009.)
|- ( ( A = B /\ C = D ) -> ( A X. C ) = ( B X. D ) )
Theorem	xpeq1i 4738	Equality inference for cross product. (Contributed by NM, 21-Dec-2008.)
|- A = B   =>    |- ( A X. C ) = ( B X. C )
Theorem	xpeq2i 4739	Equality inference for cross product. (Contributed by NM, 21-Dec-2008.)
|- A = B   =>    |- ( C X. A ) = ( C X. B )
Theorem	xpeq12i 4740	Equality inference for cross product. (Contributed by FL, 31-Aug-2009.)
|- A = B   &    |- C = D   =>    |- ( A X. C ) = ( B X. D )
Theorem	xpeq1d 4741	Equality deduction for cross product. (Contributed by Jeff Madsen, 17-Jun-2010.)
|- ( ph -> A = B )   =>    |- ( ph -> ( A X. C ) = ( B X. C ) )
Theorem	xpeq2d 4742	Equality deduction for cross product. (Contributed by Jeff Madsen, 17-Jun-2010.)
|- ( ph -> A = B )   =>    |- ( ph -> ( C X. A ) = ( C X. B ) )
Theorem	xpeq12d 4743	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 4744	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 4745	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 4746	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 4747	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 4748	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 4749	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 4750	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 4751	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 4752	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 4753	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 4754	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 4755*	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 4756	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 4757	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 4758	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 4759	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 4760	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 4761	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 4762	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 4763	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 4764	A binary relation does not contain the empty set. (Contributed by AV, 15-Nov-2021.)
|- ( Rel R -> (/) e/ R )
Theorem	fconstmpt 4765*	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 4766*	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 4767	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 4768	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 4769	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 4770	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 4771*	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 4772*	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 4773	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 4774	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 4775	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 4776*	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 4777*	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 4778*	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 4779	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 4780*	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 4781*	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 4782	An ordered pair contains its union. (Contributed by NM, 16-Sep-2006.)
|- ( A e. ( _V X. _V ) -> U. A e. A )
Theorem	mosubopt 4783*	"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 4784*	"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 4785	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 4786	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 4787	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 4788	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 4789	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 4790	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 4791	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 4792*	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 4793*	The law of concretion for a binary relation. See brab2a 4771 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 4794*	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 4795*	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 4796*	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 4797*	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 4798	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 4799	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 4800	Equality theorem for the relation predicate. (Contributed by NM, 1-Aug-1994.)
|- ( A = B -> ( Rel A <-> Rel B ) )