P. 359 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35801-35900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	wlimeq1 35801	Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.)
⊢ (𝑅 = 𝑆 → WLim(𝑅, 𝐴) = WLim(𝑆, 𝐴))
Theorem	wlimeq2 35802	Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.)
⊢ (𝐴 = 𝐵 → WLim(𝑅, 𝐴) = WLim(𝑅, 𝐵))
Theorem	nfwlim 35803	Bound-variable hypothesis builder for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.)
⊢ Ⅎ𝑥𝑅    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥WLim(𝑅, 𝐴)
Theorem	elwlim 35804	Membership in the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) (Revised by AV, 10-Oct-2021.)
⊢ (𝑋 ∈ WLim(𝑅, 𝐴) ↔ (𝑋 ∈ 𝐴 ∧ 𝑋 ≠ inf(𝐴, 𝐴, 𝑅) ∧ 𝑋 = sup(Pred(𝑅, 𝐴, 𝑋), 𝐴, 𝑅)))
Theorem	wzel 35805	The zero of a well-founded set is a member of that set. (Contributed by Scott Fenton, 13-Jun-2018.) (Revised by AV, 10-Oct-2021.)
⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐴 ≠ ∅) → inf(𝐴, 𝐴, 𝑅) ∈ 𝐴)
Theorem	wsuclem 35806*	Lemma for the supremum properties of well-founded successor. (Contributed by Scott Fenton, 15-Jun-2018.) (Revised by AV, 10-Oct-2021.)
⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → ∃𝑤 ∈ 𝐴 𝑋𝑅𝑤)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ Pred (◡𝑅, 𝐴, 𝑋) ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ Pred (◡𝑅, 𝐴, 𝑋)𝑧𝑅𝑦)))
Theorem	wsucex 35807	Existence theorem for well-founded successor. (Contributed by Scott Fenton, 16-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.)
⊢ (𝜑 → 𝑅 Or 𝐴)    ⇒   ⊢ (𝜑 → wsuc(𝑅, 𝐴, 𝑋) ∈ V)
Theorem	wsuccl 35808*	If 𝑋 is a set with an 𝑅 successor in 𝐴, then its well-founded successor is a member of 𝐴. (Contributed by Scott Fenton, 15-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.)
⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → ∃𝑦 ∈ 𝐴 𝑋𝑅𝑦)    ⇒   ⊢ (𝜑 → wsuc(𝑅, 𝐴, 𝑋) ∈ 𝐴)
Theorem	wsuclb 35809	A well-founded successor is a lower bound on points after 𝑋. (Contributed by Scott Fenton, 16-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.)
⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋𝑅𝑌)    ⇒   ⊢ (𝜑 → ¬ 𝑌𝑅wsuc(𝑅, 𝐴, 𝑋))
Theorem	wlimss 35810	The class of limit points is a subclass of the base class. (Contributed by Scott Fenton, 16-Jun-2018.)
⊢ WLim(𝑅, 𝐴) ⊆ 𝐴
21.11.16  Quantifier-free definitions
Syntax	ctxp 35811	Declare the syntax for tail Cartesian product.
class (𝐴 ⊗ 𝐵)
Syntax	cpprod 35812	Declare the syntax for the parallel product.
class pprod(𝑅, 𝑆)
Syntax	csset 35813	Declare the subset relationship class.
class SSet
Syntax	ctrans 35814	Declare the transitive set class.
class Trans
Syntax	cbigcup 35815	Declare the set union relationship.
class Bigcup
Syntax	cfix 35816	Declare the syntax for the fixpoints of a class.
class Fix 𝐴
Syntax	climits 35817	Declare the class of limit ordinals.
class Limits
Syntax	cfuns 35818	Declare the syntax for the class of all function.
class Funs
Syntax	csingle 35819	Declare the syntax for the singleton function.
class Singleton
Syntax	csingles 35820	Declare the syntax for the class of all singletons.
class Singletons
Syntax	cimage 35821	Declare the syntax for the image functor.
class Image𝐴
Syntax	ccart 35822	Declare the syntax for the cartesian function.
class Cart
Syntax	cimg 35823	Declare the syntax for the image function.
class Img
Syntax	cdomain 35824	Declare the syntax for the domain function.
class Domain
Syntax	crange 35825	Declare the syntax for the range function.
class Range
Syntax	capply 35826	Declare the syntax for the application function.
class Apply
Syntax	ccup 35827	Declare the syntax for the cup function.
class Cup
Syntax	ccap 35828	Declare the syntax for the cap function.
class Cap
Syntax	csuccf 35829	Declare the syntax for the successor function.
class Succ
Syntax	cfunpart 35830	Declare the syntax for the functional part functor.
class Funpart𝐹
Syntax	cfullfn 35831	Declare the syntax for the full function functor.
class FullFun𝐹
Syntax	crestrict 35832	Declare the syntax for the restriction function.
class Restrict
Syntax	cub 35833	Declare the syntax for the upper bound relationship functor.
class UB𝑅
Syntax	clb 35834	Declare the syntax for the lower bound relationship functor.
class LB𝑅
Definition	df-txp 35835	Define the tail cross of two classes. Membership in this class is defined by txpss3v 35859 and brtxp 35861. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ (𝐴 ⊗ 𝐵) = ((◡(1st ↾ (V × V)) ∘ 𝐴) ∩ (◡(2nd ↾ (V × V)) ∘ 𝐵))
Definition	df-pprod 35836	Define the parallel product of two classes. Membership in this class is defined by pprodss4v 35865 and brpprod 35866. (Contributed by Scott Fenton, 11-Apr-2014.)
⊢ pprod(𝐴, 𝐵) = ((𝐴 ∘ (1st ↾ (V × V))) ⊗ (𝐵 ∘ (2nd ↾ (V × V))))
Definition	df-sset 35837	Define the subset class. For the value, see brsset 35870. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ SSet = ((V × V) ∖ ran ( E ⊗ (V ∖ E )))
Definition	df-trans 35838	Define the class of all transitive sets. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ Trans = (V ∖ ran (( E ∘ E ) ∖ E ))
Definition	df-bigcup 35839	Define the Bigcup function, which, per fvbigcup 35883, carries a set to its union. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ Bigcup = ((V × V) ∖ ran ((V ⊗ E ) △ (( E ∘ E ) ⊗ V)))
Definition	df-fix 35840	Define the class of all fixpoints of a relationship. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ Fix 𝐴 = dom (𝐴 ∩ I )
Definition	df-limits 35841	Define the class of all limit ordinals. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ Limits = ((On ∩ Fix Bigcup ) ∖ {∅})
Definition	df-funs 35842	Define the class of all functions. See elfuns 35896 for membership. (Contributed by Scott Fenton, 18-Feb-2013.)
⊢ Funs = (𝒫 (V × V) ∖ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E )))
Definition	df-singleton 35843	Define the singleton function. See brsingle 35898 for its value. (Contributed by Scott Fenton, 4-Apr-2014.)
⊢ Singleton = ((V × V) ∖ ran ((V ⊗ E ) △ ( I ⊗ V)))
Definition	df-singles 35844	Define the class of all singletons. See elsingles 35899 for membership. (Contributed by Scott Fenton, 19-Feb-2013.)
⊢ Singletons = ran Singleton
Definition	df-image 35845	Define the image functor. This function takes a set 𝐴 to a function 𝑥 ↦ (𝐴 “ 𝑥), providing that the latter exists. See imageval 35911 for the derivation. (Contributed by Scott Fenton, 27-Mar-2014.)
⊢ Image𝐴 = ((V × V) ∖ ran ((V ⊗ E ) △ (( E ∘ ◡𝐴) ⊗ V)))
Definition	df-cart 35846	Define the cartesian product function. See brcart 35913 for its value. (Contributed by Scott Fenton, 11-Apr-2014.)
⊢ Cart = (((V × V) × V) ∖ ran ((V ⊗ E ) △ (pprod( E , E ) ⊗ V)))
Definition	df-img 35847	Define the image function. See brimg 35918 for its value. (Contributed by Scott Fenton, 12-Apr-2014.)
⊢ Img = (Image((2nd ∘ 1st ) ↾ (1st ↾ (V × V))) ∘ Cart)
Definition	df-domain 35848	Define the domain function. See brdomain 35914 for its value. (Contributed by Scott Fenton, 11-Apr-2014.)
⊢ Domain = Image(1st ↾ (V × V))
Definition	df-range 35849	Define the range function. See brrange 35915 for its value. (Contributed by Scott Fenton, 11-Apr-2014.)
⊢ Range = Image(2nd ↾ (V × V))
Definition	df-cup 35850	Define the little cup function. See brcup 35920 for its value. (Contributed by Scott Fenton, 14-Apr-2014.)
⊢ Cup = (((V × V) × V) ∖ ran ((V ⊗ E ) △ (((◡1st ∘ E ) ∪ (◡2nd ∘ E )) ⊗ V)))
Definition	df-cap 35851	Define the little cap function. See brcap 35921 for its value. (Contributed by Scott Fenton, 17-Apr-2014.)
⊢ Cap = (((V × V) × V) ∖ ran ((V ⊗ E ) △ (((◡1st ∘ E ) ∩ (◡2nd ∘ E )) ⊗ V)))
Definition	df-restrict 35852	Define the restriction function. See brrestrict 35930 for its value. (Contributed by Scott Fenton, 17-Apr-2014.)
⊢ Restrict = (Cap ∘ (1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st )))))
Definition	df-succf 35853	Define the successor function. See brsuccf 35922 for its value. (Contributed by Scott Fenton, 14-Apr-2014.)
⊢ Succ = (Cup ∘ ( I ⊗ Singleton))
Definition	df-apply 35854	Define the application function. See brapply 35919 for its value. (Contributed by Scott Fenton, 12-Apr-2014.)
⊢ Apply = (( Bigcup ∘ Bigcup ) ∘ (((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))) ∘ ((Singleton ∘ Img) ∘ pprod( I , Singleton))))
Definition	df-funpart 35855	Define the functional part of a class 𝐹. This is the maximal part of 𝐹 that is a function. See funpartfun 35924 and funpartfv 35926 for the meaning of this statement. (Contributed by Scott Fenton, 16-Apr-2014.)
⊢ Funpart𝐹 = (𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))
Definition	df-fullfun 35856	Define the full function over 𝐹. This is a function with domain V that always agrees with 𝐹 for its value. (Contributed by Scott Fenton, 17-Apr-2014.)
⊢ FullFun𝐹 = (Funpart𝐹 ∪ ((V ∖ dom Funpart𝐹) × {∅}))
Definition	df-ub 35857	Define the upper bound relationship functor. See brub 35935 for value. (Contributed by Scott Fenton, 3-May-2018.)
⊢ UB𝑅 = ((V × V) ∖ ((V ∖ 𝑅) ∘ ◡ E ))
Definition	df-lb 35858	Define the lower bound relationship functor. See brlb 35936 for value. (Contributed by Scott Fenton, 3-May-2018.)
⊢ LB𝑅 = UB◡𝑅
Theorem	txpss3v 35859	A tail Cartesian product is a subset of the class of ordered triples. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ (𝐴 ⊗ 𝐵) ⊆ (V × (V × V))
Theorem	txprel 35860	A tail Cartesian product is a relationship. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ Rel (𝐴 ⊗ 𝐵)
Theorem	brtxp 35861	Characterize a ternary relation over a tail Cartesian product. Together with txpss3v 35859, this completely defines membership in a tail cross. (Contributed by Scott Fenton, 31-Mar-2012.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ 𝑋 ∈ V    &   ⊢ 𝑌 ∈ V    &   ⊢ 𝑍 ∈ V    ⇒   ⊢ (𝑋(𝐴 ⊗ 𝐵)⟨𝑌, 𝑍⟩ ↔ (𝑋𝐴𝑌 ∧ 𝑋𝐵𝑍))
Theorem	brtxp2 35862*	The binary relation over a tail cross when the second argument is not an ordered pair. (Contributed by Scott Fenton, 14-Apr-2014.) (Revised by Mario Carneiro, 3-May-2015.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴(𝑅 ⊗ 𝑆)𝐵 ↔ ∃𝑥∃𝑦(𝐵 = ⟨𝑥, 𝑦⟩ ∧ 𝐴𝑅𝑥 ∧ 𝐴𝑆𝑦))
Theorem	dfpprod2 35863	Expanded definition of parallel product. (Contributed by Scott Fenton, 3-May-2014.)
⊢ pprod(𝐴, 𝐵) = ((◡(1st ↾ (V × V)) ∘ (𝐴 ∘ (1st ↾ (V × V)))) ∩ (◡(2nd ↾ (V × V)) ∘ (𝐵 ∘ (2nd ↾ (V × V)))))
Theorem	pprodcnveq 35864	A converse law for parallel product. (Contributed by Scott Fenton, 3-May-2014.)
⊢ pprod(𝑅, 𝑆) = ◡pprod(◡𝑅, ◡𝑆)
Theorem	pprodss4v 35865	The parallel product is a subclass of ((V × V) × (V × V)). (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ pprod(𝐴, 𝐵) ⊆ ((V × V) × (V × V))
Theorem	brpprod 35866	Characterize a quaternary relation over a tail Cartesian product. Together with pprodss4v 35865, this completely defines membership in a parallel product. (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝑋 ∈ V    &   ⊢ 𝑌 ∈ V    &   ⊢ 𝑍 ∈ V    &   ⊢ 𝑊 ∈ V    ⇒   ⊢ (⟨𝑋, 𝑌⟩pprod(𝐴, 𝐵)⟨𝑍, 𝑊⟩ ↔ (𝑋𝐴𝑍 ∧ 𝑌𝐵𝑊))
Theorem	brpprod3a 35867*	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.)
⊢ 𝑋 ∈ V    &   ⊢ 𝑌 ∈ V    &   ⊢ 𝑍 ∈ V    ⇒   ⊢ (⟨𝑋, 𝑌⟩pprod(𝑅, 𝑆)𝑍 ↔ ∃𝑧∃𝑤(𝑍 = ⟨𝑧, 𝑤⟩ ∧ 𝑋𝑅𝑧 ∧ 𝑌𝑆𝑤))
Theorem	brpprod3b 35868*	Condition for parallel product when the first argument is not an ordered pair. (Contributed by Scott Fenton, 3-May-2014.)
⊢ 𝑋 ∈ V    &   ⊢ 𝑌 ∈ V    &   ⊢ 𝑍 ∈ V    ⇒   ⊢ (𝑋pprod(𝑅, 𝑆)⟨𝑌, 𝑍⟩ ↔ ∃𝑧∃𝑤(𝑋 = ⟨𝑧, 𝑤⟩ ∧ 𝑧𝑅𝑌 ∧ 𝑤𝑆𝑍))
Theorem	relsset 35869	The subset class is a binary relation. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ Rel SSet
Theorem	brsset 35870	For sets, the SSet binary relation is equivalent to the subset relationship. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 SSet 𝐵 ↔ 𝐴 ⊆ 𝐵)
Theorem	idsset 35871	I is equal to the intersection of SSet and its converse. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ I = ( SSet ∩ ◡ SSet )
Theorem	eltrans 35872	Membership in the class of all transitive sets. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ Trans ↔ Tr 𝐴)
Theorem	dfon3 35873	A quantifier-free definition of On. (Contributed by Scott Fenton, 5-Apr-2012.)
⊢ On = (V ∖ ran (( SSet ∩ ( Trans × V)) ∖ ( I ∪ E )))
Theorem	dfon4 35874	Another quantifier-free definition of On. (Contributed by Scott Fenton, 4-May-2014.)
⊢ On = (V ∖ (( SSet ∖ ( I ∪ E )) “ Trans ))
Theorem	brtxpsd 35875*	Expansion of a common form used in quantifier-free definitions. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (¬ 𝐴ran ((V ⊗ E ) △ (𝑅 ⊗ V))𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥𝑅𝐴))
Theorem	brtxpsd2 35876*	Another common abbreviation for quantifier-free definitions. (Contributed by Scott Fenton, 21-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝑅 = (𝐶 ∖ ran ((V ⊗ E ) △ (𝑆 ⊗ V)))    &   ⊢ 𝐴𝐶𝐵    ⇒   ⊢ (𝐴𝑅𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥𝑆𝐴))
Theorem	brtxpsd3 35877*	A third common abbreviation for quantifier-free definitions. (Contributed by Scott Fenton, 3-May-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝑅 = (𝐶 ∖ ran ((V ⊗ E ) △ (𝑆 ⊗ V)))    &   ⊢ 𝐴𝐶𝐵    &   ⊢ (𝑥 ∈ 𝑋 ↔ 𝑥𝑆𝐴)    ⇒   ⊢ (𝐴𝑅𝐵 ↔ 𝐵 = 𝑋)
Theorem	relbigcup 35878	The Bigcup relationship is a relationship. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ Rel Bigcup
Theorem	brbigcup 35879	Binary relation over Bigcup . (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 Bigcup 𝐵 ↔ ∪ 𝐴 = 𝐵)
Theorem	dfbigcup2 35880	Bigcup using maps-to notation. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ Bigcup = (𝑥 ∈ V ↦ ∪ 𝑥)
Theorem	fobigcup 35881	Bigcup maps the universe onto itself. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ Bigcup :V–onto→V
Theorem	fnbigcup 35882	Bigcup is a function over the universal class. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ Bigcup Fn V
Theorem	fvbigcup 35883	For sets, Bigcup yields union. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ( Bigcup ‘𝐴) = ∪ 𝐴
Theorem	elfix 35884	Membership in the fixpoints of a class. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ Fix 𝑅 ↔ 𝐴𝑅𝐴)
Theorem	elfix2 35885	Alternative membership in the fixpoint of a class. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ Rel 𝑅    ⇒   ⊢ (𝐴 ∈ Fix 𝑅 ↔ 𝐴𝑅𝐴)
Theorem	dffix2 35886	The fixpoints of a class in terms of its range. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ Fix 𝐴 = ran (𝐴 ∩ I )
Theorem	fixssdm 35887	The fixpoints of a class are a subset of its domain. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ Fix 𝐴 ⊆ dom 𝐴
Theorem	fixssrn 35888	The fixpoints of a class are a subset of its range. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ Fix 𝐴 ⊆ ran 𝐴
Theorem	fixcnv 35889	The fixpoints of a class are the same as those of its converse. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ Fix 𝐴 = Fix ◡𝐴
Theorem	fixun 35890	The fixpoint operator distributes over union. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ Fix (𝐴 ∪ 𝐵) = ( Fix 𝐴 ∪ Fix 𝐵)
Theorem	ellimits 35891	Membership in the class of all limit ordinals. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ Limits ↔ Lim 𝐴)
Theorem	limitssson 35892	The class of all limit ordinals is a subclass of the class of all ordinals. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ Limits ⊆ On
Theorem	dfom5b 35893	A quantifier-free definition of ω that does not depend on ax-inf 9675. (Note: label was changed from dfom5 9687 to dfom5b 35893 to prevent naming conflict. NM, 12-Feb-2013.) (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ ω = (On ∩ ∩ Limits )
Theorem	sscoid 35894	A condition for subset and composition with identity. (Contributed by Scott Fenton, 13-Apr-2018.)
⊢ (𝐴 ⊆ ( I ∘ 𝐵) ↔ (Rel 𝐴 ∧ 𝐴 ⊆ 𝐵))
Theorem	dffun10 35895	Another potential definition of functionality. Based on statements in http://people.math.gatech.edu/~belinfan/research/autoreas/otter/sum/fs/. (Contributed by Scott Fenton, 30-Aug-2017.)
⊢ (Fun 𝐹 ↔ 𝐹 ⊆ ( I ∘ (V ∖ ((V ∖ I ) ∘ 𝐹))))
Theorem	elfuns 35896	Membership in the class of all functions. (Contributed by Scott Fenton, 18-Feb-2013.)
⊢ 𝐹 ∈ V    ⇒   ⊢ (𝐹 ∈ Funs ↔ Fun 𝐹)
Theorem	elfunsg 35897	Closed form of elfuns 35896. (Contributed by Scott Fenton, 2-May-2014.)
⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ Funs ↔ Fun 𝐹))
Theorem	brsingle 35898	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 35899*	Membership in the class of all singletons. (Contributed by Scott Fenton, 19-Feb-2013.)
⊢ (𝐴 ∈ Singletons ↔ ∃𝑥 𝐴 = {𝑥})
Theorem	fnsingle 35900	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