P. 292 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 29101-29200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	brpprod3a 29101*	Condition for parallel product when the last argument is not an ordered pair. (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- X e. _V   &    |- Y e. _V   &    |- Z e. _V   =>    |- ( <. X , Y >.pprod ( R , S ) Z <-> E. z E. w ( Z = <. z , w >. /\ X R z /\ Y S w ) )
Theorem	brpprod3b 29102*	Condition for parallel product when the first argument is not an ordered pair. (Contributed by Scott Fenton, 3-May-2014.)
|- X e. _V   &    |- Y e. _V   &    |- Z e. _V   =>    |- ( Xpprod ( R , S ) <. Y , Z >. <-> E. z E. w ( X = <. z , w >. /\ z R Y /\ w S Z ) )
Theorem	relsset 29103	The subset class is a relationship. (Contributed by Scott Fenton, 31-Mar-2012.)
|- Rel SSet
Theorem	brsset 29104	For sets, the SSet binary relationship is equivalent to the subset relationship. (Contributed by Scott Fenton, 31-Mar-2012.)
|- B e. _V   =>    |- ( A SSet B <-> A C_ B )
Theorem	idsset 29105	_I is equal to SSet and its converse. (Contributed by Scott Fenton, 31-Mar-2012.)
|- _I = ( SSet i^i `' SSet )
Theorem	eltrans 29106	Membership in the class of all transitive sets. (Contributed by Scott Fenton, 31-Mar-2012.)
|- A e. _V   =>    |- ( A e. Trans <-> Tr A )
Theorem	dfon3 29107	A quantifier-free definition of On. (Contributed by Scott Fenton, 5-Apr-2012.)
|- On = ( _V \ ran ( ( SSet i^i ( Trans X. _V ) ) \ ( _I u. _E ) ) )
Theorem	dfon4 29108	Another quantifier-free definition of On. (Contributed by Scott Fenton, 4-May-2014.)
|- On = ( _V \ ( ( SSet \ ( _I u. _E ) ) " Trans ) )
Theorem	brtxpsd 29109*	Expansion of a common form used in quantifier-free definitions. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- A e. _V   &    |- B e. _V   =>    |- ( -. A ran ( ( _V (x) _E )(++) ( R (x) _V ) ) B <-> A. x ( x e. B <-> x R A ) )
Theorem	brtxpsd2 29110*	Another common abbreviation for quantifier-free definitions. (Contributed by Scott Fenton, 21-Apr-2014.)
|- A e. _V   &    |- B e. _V   &    |- R = ( C \ ran ( ( _V (x) _E )(++) ( S (x) _V ) ) )   &    |- A C B   =>    |- ( A R B <-> A. x ( x e. B <-> x S A ) )
Theorem	brtxpsd3 29111*	A third common abbreviation for quantifier-free definitions. (Contributed by Scott Fenton, 3-May-2014.)
|- A e. _V   &    |- B e. _V   &    |- R = ( C \ ran ( ( _V (x) _E )(++) ( S (x) _V ) ) )   &    |- A C B   &    |- ( x e. X <-> x S A )   =>    |- ( A R B <-> B = X )
Theorem	relbigcup 29112	The Bigcup relationship is a relationship. (Contributed by Scott Fenton, 11-Apr-2012.)
|- Rel Bigcup
Theorem	brbigcup 29113	Binary relationship over Bigcup. (Contributed by Scott Fenton, 11-Apr-2012.)
|- B e. _V   =>    |- ( A Bigcup B <-> U. A = B )
Theorem	dfbigcup2 29114	Bigcup using maps-to notation. (Contributed by Scott Fenton, 16-Apr-2012.)
|- Bigcup = ( x e. _V |-> U. x )
Theorem	fobigcup 29115	Bigcup maps the universe onto itself. (Contributed by Scott Fenton, 16-Apr-2012.)
|- Bigcup : _V -onto-> _V
Theorem	fnbigcup 29116	Bigcup is a function over the universal class. (Contributed by Scott Fenton, 11-Apr-2012.)
|- Bigcup Fn _V
Theorem	fvbigcup 29117	For sets, Bigcup yields union. (Contributed by Scott Fenton, 11-Apr-2012.)
|- A e. _V   =>    |- ( Bigcup ` A ) = U. A
Theorem	elfix 29118	Membership in the fixpoints of a class. (Contributed by Scott Fenton, 11-Apr-2012.)
|- A e. _V   =>    |- ( A e. Fix R <-> A R A )
Theorem	elfix2 29119	Alternative membership in the fixpoint of a class. (Contributed by Scott Fenton, 11-Apr-2012.)
|- Rel R   =>    |- ( A e. Fix R <-> A R A )
Theorem	dffix2 29120	The fixpoints of a class in terms of its range. (Contributed by Scott Fenton, 16-Apr-2012.)
|- Fix A = ran ( A i^i _I )
Theorem	fixssdm 29121	The fixpoints of a class are a subset of its domain. (Contributed by Scott Fenton, 16-Apr-2012.)
|- Fix A C_ dom A
Theorem	fixssrn 29122	The fixpoints of a class are a subset of its range. (Contributed by Scott Fenton, 16-Apr-2012.)
|- Fix A C_ ran A
Theorem	fixcnv 29123	The fixpoints of a class are the same as those of its converse. (Contributed by Scott Fenton, 16-Apr-2012.)
|- Fix A = Fix `' A
Theorem	fixun 29124	The fixpoint operator distributes over union. (Contributed by Scott Fenton, 16-Apr-2012.)
|- Fix ( A u. B ) = ( Fix A u. Fix B )
Theorem	ellimits 29125	Membership in the class of all limit ordinals. (Contributed by Scott Fenton, 11-Apr-2012.)
|- A e. _V   =>    |- ( A e. Limits <-> Lim A )
Theorem	limitssson 29126	The class of all limit ordinals is a subclass of the class of all ordinals. (Contributed by Scott Fenton, 11-Apr-2012.)
|- Limits C_ On
Theorem	dfom5b 29127	A quantifier-free definition of om that does not depend on ax-inf 8046. (Note: label was changed from dfom5 8058 to dfom5b 29127 to prevent naming conflict. NM 12-Feb-2013) (Contributed by Scott Fenton, 11-Apr-2012.)
|- om = ( On i^i |^| Limits )
Theorem	sscoid 29128	A condition for subset and composition with identity. (Contributed by Scott Fenton, 13-Apr-2018.)
|- ( A C_ ( _I o. B ) <-> ( Rel A /\ A C_ B ) )
Theorem	dffun10 29129	Another potential definition of functionhood. Based on statements in http://people.math.gatech.edu/~belinfan/research/autoreas/otter/sum/fs/. (Contributed by Scott Fenton, 30-Aug-2017.)
|- ( Fun F <-> F C_ ( _I o. ( _V \ ( ( _V \ _I ) o. F ) ) ) )
Theorem	elfuns 29130	Membership in the class of all functions. (Contributed by Scott Fenton, 18-Feb-2013.)
|- F e. _V   =>    |- ( F e. Funs <-> Fun F )
Theorem	elfunsg 29131	Closed form of elfuns 29130. (Contributed by Scott Fenton, 2-May-2014.)
|- ( F e. V -> ( F e. Funs <-> Fun F ) )
Theorem	brsingle 29132	The binary relationship form of the singleton function. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- A e. _V   &    |- B e. _V   =>    |- ( ASingleton B <-> B = { A } )
Theorem	elsingles 29133*	Membership in the class of all singletons. (Contributed by Scott Fenton, 19-Feb-2013.)
|- ( A e. Singletons <-> E. x A = { x } )
Theorem	fnsingle 29134	The singleton relationship is a function over the universe. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- Singleton Fn _V
Theorem	fvsingle 29135	The value of the singleton function. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Revised by Scott Fenton, 13-Apr-2018.)
|- (Singleton ` A ) = { A }
Theorem	dfsingles2 29136*	Alternate definition of the class of all singletons. (Contributed by Scott Fenton, 20-Nov-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- Singletons = { x | E. y x = { y } }
Theorem	snelsingles 29137	A singleton is a member of the class of all singletons. (Contributed by Scott Fenton, 19-Feb-2013.)
|- A e. _V   =>    |- { A } e. Singletons
Theorem	dfiota3 29138	A definiton of iota using minimal quantifiers. (Contributed by Scott Fenton, 19-Feb-2013.)
|- ( iota x ph ) = U. U. ( { { x | ph } } i^i Singletons )
Theorem	dffv5 29139	Another quantifier free definition of function value. (Contributed by Scott Fenton, 19-Feb-2013.)
|- ( F ` A ) = U. U. ( { ( F " { A } ) } i^i Singletons )
Theorem	unisnif 29140	Express union of singleton in terms of if. (Contributed by Scott Fenton, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- U. { A } = if ( A e. _V , A , (/) )
Theorem	brimage 29141	Binary relationship form of the Image functor. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- A e. _V   &    |- B e. _V   =>    |- ( AImage R B <-> B = ( R " A ) )
Theorem	brimageg 29142	Closed form of brimage 29141. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- ( ( A e. V /\ B e. W ) -> ( AImage R B <-> B = ( R " A ) ) )
Theorem	funimage 29143	Image A is a function. (Contributed by Scott Fenton, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- Fun Image A
Theorem	fnimage 29144*	Image R is a function over the set-like portion of R. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- Image R Fn { x | ( R " x ) e. _V }
Theorem	imageval 29145*	The image functor in maps-to notation. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- Image R = ( x e. _V |-> ( R " x ) )
Theorem	fvimage 29146	The value of the image functor. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- ( ( A e. V /\ ( R " A ) e. W ) -> (Image R ` A ) = ( R " A ) )
Theorem	brcart 29147	Binary relationship form of the cartesian product operator. (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   =>    |- ( <. A , B >.Cart C <-> C = ( A X. B ) )
Theorem	brdomain 29148	The binary relationship form of the domain function. (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- A e. _V   &    |- B e. _V   =>    |- ( ADomain B <-> B = dom A )
Theorem	brrange 29149	The binary relationship form of the range function. (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- A e. _V   &    |- B e. _V   =>    |- ( ARange B <-> B = ran A )
Theorem	brdomaing 29150	Closed form of brdomain 29148. (Contributed by Scott Fenton, 2-May-2014.)
|- ( ( A e. V /\ B e. W ) -> ( ADomain B <-> B = dom A ) )
Theorem	brrangeg 29151	Closed form of brrange 29149. (Contributed by Scott Fenton, 3-May-2014.)
|- ( ( A e. V /\ B e. W ) -> ( ARange B <-> B = ran A ) )
Theorem	brimg 29152	The binary relationship form of the Img function. (Contributed by Scott Fenton, 12-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   =>    |- ( <. A , B >.Img C <-> C = ( A " B ) )
Theorem	brapply 29153	The binary relationship form of the Apply function. (Contributed by Scott Fenton, 12-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   =>    |- ( <. A , B >.Apply C <-> C = ( A ` B ) )
Theorem	brcup 29154	Binary relationship form of the Cup function. (Contributed by Scott Fenton, 14-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   =>    |- ( <. A , B >.Cup C <-> C = ( A u. B ) )
Theorem	brcap 29155	Binary relationship form of the Cap function. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   =>    |- ( <. A , B >.Cap C <-> C = ( A i^i B ) )
Theorem	brsuccf 29156	Binary relationship form of the Succ function. (Contributed by Scott Fenton, 14-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- A e. _V   &    |- B e. _V   =>    |- ( ASucc B <-> B = suc A )
Theorem	funpartlem 29157*	Lemma for funpartfun 29158. Show membership in the restriction. (Contributed by Scott Fenton, 4-Dec-2017.)
|- ( A e. dom ( (Image F o. Singleton ) i^i ( _V X. Singletons ) ) <-> E. x ( F " { A } ) = { x } )
Theorem	funpartfun 29158	The functional part of F is a function. (Contributed by Scott Fenton, 16-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- Fun Funpart F
Theorem	funpartss 29159	The functional part of F is a subset of F. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- Funpart F C_ F
Theorem	funpartfv 29160	The function value of the functional part is identical to the original functional value. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- (Funpart F ` A ) = ( F ` A )
Theorem	fullfunfnv 29161	The full functional part of F is a function over _V. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- FullFun F Fn _V
Theorem	fullfunfv 29162	The function value of the full function of F agrees with F. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- (FullFun F ` A ) = ( F ` A )
Theorem	brfullfun 29163	A binary relationship form condition for the full function. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- A e. _V   &    |- B e. _V   =>    |- ( AFullFun F B <-> B = ( F ` A ) )
Theorem	brrestrict 29164	The binary relationship form of the Restrict function. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   =>    |- ( <. A , B >.Restrict C <-> C = ( A |` B ) )
Theorem	dfrdg4 29165	A quantifier-free definition of the recursive definition generator. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- rec ( F , A ) = U. ( ( Funs i^i ( `'Domain " On ) ) \ dom ( ( `' _E o. Domain ) \ Fix ( `'Apply o. ( ( ( _V X. { (/) } ) X. { U. { A } } ) u. ( ( ( Bigcup o. Img ) |` ( _V X. Limits ) ) u. ( (FullFun F o. (Apply o. pprod ( _I , Bigcup ) ) ) |` ( _V X. ran Succ ) ) ) ) ) ) )
Theorem	tfrqfree 29166*	Calculate a quantifier-free version of the function from tfr1 7058 through tfr3 7060. (Contributed by Scott Fenton, 29-Apr-2014.)
|- ( ( Funs i^i ( `'Domain " On ) ) \ dom ( ( `' _E o. Domain ) \ Fix ( `'Apply o. (FullFun G o. Restrict ) ) ) ) = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( G ` ( f |` y ) ) ) }
Theorem	dfint3 29167	Quantifier-free definition of class intersection. (Contributed by Scott Fenton, 13-Apr-2018.)
|- |^| A = ( _V \ ( `' ( _V \ _E ) " A ) )
Theorem	imagesset 29168	The Image functor applied to the converse of the subset relationship yields a subset of the subset relationship. (Contributed by Scott Fenton, 14-Apr-2018.)
|- Image `' SSet C_ SSet
Theorem	brub 29169*	Binary relationship form of the upper bound functor. (Contributed by Scott Fenton, 3-May-2018.)
|- S e. _V   &    |- A e. _V   =>    |- ( SUB R A <-> A. x e. S x R A )
Theorem	brlb 29170*	Binary relationship form of the lower bound functor. (Contributed by Scott Fenton, 3-May-2018.)
|- S e. _V   &    |- A e. _V   =>    |- ( SLB R A <-> A. x e. S A R x )
21.8.39  Alternate ordered pairs
Syntax	caltop 29171	Declare the syntax for an alternate ordered pair.
class << A , B >>
Syntax	caltxp 29172	Declare the syntax for an alternate Cartesian product.
class ( A XX. B )
Definition	df-altop 29173	An alternative definition of ordered pairs. This definition removes a hypothesis from its defining theorem (see altopth 29184), making it more convenient in some circumstances. (Contributed by Scott Fenton, 22-Mar-2012.)
|- << A , B >> = { { A } , { A , { B } } }
Definition	df-altxp 29174*	Define Cartesian products of alternative ordered pairs. (Contributed by Scott Fenton, 23-Mar-2012.)
|- ( A XX. B ) = { z | E. x e. A E. y e. B z = << x , y >> }
Theorem	altopex 29175	Alternative ordered pairs always exist. (Contributed by Scott Fenton, 22-Mar-2012.)
|- << A , B >> e. _V
Theorem	altopthsn 29176	Two alternate ordered pairs are equal iff the singletons of their respective elements are equal. Note that this holds regardless of sethood of any of the elements. (Contributed by Scott Fenton, 16-Apr-2012.)
|- ( << A , B >> = << C , D >> <-> ( { A } = { C } /\ { B } = { D } ) )
Theorem	altopeq12 29177	Equality for alternate ordered pairs. (Contributed by Scott Fenton, 22-Mar-2012.)
|- ( ( A = B /\ C = D ) -> << A , C >> = << B , D >> )
Theorem	altopeq1 29178	Equality for alternate ordered pairs. (Contributed by Scott Fenton, 22-Mar-2012.)
|- ( A = B -> << A , C >> = << B , C >> )
Theorem	altopeq2 29179	Equality for alternate ordered pairs. (Contributed by Scott Fenton, 22-Mar-2012.)
|- ( A = B -> << C , A >> = << C , B >> )
Theorem	altopth1 29180	Equality of the first members of equal alternate ordered pairs, which holds regardless of the second members' sethood. (Contributed by Scott Fenton, 22-Mar-2012.)
|- ( A e. V -> ( << A , B >> = << C , D >> -> A = C ) )
Theorem	altopth2 29181	Equality of the second members of equal alternate ordered pairs, which holds regardless of the first members' sethood. (Contributed by Scott Fenton, 22-Mar-2012.)
|- ( B e. V -> ( << A , B >> = << C , D >> -> B = D ) )
Theorem	altopthg 29182	Alternate ordered pair theorem. (Contributed by Scott Fenton, 22-Mar-2012.)
|- ( ( A e. V /\ B e. W ) -> ( << A , B >> = << C , D >> <-> ( A = C /\ B = D ) ) )
Theorem	altopthbg 29183	Alternate ordered pair theorem. (Contributed by Scott Fenton, 14-Apr-2012.)
|- ( ( A e. V /\ D e. W ) -> ( << A , B >> = << C , D >> <-> ( A = C /\ B = D ) ) )
Theorem	altopth 29184	The alternate ordered pair theorem. If two alternate ordered pairs are equal, their first elements are equal and their second elements are equal. Note that C and D are not required to be a set due to a peculiarity of our specific ordered pair definition, as opposed to the regular ordered pairs used here, which (as in opth 4716), requires D to be a set. (Contributed by Scott Fenton, 23-Mar-2012.)
|- A e. _V   &    |- B e. _V   =>    |- ( << A , B >> = << C , D >> <-> ( A = C /\ B = D ) )
Theorem	altopthb 29185	Alternate ordered pair theorem with different sethood requirements. See altopth 29184 for more comments. (Contributed by Scott Fenton, 14-Apr-2012.)
|- A e. _V   &    |- D e. _V   =>    |- ( << A , B >> = << C , D >> <-> ( A = C /\ B = D ) )
Theorem	altopthc 29186	Alternate ordered pair theorem with different sethood requirements. See altopth 29184 for more comments. (Contributed by Scott Fenton, 14-Apr-2012.)
|- B e. _V   &    |- C e. _V   =>    |- ( << A , B >> = << C , D >> <-> ( A = C /\ B = D ) )
Theorem	altopthd 29187	Alternate ordered pair theorem with different sethood requirements. See altopth 29184 for more comments. (Contributed by Scott Fenton, 14-Apr-2012.)
|- C e. _V   &    |- D e. _V   =>    |- ( << A , B >> = << C , D >> <-> ( A = C /\ B = D ) )
Theorem	altxpeq1 29188	Equality for alternate Cartesian products. (Contributed by Scott Fenton, 24-Mar-2012.)
|- ( A = B -> ( A XX. C ) = ( B XX. C ) )
Theorem	altxpeq2 29189	Equality for alternate Cartesian products. (Contributed by Scott Fenton, 24-Mar-2012.)
|- ( A = B -> ( C XX. A ) = ( C XX. B ) )
Theorem	elaltxp 29190*	Membership in alternate Cartesian products. (Contributed by Scott Fenton, 23-Mar-2012.)
|- ( X e. ( A XX. B ) <-> E. x e. A E. y e. B X = << x , y >> )
Theorem	altopelaltxp 29191	Alternate ordered pair membership in a Cartesian product. Note that, unlike opelxp 5023, there is no sethood requirement here. (Contributed by Scott Fenton, 22-Mar-2012.)
|- ( << X , Y >> e. ( A XX. B ) <-> ( X e. A /\ Y e. B ) )
Theorem	altxpsspw 29192	An inclusion rule for alternate Cartesian products. (Contributed by Scott Fenton, 24-Mar-2012.)
|- ( A XX. B ) C_ ~P ~P ( A u. ~P B )
Theorem	altxpexg 29193	The alternate Cartesian product of two sets is a set. (Contributed by Scott Fenton, 24-Mar-2012.)
|- ( ( A e. V /\ B e. W ) -> ( A XX. B ) e. _V )
Theorem	rankaltopb 29194	Compute the rank of an alternate ordered pair. (Contributed by Scott Fenton, 18-Dec-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> ( rank ` << A , B >> ) = suc suc ( ( rank ` A ) u. suc ( rank ` B ) ) )
Theorem	nfaltop 29195	Bound-variable hypothesis builder for alternate ordered pairs. (Contributed by Scott Fenton, 25-Sep-2015.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/_ x << A , B >>
Theorem	sbcaltop 29196*	Distribution of class substitution over alternate ordered pairs. (Contributed by Scott Fenton, 25-Sep-2015.)
|- ( A e. _V -> [_ A / x ]_ << C , D >> = << [_ A / x ]_ C , [_ A / x ]_ D >> )
21.8.40  Geometry in the Euclidean space
21.8.40.1  Congruence properties
Syntax	cofs 29197	Declare the syntax for the outer five segment configuration.
class OuterFiveSeg
Definition	df-ofs 29198*	The outer five segment configuration is an abbreviation for the conditions of the Five Segment Axiom (ax5seg 23912). See brofs 29220 and 5segofs 29221 for how it is used. Definition 2.10 of [Schwabhauser] p. 28. (Contributed by Scott Fenton, 21-Sep-2013.)
|- OuterFiveSeg = { <. p , q >. | E. n e. NN E. a e. ( EE ` n ) E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) E. x e. ( EE ` n ) E. y e. ( EE ` n ) E. z e. ( EE ` n ) E. w e. ( EE ` n ) ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. x , y >. , <. z , w >. >. /\ ( ( b Btwn <. a , c >. /\ y Btwn <. x , z >. ) /\ ( <. a , b >.Cgr <. x , y >. /\ <. b , c >.Cgr <. y , z >. ) /\ ( <. a , d >.Cgr <. x , w >. /\ <. b , d >.Cgr <. y , w >. ) ) ) }
Theorem	cgrrflx2d 29199	Deduction form of axcgrrflx 23888. (Contributed by Scott Fenton, 13-Oct-2013.)
|- ( ph -> N e. NN )   &    |- ( ph -> A e. ( EE ` N ) )   &    |- ( ph -> B e. ( EE ` N ) )   =>    |- ( ph -> <. A , B >.Cgr <. B , A >. )
Theorem	cgrtr4d 29200	Deduction form of axcgrtr 23889. (Contributed by Scott Fenton, 13-Oct-2013.)
|- ( ph -> N e. NN )   &    |- ( ph -> A e. ( EE ` N ) )   &    |- ( ph -> B e. ( EE ` N ) )   &    |- ( ph -> C e. ( EE ` N ) )   &    |- ( ph -> D e. ( EE ` N ) )   &    |- ( ph -> E e. ( EE ` N ) )   &    |- ( ph -> F e. ( EE ` N ) )   &    |- ( ph -> <. A , B >.Cgr <. C , D >. )   &    |- ( ph -> <. A , B >.Cgr <. E , F >. )   =>    |- ( ph -> <. C , D >.Cgr <. E , F >. )