P. 42 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 4101-4200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	breq2i 4101	Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.)
|- A = B   =>    |- ( C R A <-> C R B )
Theorem	breq12i 4102	Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Eric Schmidt, 4-Apr-2007.)
|- A = B   &    |- C = D   =>    |- ( A R C <-> B R D )
Theorem	breq1d 4103	Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
|- ( ph -> A = B )   =>    |- ( ph -> ( A R C <-> B R C ) )
Theorem	breqd 4104	Equality deduction for a binary relation. (Contributed by NM, 29-Oct-2011.)
|- ( ph -> A = B )   =>    |- ( ph -> ( C A D <-> C B D ) )
Theorem	breq2d 4105	Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
|- ( ph -> A = B )   =>    |- ( ph -> ( C R A <-> C R B ) )
Theorem	breq12d 4106	Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> ( A R C <-> B R D ) )
Theorem	breq123d 4107	Equality deduction for a binary relation. (Contributed by NM, 29-Oct-2011.)
|- ( ph -> A = B )   &    |- ( ph -> R = S )   &    |- ( ph -> C = D )   =>    |- ( ph -> ( A R C <-> B S D ) )
Theorem	breqdi 4108	Equality deduction for a binary relation. (Contributed by Thierry Arnoux, 5-Oct-2020.)
|- ( ph -> A = B )   &    |- ( ph -> C A D )   =>    |- ( ph -> C B D )
Theorem	breqan12d 4109	Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
|- ( ph -> A = B )   &    |- ( ps -> C = D )   =>    |- ( ( ph /\ ps ) -> ( A R C <-> B R D ) )
Theorem	breqan12rd 4110	Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
|- ( ph -> A = B )   &    |- ( ps -> C = D )   =>    |- ( ( ps /\ ph ) -> ( A R C <-> B R D ) )
Theorem	eqnbrtrd 4111	Substitution of equal classes into the negation of a binary relation. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- ( ph -> A = B )   &    |- ( ph -> -. B R C )   =>    |- ( ph -> -. A R C )
Theorem	nbrne1 4112	Two classes are different if they don't have the same relationship to a third class. (Contributed by NM, 3-Jun-2012.)
|- ( ( A R B /\ -. A R C ) -> B =/= C )
Theorem	nbrne2 4113	Two classes are different if they don't have the same relationship to a third class. (Contributed by NM, 3-Jun-2012.)
|- ( ( A R C /\ -. B R C ) -> A =/= B )
Theorem	eqbrtri 4114	Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.)
|- A = B   &    |- B R C   =>    |- A R C
Theorem	eqbrtrd 4115	Substitution of equal classes into a binary relation. (Contributed by NM, 8-Oct-1999.)
|- ( ph -> A = B )   &    |- ( ph -> B R C )   =>    |- ( ph -> A R C )
Theorem	eqbrtrri 4116	Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.)
|- A = B   &    |- A R C   =>    |- B R C
Theorem	eqbrtrrd 4117	Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
|- ( ph -> A = B )   &    |- ( ph -> A R C )   =>    |- ( ph -> B R C )
Theorem	breqtri 4118	Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.)
|- A R B   &    |- B = C   =>    |- A R C
Theorem	breqtrd 4119	Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
|- ( ph -> A R B )   &    |- ( ph -> B = C )   =>    |- ( ph -> A R C )
Theorem	breqtrri 4120	Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.)
|- A R B   &    |- C = B   =>    |- A R C
Theorem	breqtrrd 4121	Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
|- ( ph -> A R B )   &    |- ( ph -> C = B )   =>    |- ( ph -> A R C )
Theorem	3brtr3i 4122	Substitution of equality into both sides of a binary relation. (Contributed by NM, 11-Aug-1999.)
|- A R B   &    |- A = C   &    |- B = D   =>    |- C R D
Theorem	3brtr4i 4123	Substitution of equality into both sides of a binary relation. (Contributed by NM, 11-Aug-1999.)
|- A R B   &    |- C = A   &    |- D = B   =>    |- C R D
Theorem	3brtr3d 4124	Substitution of equality into both sides of a binary relation. (Contributed by NM, 18-Oct-1999.)
|- ( ph -> A R B )   &    |- ( ph -> A = C )   &    |- ( ph -> B = D )   =>    |- ( ph -> C R D )
Theorem	3brtr4d 4125	Substitution of equality into both sides of a binary relation. (Contributed by NM, 21-Feb-2005.)
|- ( ph -> A R B )   &    |- ( ph -> C = A )   &    |- ( ph -> D = B )   =>    |- ( ph -> C R D )
Theorem	3brtr3g 4126	Substitution of equality into both sides of a binary relation. (Contributed by NM, 16-Jan-1997.)
|- ( ph -> A R B )   &    |- A = C   &    |- B = D   =>    |- ( ph -> C R D )
Theorem	3brtr4g 4127	Substitution of equality into both sides of a binary relation. (Contributed by NM, 16-Jan-1997.)
|- ( ph -> A R B )   &    |- C = A   &    |- D = B   =>    |- ( ph -> C R D )
Theorem	eqbrtrid 4128	B chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)
|- A = B   &    |- ( ph -> B R C )   =>    |- ( ph -> A R C )
Theorem	eqbrtrrid 4129	B chained equality inference for a binary relation. (Contributed by NM, 17-Sep-2004.)
|- B = A   &    |- ( ph -> B R C )   =>    |- ( ph -> A R C )
Theorem	breqtrid 4130	B chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)
|- A R B   &    |- ( ph -> B = C )   =>    |- ( ph -> A R C )
Theorem	breqtrrid 4131	B chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.)
|- A R B   &    |- ( ph -> C = B )   =>    |- ( ph -> A R C )
Theorem	eqbrtrdi 4132	A chained equality inference for a binary relation. (Contributed by NM, 12-Oct-1999.)
|- ( ph -> A = B )   &    |- B R C   =>    |- ( ph -> A R C )
Theorem	eqbrtrrdi 4133	A chained equality inference for a binary relation. (Contributed by NM, 4-Jan-2006.)
|- ( ph -> B = A )   &    |- B R C   =>    |- ( ph -> A R C )
Theorem	breqtrdi 4134	A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)
|- ( ph -> A R B )   &    |- B = C   =>    |- ( ph -> A R C )
Theorem	breqtrrdi 4135	A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.)
|- ( ph -> A R B )   &    |- C = B   =>    |- ( ph -> A R C )
Theorem	ssbrd 4136	Deduction from a subclass relationship of binary relations. (Contributed by NM, 30-Apr-2004.)
|- ( ph -> A C_ B )   =>    |- ( ph -> ( C A D -> C B D ) )
Theorem	ssbr 4137	Implication from a subclass relationship of binary relations. (Contributed by Peter Mazsa, 11-Nov-2019.)
|- ( A C_ B -> ( C A D -> C B D ) )
Theorem	ssbri 4138	Inference from a subclass relationship of binary relations. (Contributed by NM, 28-Mar-2007.) (Revised by Mario Carneiro, 8-Feb-2015.)
|- A C_ B   =>    |- ( C A D -> C B D )
Theorem	nfbrd 4139	Deduction version of bound-variable hypothesis builder nfbr 4140. (Contributed by NM, 13-Dec-2005.) (Revised by Mario Carneiro, 14-Oct-2016.)
|- ( ph -> F/_ x A )   &    |- ( ph -> F/_ x R )   &    |- ( ph -> F/_ x B )   =>    |- ( ph -> F/ x A R B )
Theorem	nfbr 4140	Bound-variable hypothesis builder for binary relation. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 14-Oct-2016.)
|- F/_ x A   &    |- F/_ x R   &    |- F/_ x B   =>    |- F/ x A R B
Theorem	brab1 4141*	Relationship between a binary relation and a class abstraction. (Contributed by Andrew Salmon, 8-Jul-2011.)
|- ( x R A <-> x e. { z | z R A } )
Theorem	br0 4142	The empty binary relation never holds. (Contributed by NM, 23-Aug-2018.)
|- -. A (/) B
Theorem	brne0 4143	If two sets are in a binary relation, the relation cannot be empty. In fact, the relation is also inhabited, as seen at brm 4144. (Contributed by Alexander van der Vekens, 7-Jul-2018.)
|- ( A R B -> R =/= (/) )
Theorem	brm 4144*	If two sets are in a binary relation, the relation is inhabited. (Contributed by Jim Kingdon, 31-Dec-2023.)
|- ( A R B -> E. x x e. R )
Theorem	brun 4145	The union of two binary relations. (Contributed by NM, 21-Dec-2008.)
|- ( A ( R u. S ) B <-> ( A R B \/ A S B ) )
Theorem	brin 4146	The intersection of two relations. (Contributed by FL, 7-Oct-2008.)
|- ( A ( R i^i S ) B <-> ( A R B /\ A S B ) )
Theorem	brdif 4147	The difference of two binary relations. (Contributed by Scott Fenton, 11-Apr-2011.)
|- ( A ( R \ S ) B <-> ( A R B /\ -. A S B ) )
Theorem	sbcbrg 4148	Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- ( A e. D -> ( [. A / x ]. B R C <-> [_ A / x ]_ B [_ A / x ]_ R [_ A / x ]_ C ) )
Theorem	sbcbr12g 4149*	Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.)
|- ( A e. D -> ( [. A / x ]. B R C <-> [_ A / x ]_ B R [_ A / x ]_ C ) )
Theorem	sbcbr1g 4150*	Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.)
|- ( A e. D -> ( [. A / x ]. B R C <-> [_ A / x ]_ B R C ) )
Theorem	sbcbr2g 4151*	Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.)
|- ( A e. D -> ( [. A / x ]. B R C <-> B R [_ A / x ]_ C ) )
Theorem	brralrspcev 4152*	Restricted existential specialization with a restricted universal quantifier over a relation, closed form. (Contributed by AV, 20-Aug-2022.)
|- ( ( B e. X /\ A. y e. Y A R B ) -> E. x e. X A. y e. Y A R x )
Theorem	brimralrspcev 4153*	Restricted existential specialization with a restricted universal quantifier over an implication with a relation in the antecedent, closed form. (Contributed by AV, 20-Aug-2022.)
|- ( ( B e. X /\ A. y e. Y ( ( ph /\ A R B ) -> ps ) ) -> E. x e. X A. y e. Y ( ( ph /\ A R x ) -> ps ) )
2.1.23  Ordered-pair class abstractions (class builders)
Syntax	copab 4154	Extend class notation to include ordered-pair class abstraction (class builder).
class { <. x , y >. | ph }
Syntax	cmpt 4155	Extend the definition of a class to include maps-to notation for defining a function via a rule.
class ( x e. A |-> B )
Definition	df-opab 4156*	Define the class abstraction of a collection of ordered pairs. Definition 3.3 of [Monk1] p. 34. Usually x and y are distinct, although the definition doesn't strictly require it. The brace notation is called "class abstraction" by Quine; it is also (more commonly) called a "class builder" in the literature. (Contributed by NM, 4-Jul-1994.)
|- { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
Definition	df-mpt 4157*	Define maps-to notation for defining a function via a rule. Read as "the function defined by the map from x (in A) to B ( x )". The class expression B is the value of the function at x and normally contains the variable x. Similar to the definition of mapping in [ChoquetDD] p. 2. (Contributed by NM, 17-Feb-2008.)
|- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
Theorem	opabss 4158*	The collection of ordered pairs in a class is a subclass of it. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- { <. x , y >. | x R y } C_ R
Theorem	opabbid 4159	Equivalent wff's yield equal ordered-pair class abstractions (deduction form). (Contributed by NM, 21-Feb-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- F/ x ph   &    |- F/ y ph   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> { <. x , y >. | ps } = { <. x , y >. | ch } )
Theorem	opabbidv 4160*	Equivalent wff's yield equal ordered-pair class abstractions (deduction form). (Contributed by NM, 15-May-1995.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> { <. x , y >. | ps } = { <. x , y >. | ch } )
Theorem	opabbii 4161	Equivalent wff's yield equal class abstractions. (Contributed by NM, 15-May-1995.)
|- ( ph <-> ps )   =>    |- { <. x , y >. | ph } = { <. x , y >. | ps }
Theorem	nfopab 4162*	Bound-variable hypothesis builder for class abstraction. (Contributed by NM, 1-Sep-1999.) Remove disjoint variable conditions. (Revised by Andrew Salmon, 11-Jul-2011.)
|- F/ z ph   =>    |- F/_ z { <. x , y >. | ph }
Theorem	nfopab1 4163	The first abstraction variable in an ordered-pair class abstraction (class builder) is effectively not free. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 14-Oct-2016.)
|- F/_ x { <. x , y >. | ph }
Theorem	nfopab2 4164	The second abstraction variable in an ordered-pair class abstraction (class builder) is effectively not free. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 14-Oct-2016.)
|- F/_ y { <. x , y >. | ph }
Theorem	cbvopab 4165*	Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 14-Sep-2003.)
|- F/ z ph   &    |- F/ w ph   &    |- F/ x ps   &    |- F/ y ps   &    |- ( ( x = z /\ y = w ) -> ( ph <-> ps ) )   =>    |- { <. x , y >. | ph } = { <. z , w >. | ps }
Theorem	cbvopabv 4166*	Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 15-Oct-1996.)
|- ( ( x = z /\ y = w ) -> ( ph <-> ps ) )   =>    |- { <. x , y >. | ph } = { <. z , w >. | ps }
Theorem	cbvopab1 4167*	Change first bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 6-Oct-2004.) (Revised by Mario Carneiro, 14-Oct-2016.)
|- F/ z ph   &    |- F/ x ps   &    |- ( x = z -> ( ph <-> ps ) )   =>    |- { <. x , y >. | ph } = { <. z , y >. | ps }
Theorem	cbvopab2 4168*	Change second bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 22-Aug-2013.)
|- F/ z ph   &    |- F/ y ps   &    |- ( y = z -> ( ph <-> ps ) )   =>    |- { <. x , y >. | ph } = { <. x , z >. | ps }
Theorem	cbvopab1s 4169*	Change first bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 31-Jul-2003.)
|- { <. x , y >. | ph } = { <. z , y >. | [ z / x ] ph }
Theorem	cbvopab1v 4170*	Rule used to change the first bound variable in an ordered pair abstraction, using implicit substitution. (Contributed by NM, 31-Jul-2003.) (Proof shortened by Eric Schmidt, 4-Apr-2007.)
|- ( x = z -> ( ph <-> ps ) )   =>    |- { <. x , y >. | ph } = { <. z , y >. | ps }
Theorem	cbvopab2v 4171*	Rule used to change the second bound variable in an ordered pair abstraction, using implicit substitution. (Contributed by NM, 2-Sep-1999.)
|- ( y = z -> ( ph <-> ps ) )   =>    |- { <. x , y >. | ph } = { <. x , z >. | ps }
Theorem	csbopabg 4172*	Move substitution into a class abstraction. (Contributed by NM, 6-Aug-2007.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
|- ( A e. V -> [_ A / x ]_ { <. y , z >. | ph } = { <. y , z >. | [. A / x ]. ph } )
Theorem	unopab 4173	Union of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002.)
|- ( { <. x , y >. | ph } u. { <. x , y >. | ps } ) = { <. x , y >. | ( ph \/ ps ) }
Theorem	mpteq12f 4174	An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
|- ( ( A. x A = C /\ A. x e. A B = D ) -> ( x e. A |-> B ) = ( x e. C |-> D ) )
Theorem	mpteq12dva 4175*	An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017.)
|- ( ph -> A = C )   &    |- ( ( ph /\ x e. A ) -> B = D )   =>    |- ( ph -> ( x e. A |-> B ) = ( x e. C |-> D ) )
Theorem	mpteq12dv 4176*	An equality inference for the maps-to notation. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 16-Dec-2013.)
|- ( ph -> A = C )   &    |- ( ph -> B = D )   =>    |- ( ph -> ( x e. A |-> B ) = ( x e. C |-> D ) )
Theorem	mpteq12 4177*	An equality theorem for the maps-to notation. (Contributed by NM, 16-Dec-2013.)
|- ( ( A = C /\ A. x e. A B = D ) -> ( x e. A |-> B ) = ( x e. C |-> D ) )
Theorem	mpteq1 4178*	An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
|- ( A = B -> ( x e. A |-> C ) = ( x e. B |-> C ) )
Theorem	mpteq1d 4179*	An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 11-Jun-2016.)
|- ( ph -> A = B )   =>    |- ( ph -> ( x e. A |-> C ) = ( x e. B |-> C ) )
Theorem	mpteq2ia 4180	An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
|- ( x e. A -> B = C )   =>    |- ( x e. A |-> B ) = ( x e. A |-> C )
Theorem	mpteq2i 4181	An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
|- B = C   =>    |- ( x e. A |-> B ) = ( x e. A |-> C )
Theorem	mpteq12i 4182	An equality inference for the maps-to notation. (Contributed by Scott Fenton, 27-Oct-2010.) (Revised by Mario Carneiro, 16-Dec-2013.)
|- A = C   &    |- B = D   =>    |- ( x e. A |-> B ) = ( x e. C |-> D )
Theorem	mpteq2da 4183	Slightly more general equality inference for the maps-to notation. (Contributed by FL, 14-Sep-2013.) (Revised by Mario Carneiro, 16-Dec-2013.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> B = C )   =>    |- ( ph -> ( x e. A |-> B ) = ( x e. A |-> C ) )
Theorem	mpteq2dva 4184*	Slightly more general equality inference for the maps-to notation. (Contributed by Scott Fenton, 25-Apr-2012.)
|- ( ( ph /\ x e. A ) -> B = C )   =>    |- ( ph -> ( x e. A |-> B ) = ( x e. A |-> C ) )
Theorem	mpteq2dv 4185*	An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 23-Aug-2014.)
|- ( ph -> B = C )   =>    |- ( ph -> ( x e. A |-> B ) = ( x e. A |-> C ) )
Theorem	nfmpt 4186*	Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/_ x ( y e. A |-> B )
Theorem	nfmpt1 4187	Bound-variable hypothesis builder for the maps-to notation. (Contributed by FL, 17-Feb-2008.)
|- F/_ x ( x e. A |-> B )
Theorem	cbvmptf 4188*	Rule to change the bound variable in a maps-to function, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. (Contributed by Thierry Arnoux, 9-Mar-2017.)
|- F/_ x A   &    |- F/_ y A   &    |- F/_ y B   &    |- F/_ x C   &    |- ( x = y -> B = C )   =>    |- ( x e. A |-> B ) = ( y e. A |-> C )
Theorem	cbvmpt 4189*	Rule to change the bound variable in a maps-to function, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. (Contributed by NM, 11-Sep-2011.)
|- F/_ y B   &    |- F/_ x C   &    |- ( x = y -> B = C )   =>    |- ( x e. A |-> B ) = ( y e. A |-> C )
Theorem	cbvmptv 4190*	Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by Mario Carneiro, 19-Feb-2013.)
|- ( x = y -> B = C )   =>    |- ( x e. A |-> B ) = ( y e. A |-> C )
Theorem	mptv 4191*	Function with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013.)
|- ( x e. _V |-> B ) = { <. x , y >. | y = B }
2.1.24  Transitive classes
Syntax	wtr 4192	Extend wff notation to include transitive classes. Notation from [TakeutiZaring] p. 35.
wff Tr A
Definition	df-tr 4193	Define the transitive class predicate. Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 4194 (which is suggestive of the word "transitive"), dftr3 4196, dftr4 4197, and dftr5 4195. The term "complete" is used instead of "transitive" in Definition 3 of [Suppes] p. 130. (Contributed by NM, 29-Aug-1993.)
|- ( Tr A <-> U. A C_ A )
Theorem	dftr2 4194*	An alternate way of defining a transitive class. Exercise 7 of [TakeutiZaring] p. 40. (Contributed by NM, 24-Apr-1994.)
|- ( Tr A <-> A. x A. y ( ( x e. y /\ y e. A ) -> x e. A ) )
Theorem	dftr5 4195*	An alternate way of defining a transitive class. (Contributed by NM, 20-Mar-2004.)
|- ( Tr A <-> A. x e. A A. y e. x y e. A )
Theorem	dftr3 4196*	An alternate way of defining a transitive class. Definition 7.1 of [TakeutiZaring] p. 35. (Contributed by NM, 29-Aug-1993.)
|- ( Tr A <-> A. x e. A x C_ A )
Theorem	dftr4 4197	An alternate way of defining a transitive class. Definition of [Enderton] p. 71. (Contributed by NM, 29-Aug-1993.)
|- ( Tr A <-> A C_ ~P A )
Theorem	treq 4198	Equality theorem for the transitive class predicate. (Contributed by NM, 17-Sep-1993.)
|- ( A = B -> ( Tr A <-> Tr B ) )
Theorem	trel 4199	In a transitive class, the membership relation is transitive. (Contributed by NM, 19-Apr-1994.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- ( Tr A -> ( ( B e. C /\ C e. A ) -> B e. A ) )
Theorem	trel3 4200	In a transitive class, the membership relation is transitive. (Contributed by NM, 19-Apr-1994.)
|- ( Tr A -> ( ( B e. C /\ C e. D /\ D e. A ) -> B e. A ) )