P. 366 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36501-36600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	elfunsg 36501	Closed form of elfuns 36500. (Contributed by Scott Fenton, 2-May-2014.)
⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ Funs ↔ Fun 𝐹))
Theorem	brsingle 36502	The binary relation form of the singleton function. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴Singleton𝐵 ↔ 𝐵 = {𝐴})
Theorem	elsingles 36503*	Membership in the class of all singletons. (Contributed by Scott Fenton, 19-Feb-2013.)
⊢ (𝐴 ∈ Singletons ↔ ∃𝑥 𝐴 = {𝑥})
Theorem	fnsingle 36504	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 36505	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‘𝐴) = {𝐴}
Theorem	dfsingles2 36506*	Alternate definition of the class of all singletons. (Contributed by Scott Fenton, 20-Nov-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ Singletons = {𝑥 ∣ ∃𝑦 𝑥 = {𝑦}}
Theorem	snelsingles 36507	A singleton is a member of the class of all singletons. (Contributed by Scott Fenton, 19-Feb-2013.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {𝐴} ∈ Singletons
Theorem	dfiota3 36508	A definition of iota using minimal quantifiers. (Contributed by Scott Fenton, 19-Feb-2013.)
⊢ (℩𝑥𝜑) = ∪ ∪ ({{𝑥 ∣ 𝜑}} ∩ Singletons )
Theorem	dffv5 36509	Another quantifier-free definition of function value. (Contributed by Scott Fenton, 19-Feb-2013.)
⊢ (𝐹‘𝐴) = ∪ ∪ ({(𝐹 “ {𝐴})} ∩ Singletons )
Theorem	unisnif 36510	Express union of singleton in terms of if. (Contributed by Scott Fenton, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ∪ {𝐴} = if(𝐴 ∈ V, 𝐴, ∅)
Theorem	brimage 36511	Binary relation form of the Image functor. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴Image𝑅𝐵 ↔ 𝐵 = (𝑅 “ 𝐴))
Theorem	brimageg 36512	Closed form of brimage 36511. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴Image𝑅𝐵 ↔ 𝐵 = (𝑅 “ 𝐴)))
Theorem	funimage 36513	Image𝐴 is a function. (Contributed by Scott Fenton, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ Fun Image𝐴
Theorem	fnimage 36514*	Image𝑅 is a function over the set-like portion of 𝑅. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ Image𝑅 Fn {𝑥 ∣ (𝑅 “ 𝑥) ∈ V}
Theorem	imageval 36515*	The image functor in maps-to notation. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ Image𝑅 = (𝑥 ∈ V ↦ (𝑅 “ 𝑥))
Theorem	fvimage 36516	Value of the image functor. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑅 “ 𝐴) ∈ 𝑊) → (Image𝑅‘𝐴) = (𝑅 “ 𝐴))
Theorem	brcart 36517	Binary relation form of the cartesian product operator. (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩Cart𝐶 ↔ 𝐶 = (𝐴 × 𝐵))
Theorem	brdomain 36518	Binary relation form of the domain function. (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴Domain𝐵 ↔ 𝐵 = dom 𝐴)
Theorem	brrange 36519	Binary relation form of the range function. (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴Range𝐵 ↔ 𝐵 = ran 𝐴)
Theorem	brdomaing 36520	Closed form of brdomain 36518. (Contributed by Scott Fenton, 2-May-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴Domain𝐵 ↔ 𝐵 = dom 𝐴))
Theorem	brrangeg 36521	Closed form of brrange 36519. (Contributed by Scott Fenton, 3-May-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴Range𝐵 ↔ 𝐵 = ran 𝐴))
Theorem	brimg 36522	Binary relation form of the Img function. (Contributed by Scott Fenton, 12-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩Img𝐶 ↔ 𝐶 = (𝐴 “ 𝐵))
Theorem	brapply 36523	Binary relation form of the Apply function. (Contributed by Scott Fenton, 12-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩Apply𝐶 ↔ 𝐶 = (𝐴‘𝐵))
Theorem	brcup 36524	Binary relation form of the Cup function. (Contributed by Scott Fenton, 14-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩Cup𝐶 ↔ 𝐶 = (𝐴 ∪ 𝐵))
Theorem	brcap 36525	Binary relation form of the Cap function. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩Cap𝐶 ↔ 𝐶 = (𝐴 ∩ 𝐵))
Theorem	lemsuccf 36526*	Lemma for unfolding different forms of the Succ function. (Contributed by Scott Fenton, 14-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (∃𝑥(𝐴( I ⊗ Singleton)𝑥 ∧ 𝑥Cup𝐵) ↔ 𝐵 = suc 𝐴)
Theorem	brsuccf 36527	Binary relation form of the Succ function. (Contributed by Scott Fenton, 14-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴Succ𝐵 ↔ 𝐵 = suc 𝐴)
Theorem	dfsuccf2 36528*	Alternate definition of Scott Fenton's version of Succ, cf. df-sucmap 39218. (Contributed by Peter Mazsa, 6-Jan-2026.)
⊢ Succ = {⟨𝑚, 𝑛⟩ ∣ suc 𝑚 = 𝑛}
Theorem	funpartlem 36529*	Lemma for funpartfun 36530. Show membership in the restriction. (Contributed by Scott Fenton, 4-Dec-2017.)
⊢ (𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )) ↔ ∃𝑥(𝐹 “ {𝐴}) = {𝑥})
Theorem	funpartfun 36530	The functional part of 𝐹 is a function. (Contributed by Scott Fenton, 16-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ Fun Funpart𝐹
Theorem	funpartss 36531	The functional part of 𝐹 is a subset of 𝐹. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ Funpart𝐹 ⊆ 𝐹
Theorem	funpartfv 36532	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𝐹‘𝐴) = (𝐹‘𝐴)
Theorem	fullfunfnv 36533	The full functional part of 𝐹 is a function over V. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ FullFun𝐹 Fn V
Theorem	fullfunfv 36534	The function value of the full function of 𝐹 agrees with 𝐹. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (FullFun𝐹‘𝐴) = (𝐹‘𝐴)
Theorem	brfullfun 36535	A binary relation form condition for the full function. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴FullFun𝐹𝐵 ↔ 𝐵 = (𝐹‘𝐴))
Theorem	brrestrict 36536	Binary relation form of the Restrict function. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩Restrict𝐶 ↔ 𝐶 = (𝐴 ↾ 𝐵))
Theorem	dfrecs2 36537	A quantifier-free definition of recs. (Contributed by Scott Fenton, 17-Jul-2020.)
⊢ recs(𝐹) = ∪ (( Funs ∩ (◡Domain “ On)) ∖ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict))))
Theorem	dfrdg4 36538	A quantifier-free definition of the recursive definition generator. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ rec(𝐹, 𝐴) = ∪ (( Funs ∩ (◡Domain “ On)) ∖ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))))))
Theorem	dfint3 36539	Quantifier-free definition of class intersection. (Contributed by Scott Fenton, 13-Apr-2018.)
⊢ ∩ 𝐴 = (V ∖ (◡(V ∖ E ) “ 𝐴))
Theorem	imagesset 36540	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 ⊆ SSet
Theorem	brub 36541*	Binary relation form of the upper bound functor. (Contributed by Scott Fenton, 3-May-2018.)
⊢ 𝑆 ∈ V    &   ⊢ 𝐴 ∈ V    ⇒   ⊢ (𝑆UB𝑅𝐴 ↔ ∀𝑥 ∈ 𝑆 𝑥𝑅𝐴)
Theorem	brlb 36542*	Binary relation form of the lower bound functor. (Contributed by Scott Fenton, 3-May-2018.)
⊢ 𝑆 ∈ V    &   ⊢ 𝐴 ∈ V    ⇒   ⊢ (𝑆LB𝑅𝐴 ↔ ∀𝑥 ∈ 𝑆 𝐴𝑅𝑥)
Theorem	dffr7 36543	Alternate quantifier-free definition of a well-founded relation. (Contributed by Scott Fenton, 26-Aug-2026.)
⊢ (𝑅 Fr 𝐴 ↔ (𝒫 𝐴 ∖ {∅}) ⊆ Fix ( E ∘ (V ∖ (𝑅 ∘ ◡ E ))))
21.11.16  Alternate ordered pairs
Syntax	caltop 36544	Declare the syntax for an alternate ordered pair.
class ⟪𝐴, 𝐵⟫
Syntax	caltxp 36545	Declare the syntax for an alternate Cartesian product.
class (𝐴 ×× 𝐵)
Definition	df-altop 36546	An alternative definition of ordered pairs. This definition removes a hypothesis from its defining theorem (see altopth 36557), making it more convenient in some circumstances. (Contributed by Scott Fenton, 22-Mar-2012.)
⊢ ⟪𝐴, 𝐵⟫ = {{𝐴}, {𝐴, {𝐵}}}
Definition	df-altxp 36547*	Define Cartesian products of alternative ordered pairs. (Contributed by Scott Fenton, 23-Mar-2012.)
⊢ (𝐴 ×× 𝐵) = {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = ⟪𝑥, 𝑦⟫}
Theorem	altopex 36548	Alternative ordered pairs always exist. (Contributed by Scott Fenton, 22-Mar-2012.)
⊢ ⟪𝐴, 𝐵⟫ ∈ V
Theorem	altopthsn 36549	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.)
⊢ (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ ({𝐴} = {𝐶} ∧ {𝐵} = {𝐷}))
Theorem	altopeq12 36550	Equality for alternate ordered pairs. (Contributed by Scott Fenton, 22-Mar-2012.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → ⟪𝐴, 𝐶⟫ = ⟪𝐵, 𝐷⟫)
Theorem	altopeq1 36551	Equality for alternate ordered pairs. (Contributed by Scott Fenton, 22-Mar-2012.)
⊢ (𝐴 = 𝐵 → ⟪𝐴, 𝐶⟫ = ⟪𝐵, 𝐶⟫)
Theorem	altopeq2 36552	Equality for alternate ordered pairs. (Contributed by Scott Fenton, 22-Mar-2012.)
⊢ (𝐴 = 𝐵 → ⟪𝐶, 𝐴⟫ = ⟪𝐶, 𝐵⟫)
Theorem	altopth1 36553	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.)
⊢ (𝐴 ∈ 𝑉 → (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ → 𝐴 = 𝐶))
Theorem	altopth2 36554	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.)
⊢ (𝐵 ∈ 𝑉 → (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ → 𝐵 = 𝐷))
Theorem	altopthg 36555	Alternate ordered pair theorem. (Contributed by Scott Fenton, 22-Mar-2012.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
Theorem	altopthbg 36556	Alternate ordered pair theorem. (Contributed by Scott Fenton, 14-Apr-2012.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) → (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
Theorem	altopth 36557	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 𝐶 and 𝐷 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 5456), requires 𝐷 to be a set. (Contributed by Scott Fenton, 23-Mar-2012.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	altopthb 36558	Alternate ordered pair theorem with different sethood requirements. See altopth 36557 for more comments. (Contributed by Scott Fenton, 14-Apr-2012.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	altopthc 36559	Alternate ordered pair theorem with different sethood requirements. See altopth 36557 for more comments. (Contributed by Scott Fenton, 14-Apr-2012.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	altopthd 36560	Alternate ordered pair theorem with different sethood requirements. See altopth 36557 for more comments. (Contributed by Scott Fenton, 14-Apr-2012.)
⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	altxpeq1 36561	Equality for alternate Cartesian products. (Contributed by Scott Fenton, 24-Mar-2012.)
⊢ (𝐴 = 𝐵 → (𝐴 ×× 𝐶) = (𝐵 ×× 𝐶))
Theorem	altxpeq2 36562	Equality for alternate Cartesian products. (Contributed by Scott Fenton, 24-Mar-2012.)
⊢ (𝐴 = 𝐵 → (𝐶 ×× 𝐴) = (𝐶 ×× 𝐵))
Theorem	elaltxp 36563*	Membership in alternate Cartesian products. (Contributed by Scott Fenton, 23-Mar-2012.)
⊢ (𝑋 ∈ (𝐴 ×× 𝐵) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑋 = ⟪𝑥, 𝑦⟫)
Theorem	altopelaltxp 36564	Alternate ordered pair membership in a Cartesian product. Note that, unlike opelxp 5695, there is no sethood requirement here. (Contributed by Scott Fenton, 22-Mar-2012.)
⊢ (⟪𝑋, 𝑌⟫ ∈ (𝐴 ×× 𝐵) ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵))
Theorem	altxpsspw 36565	An inclusion rule for alternate Cartesian products. (Contributed by Scott Fenton, 24-Mar-2012.)
⊢ (𝐴 ×× 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝒫 𝐵)
Theorem	altxpexg 36566	The alternate Cartesian product of two sets is a set. (Contributed by Scott Fenton, 24-Mar-2012.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ×× 𝐵) ∈ V)
Theorem	rankaltopb 36567	Compute the rank of an alternate ordered pair. (Contributed by Scott Fenton, 18-Dec-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ ∪ (𝑅1 “ On)) → (rank‘⟪𝐴, 𝐵⟫) = suc suc ((rank‘𝐴) ∪ suc (rank‘𝐵)))
Theorem	nfaltop 36568	Bound-variable hypothesis builder for alternate ordered pairs. (Contributed by Scott Fenton, 25-Sep-2015.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥⟪𝐴, 𝐵⟫
Theorem	sbcaltop 36569*	Distribution of class substitution over alternate ordered pairs. (Contributed by Scott Fenton, 25-Sep-2015.)
⊢ (𝐴 ∈ V → ⦋𝐴 / 𝑥⦌⟪𝐶, 𝐷⟫ = ⟪⦋𝐴 / 𝑥⦌𝐶, ⦋𝐴 / 𝑥⦌𝐷⟫)
21.11.17  Geometry in the Euclidean space
21.11.17.1  Congruence properties
Syntax	cofs 36570	Declare the syntax for the outer five segment configuration.
class OuterFiveSeg
Definition	df-ofs 36571*	The outer five segment configuration is an abbreviation for the conditions of the Five Segment Axiom (ax5seg 29403). See brofs 36593 and 5segofs 36594 for how it is used. Definition 2.10 of [Schwabhauser] p. 28. (Contributed by Scott Fenton, 21-Sep-2013.)
⊢ OuterFiveSeg = {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)))}
Theorem	cgrrflx2d 36572	Deduction form of axcgrrflx 29379. (Contributed by Scott Fenton, 13-Oct-2013.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁))    ⇒   ⊢ (𝜑 → ⟨𝐴, 𝐵⟩Cgr⟨𝐵, 𝐴⟩)
Theorem	cgrtr4d 36573	Deduction form of axcgrtr 29380. (Contributed by Scott Fenton, 13-Oct-2013.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐸 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐹 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩)    &   ⊢ (𝜑 → ⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩)    ⇒   ⊢ (𝜑 → ⟨𝐶, 𝐷⟩Cgr⟨𝐸, 𝐹⟩)
Theorem	cgrtr4and 36574	Deduction form of axcgrtr 29380. (Contributed by Scott Fenton, 13-Oct-2013.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐸 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐹 ∈ (𝔼‘𝑁))    &   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩)    &   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐶, 𝐷⟩Cgr⟨𝐸, 𝐹⟩)
Theorem	cgrrflx 36575	Reflexivity law for congruence. Theorem 2.1 of [Schwabhauser] p. 27. (Contributed by Scott Fenton, 12-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → ⟨𝐴, 𝐵⟩Cgr⟨𝐴, 𝐵⟩)
Theorem	cgrrflxd 36576	Deduction form of cgrrflx 36575. (Contributed by Scott Fenton, 13-Oct-2013.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁))    ⇒   ⊢ (𝜑 → ⟨𝐴, 𝐵⟩Cgr⟨𝐴, 𝐵⟩)
Theorem	cgrcomim 36577	Congruence commutes on the two sides. Implication version. Theorem 2.2 of [Schwabhauser] p. 27. (Contributed by Scott Fenton, 12-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩ → ⟨𝐶, 𝐷⟩Cgr⟨𝐴, 𝐵⟩))
Theorem	cgrcom 36578	Congruence commutes between the two sides. (Contributed by Scott Fenton, 12-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩ ↔ ⟨𝐶, 𝐷⟩Cgr⟨𝐴, 𝐵⟩))
Theorem	cgrcomand 36579	Deduction form of cgrcom 36578. (Contributed by Scott Fenton, 13-Oct-2013.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁))    &   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐶, 𝐷⟩Cgr⟨𝐴, 𝐵⟩)
Theorem	cgrtr 36580	Transitivity law for congruence. Theorem 2.3 of [Schwabhauser] p. 27. (Contributed by Scott Fenton, 24-Sep-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → ((⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐸, 𝐹⟩) → ⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩))
Theorem	cgrtrand 36581	Deduction form of cgrtr 36580. (Contributed by Scott Fenton, 13-Oct-2013.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐸 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐹 ∈ (𝔼‘𝑁))    &   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩)    &   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐶, 𝐷⟩Cgr⟨𝐸, 𝐹⟩)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩)
Theorem	cgrtr3 36582	Transitivity law for congruence. (Contributed by Scott Fenton, 7-Oct-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → ((⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐸, 𝐹⟩) → ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩))
Theorem	cgrtr3and 36583	Deduction form of cgrtr3 36582. (Contributed by Scott Fenton, 13-Oct-2013.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐸 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐹 ∈ (𝔼‘𝑁))    &   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩)    &   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐶, 𝐷⟩Cgr⟨𝐸, 𝐹⟩)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩)
Theorem	cgrcoml 36584	Congruence commutes on the left. Biconditional version of Theorem 2.4 of [Schwabhauser] p. 27. (Contributed by Scott Fenton, 12-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩ ↔ ⟨𝐵, 𝐴⟩Cgr⟨𝐶, 𝐷⟩))
Theorem	cgrcomr 36585	Congruence commutes on the right. Biconditional version of Theorem 2.5 of [Schwabhauser] p. 27. (Contributed by Scott Fenton, 12-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩ ↔ ⟨𝐴, 𝐵⟩Cgr⟨𝐷, 𝐶⟩))
Theorem	cgrcomlr 36586	Congruence commutes on both sides. (Contributed by Scott Fenton, 12-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩ ↔ ⟨𝐵, 𝐴⟩Cgr⟨𝐷, 𝐶⟩))
Theorem	cgrcomland 36587	Deduction form of cgrcoml 36584. (Contributed by Scott Fenton, 14-Oct-2013.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁))    &   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐵, 𝐴⟩Cgr⟨𝐶, 𝐷⟩)
Theorem	cgrcomrand 36588	Deduction form of cgrcoml 36584. (Contributed by Scott Fenton, 14-Oct-2013.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁))    &   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐴, 𝐵⟩Cgr⟨𝐷, 𝐶⟩)
Theorem	cgrcomlrand 36589	Deduction form of cgrcomlr 36586. (Contributed by Scott Fenton, 14-Oct-2013.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁))    &   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐵, 𝐴⟩Cgr⟨𝐷, 𝐶⟩)
Theorem	cgrtriv 36590	Degenerate segments are congruent. Theorem 2.8 of [Schwabhauser] p. 28. (Contributed by Scott Fenton, 12-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → ⟨𝐴, 𝐴⟩Cgr⟨𝐵, 𝐵⟩)
Theorem	cgrid2 36591	Identity law for congruence. (Contributed by Scott Fenton, 12-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (⟨𝐴, 𝐴⟩Cgr⟨𝐵, 𝐶⟩ → 𝐵 = 𝐶))
Theorem	cgrdegen 36592	Two congruent segments are either both degenerate or both nondegenerate. (Contributed by Scott Fenton, 12-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩ → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷)))
Theorem	brofs 36593	Binary relation form of the outer five segment predicate. (Contributed by Scott Fenton, 21-Sep-2013.)
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ OuterFiveSeg ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))))
Theorem	5segofs 36594	Rephrase ax5seg 29403 using the outer five segment predicate. Theorem 2.10 of [Schwabhauser] p. 28. (Contributed by Scott Fenton, 21-Sep-2013.)
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ OuterFiveSeg ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ∧ 𝐴 ≠ 𝐵) → ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))
Theorem	ofscom 36595	The outer five segment predicate commutes. (Contributed by Scott Fenton, 26-Sep-2013.)
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ OuterFiveSeg ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ OuterFiveSeg ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩))
Theorem	cgrextend 36596	Link congruence over a pair of line segments. Theorem 2.11 of [Schwabhauser] p. 29. (Contributed by Scott Fenton, 12-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝐹⟩) ∧ (⟨𝐴, 𝐵⟩Cgr⟨𝐷, 𝐸⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐸, 𝐹⟩)) → ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩))
Theorem	cgrextendand 36597	Deduction form of cgrextend 36596. (Contributed by Scott Fenton, 14-Oct-2013.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐸 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐹 ∈ (𝔼‘𝑁))    &   ⊢ ((𝜑 ∧ 𝜓) → 𝐵 Btwn ⟨𝐴, 𝐶⟩)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝐸 Btwn ⟨𝐷, 𝐹⟩)    &   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐴, 𝐵⟩Cgr⟨𝐷, 𝐸⟩)    &   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐵, 𝐶⟩Cgr⟨𝐸, 𝐹⟩)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩)
Theorem	segconeq 36598	Two points that satisfy the conclusion of axsegcon 29392 are identical. Uniqueness portion of Theorem 2.12 of [Schwabhauser] p. 29. (Contributed by Scott Fenton, 12-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑋 ∈ (𝔼‘𝑁) ∧ 𝑌 ∈ (𝔼‘𝑁))) → ((𝑄 ≠ 𝐴 ∧ (𝐴 Btwn ⟨𝑄, 𝑋⟩ ∧ ⟨𝐴, 𝑋⟩Cgr⟨𝐵, 𝐶⟩) ∧ (𝐴 Btwn ⟨𝑄, 𝑌⟩ ∧ ⟨𝐴, 𝑌⟩Cgr⟨𝐵, 𝐶⟩)) → 𝑋 = 𝑌))
Theorem	segconeu 36599*	Existential uniqueness version of segconeq 36598. (Contributed by Scott Fenton, 19-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ 𝐶 ≠ 𝐷)) → ∃!𝑟 ∈ (𝔼‘𝑁)(𝐷 Btwn ⟨𝐶, 𝑟⟩ ∧ ⟨𝐷, 𝑟⟩Cgr⟨𝐴, 𝐵⟩))
21.11.17.2  Betweenness properties
Theorem	btwntriv2 36600	Betweenness always holds for the second endpoint. Theorem 3.1 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 12-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 𝐵 Btwn ⟨𝐴, 𝐵⟩)