P. 51 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 5001-5100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ssopab2 5001	Equivalence of ordered pair abstraction subclass and implication. (Contributed by NM, 27-Dec-1996.) (Revised by Mario Carneiro, 19-May-2013.)
|- ( A. x A. y ( ph -> ps ) -> { <. x , y >. | ph } C_ { <. x , y >. | ps } )
Theorem	ssopab2b 5002	Equivalence of ordered pair abstraction subclass and implication. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
|- ( { <. x , y >. | ph } C_ { <. x , y >. | ps } <-> A. x A. y ( ph -> ps ) )
Theorem	ssopab2i 5003	Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 5-Apr-1995.)
|- ( ph -> ps )   =>    |- { <. x , y >. | ph } C_ { <. x , y >. | ps }
Theorem	ssopab2dv 5004*	Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 19-Jan-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> { <. x , y >. | ps } C_ { <. x , y >. | ch } )
Theorem	eqopab2b 5005	Equivalence of ordered pair abstraction equality and biconditional. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( { <. x , y >. | ph } = { <. x , y >. | ps } <-> A. x A. y ( ph <-> ps ) )
Theorem	opabn0 5006	Nonempty ordered pair class abstraction. (Contributed by NM, 10-Oct-2007.)
|- ( { <. x , y >. | ph } =/= (/) <-> E. x E. y ph )
Theorem	opab0 5007	Empty ordered pair class abstraction. (Contributed by AV, 29-Oct-2021.)
|- ( { <. x , y >. | ph } = (/) <-> A. x A. y -. ph )
Theorem	csbopab 5008*	Move substitution into a class abstraction. Version of csbopabgALT 5009 without a sethood antecedent but depending on more axioms. (Contributed by NM, 6-Aug-2007.) (Revised by NM, 23-Aug-2018.)
|- [_ A / x ]_ { <. y , z >. | ph } = { <. y , z >. | [. A / x ]. ph }
Theorem	csbopabgALT 5009*	Move substitution into a class abstraction. Version of csbopab 5008 with a sethood antecedent but depending on fewer axioms. (Contributed by NM, 6-Aug-2007.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( A e. V -> [_ A / x ]_ { <. y , z >. | ph } = { <. y , z >. | [. A / x ]. ph } )
Theorem	csbmpt12 5010*	Move substitution into a maps-to notation. (Contributed by AV, 26-Sep-2019.)
|- ( A e. V -> [_ A / x ]_ ( y e. Y |-> Z ) = ( y e. [_ A / x ]_ Y |-> [_ A / x ]_ Z ) )
Theorem	csbmpt2 5011*	Move substitution into the second part of a maps-to notation. (Contributed by AV, 26-Sep-2019.)
|- ( A e. V -> [_ A / x ]_ ( y e. Y |-> Z ) = ( y e. Y |-> [_ A / x ]_ Z ) )
Theorem	iunopab 5012*	Move indexed union inside an ordered-pair abstraction. (Contributed by Stefan O'Rear, 20-Feb-2015.)
|- U_ z e. A { <. x , y >. | ph } = { <. x , y >. | E. z e. A ph }
Theorem	elopabr 5013*	Membership in a class abstraction of pairs, defined by a binary relation. (Contributed by AV, 16-Feb-2021.)
|- ( A e. { <. x , y >. | x R y } -> A e. R )
Theorem	elopabran 5014*	Membership in a class abstraction of pairs, defined by a restricted binary relation. (Contributed by AV, 16-Feb-2021.)
|- ( A e. { <. x , y >. | ( x R y /\ ps ) } -> A e. R )
Theorem	rbropapd 5015*	Properties of a pair in an extended binary relation. (Contributed by Alexander van der Vekens, 30-Oct-2017.)
|- ( ph -> M = { <. f , p >. | ( f W p /\ ps ) } )   &    |- ( ( f = F /\ p = P ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( ( F e. X /\ P e. Y ) -> ( F M P <-> ( F W P /\ ch ) ) ) )
Theorem	rbropap 5016*	Properties of a pair in a restricted binary relation M expressed as an ordered-pair class abstraction: M is the binary relation W restricted by the condition ps. (Contributed by AV, 31-Jan-2021.)
|- ( ph -> M = { <. f , p >. | ( f W p /\ ps ) } )   &    |- ( ( f = F /\ p = P ) -> ( ps <-> ch ) )   =>    |- ( ( ph /\ F e. X /\ P e. Y ) -> ( F M P <-> ( F W P /\ ch ) ) )
Theorem	2rbropap 5017*	Properties of a pair in a restricted binary relation M expressed as an ordered-pair class abstraction: M is the binary relation W restricted by the conditions ps and ta. (Contributed by AV, 31-Jan-2021.)
|- ( ph -> M = { <. f , p >. | ( f W p /\ ps /\ ta ) } )   &    |- ( ( f = F /\ p = P ) -> ( ps <-> ch ) )   &    |- ( ( f = F /\ p = P ) -> ( ta <-> th ) )   =>    |- ( ( ph /\ F e. X /\ P e. Y ) -> ( F M P <-> ( F W P /\ ch /\ th ) ) )
2.3.5  Power class of union and intersection
Theorem	pwin 5018	The power class of the intersection of two classes is the intersection of their power classes. Exercise 4.12(j) of [Mendelson] p. 235. (Contributed by NM, 23-Nov-2003.)
|- ~P ( A i^i B ) = ( ~P A i^i ~P B )
Theorem	pwunss 5019	The power class of the union of two classes includes the union of their power classes. Exercise 4.12(k) of [Mendelson] p. 235. (Contributed by NM, 23-Nov-2003.)
|- ( ~P A u. ~P B ) C_ ~P ( A u. B )
Theorem	pwssun 5020	The power class of the union of two classes is a subset of the union of their power classes, iff one class is a subclass of the other. Exercise 4.12(l) of [Mendelson] p. 235. (Contributed by NM, 23-Nov-2003.)
|- ( ( A C_ B \/ B C_ A ) <-> ~P ( A u. B ) C_ ( ~P A u. ~P B ) )
Theorem	pwundif 5021	Break up the power class of a union into a union of smaller classes. (Contributed by NM, 25-Mar-2007.) (Proof shortened by Thierry Arnoux, 20-Dec-2016.)
|- ~P ( A u. B ) = ( ( ~P ( A u. B ) \ ~P A ) u. ~P A )
Theorem	pwun 5022	The power class of the union of two classes equals the union of their power classes, iff one class is a subclass of the other. Part of Exercise 7(b) of [Enderton] p. 28. (Contributed by NM, 23-Nov-2003.)
|- ( ( A C_ B \/ B C_ A ) <-> ~P ( A u. B ) = ( ~P A u. ~P B ) )
2.3.6  The identity relation
Syntax	cid 5023	Extend the definition of a class to include the identity relation.
class _I
Definition	df-id 5024*	Define the identity relation. Definition 9.15 of [Quine] p. 64. For example, 5 _I 5 and -. 4 _I 5 (ex-id 27291). (Contributed by NM, 13-Aug-1995.)
|- _I = { <. x , y >. | x = y }
Theorem	dfid3 5025	A stronger version of df-id 5024 that doesn't require x and y to be distinct. Ordinarily, we wouldn't use this as a definition, since non-distinct dummy variables would make soundness verification more difficult (as the proof here shows). The proof can be instructive in showing how distinct variable requirements may be eliminated, a task that is not necessarily obvious. (Contributed by NM, 5-Feb-2008.) (Revised by Mario Carneiro, 18-Nov-2016.)
|- _I = { <. x , y >. | x = y }
Theorem	dfid4 5026	The identity function using maps-to notation. (Contributed by Scott Fenton, 15-Dec-2017.)
|- _I = ( x e. _V |-> x )
Theorem	dfid2 5027	Alternate definition of the identity relation. (Contributed by NM, 15-Mar-2007.)
|- _I = { <. x , x >. | x = x }
2.3.7  The membership (or epsilon) relation
Syntax	cep 5028	Extend class notation to include the membership/epsilon relation.
class _E
Definition	df-eprel 5029*	Define the membership relation, or epsilon relation. Similar to Definition 6.22 of [TakeutiZaring] p. 30. The epsilon relation and set membership are the same, that is, ( A _E B <-> A e. B ) when B is a set by epelg 5030. Thus, 5 _E { 1 , 5 } (ex-eprel 27290). (Contributed by NM, 13-Aug-1995.)
|- _E = { <. x , y >. | x e. y }
Theorem	epelg 5030	The epsilon relation and membership are the same. General version of epel 5032. (Contributed by Scott Fenton, 27-Mar-2011.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( B e. V -> ( A _E B <-> A e. B ) )
Theorem	epelc 5031	The epsilon relationship and the membership relation are the same. (Contributed by Scott Fenton, 11-Apr-2012.)
|- B e. _V   =>    |- ( A _E B <-> A e. B )
Theorem	epel 5032	The epsilon relation and the membership relation are the same. (Contributed by NM, 13-Aug-1995.)
|- ( x _E y <-> x e. y )
2.3.8  Partial and complete ordering
Syntax	wpo 5033	Extend wff notation to include the strict partial ordering predicate. Read: ' R is a partial order on A.'
wff R Po A
Syntax	wor 5034	Extend wff notation to include the strict complete ordering predicate. Read: ' R orders A.'
wff R Or A
Definition	df-po 5035*	Define the strict partial order predicate. Definition of [Enderton] p. 168. The expression R Po A means R is a partial order on A. For example, < Po RR is true, while <_ Po RR is false (ex-po 27292). (Contributed by NM, 16-Mar-1997.)
|- ( R Po A <-> A. x e. A A. y e. A A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) )
Definition	df-so 5036*	Define the strict complete (linear) order predicate. The expression R Or A is true if relationship R orders A. For example, < Or RR is true (ltso 10118). Equivalent to Definition 6.19(1) of [TakeutiZaring] p. 29. (Contributed by NM, 21-Jan-1996.)
|- ( R Or A <-> ( R Po A /\ A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) ) )
Theorem	poss 5037	Subset theorem for the partial ordering predicate. (Contributed by NM, 27-Mar-1997.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
|- ( A C_ B -> ( R Po B -> R Po A ) )
Theorem	poeq1 5038	Equality theorem for partial ordering predicate. (Contributed by NM, 27-Mar-1997.)
|- ( R = S -> ( R Po A <-> S Po A ) )
Theorem	poeq2 5039	Equality theorem for partial ordering predicate. (Contributed by NM, 27-Mar-1997.)
|- ( A = B -> ( R Po A <-> R Po B ) )
Theorem	nfpo 5040	Bound-variable hypothesis builder for partial orders. (Contributed by Stefan O'Rear, 20-Jan-2015.)
|- F/_ x R   &    |- F/_ x A   =>    |- F/ x R Po A
Theorem	nfso 5041	Bound-variable hypothesis builder for total orders. (Contributed by Stefan O'Rear, 20-Jan-2015.)
|- F/_ x R   &    |- F/_ x A   =>    |- F/ x R Or A
Theorem	pocl 5042	Properties of partial order relation in class notation. (Contributed by NM, 27-Mar-1997.)
|- ( R Po A -> ( ( B e. A /\ C e. A /\ D e. A ) -> ( -. B R B /\ ( ( B R C /\ C R D ) -> B R D ) ) ) )
Theorem	ispod 5043*	Sufficient conditions for a partial order. (Contributed by NM, 9-Jul-2014.)
|- ( ( ph /\ x e. A ) -> -. x R x )   &    |- ( ( ph /\ ( x e. A /\ y e. A /\ z e. A ) ) -> ( ( x R y /\ y R z ) -> x R z ) )   =>    |- ( ph -> R Po A )
Theorem	swopolem 5044*	Perform the substitutions into the strict weak ordering law. (Contributed by Mario Carneiro, 31-Dec-2014.)
|- ( ( ph /\ ( x e. A /\ y e. A /\ z e. A ) ) -> ( x R y -> ( x R z \/ z R y ) ) )   =>    |- ( ( ph /\ ( X e. A /\ Y e. A /\ Z e. A ) ) -> ( X R Y -> ( X R Z \/ Z R Y ) ) )
Theorem	swopo 5045*	A strict weak order is a partial order. (Contributed by Mario Carneiro, 9-Jul-2014.)
|- ( ( ph /\ ( y e. A /\ z e. A ) ) -> ( y R z -> -. z R y ) )   &    |- ( ( ph /\ ( x e. A /\ y e. A /\ z e. A ) ) -> ( x R y -> ( x R z \/ z R y ) ) )   =>    |- ( ph -> R Po A )
Theorem	poirr 5046	A partial order relation is irreflexive. (Contributed by NM, 27-Mar-1997.)
|- ( ( R Po A /\ B e. A ) -> -. B R B )
Theorem	potr 5047	A partial order relation is a transitive relation. (Contributed by NM, 27-Mar-1997.)
|- ( ( R Po A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( ( B R C /\ C R D ) -> B R D ) )
Theorem	po2nr 5048	A partial order relation has no 2-cycle loops. (Contributed by NM, 27-Mar-1997.)
|- ( ( R Po A /\ ( B e. A /\ C e. A ) ) -> -. ( B R C /\ C R B ) )
Theorem	po3nr 5049	A partial order relation has no 3-cycle loops. (Contributed by NM, 27-Mar-1997.)
|- ( ( R Po A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> -. ( B R C /\ C R D /\ D R B ) )
Theorem	po0 5050	Any relation is a partial ordering of the empty set. (Contributed by NM, 28-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|- R Po (/)
Theorem	pofun 5051*	A function preserves a partial order relation. (Contributed by Jeff Madsen, 18-Jun-2011.)
|- S = { <. x , y >. | X R Y }   &    |- ( x = y -> X = Y )   =>    |- ( ( R Po B /\ A. x e. A X e. B ) -> S Po A )
Theorem	sopo 5052	A strict linear order is a strict partial order. (Contributed by NM, 28-Mar-1997.)
|- ( R Or A -> R Po A )
Theorem	soss 5053	Subset theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|- ( A C_ B -> ( R Or B -> R Or A ) )
Theorem	soeq1 5054	Equality theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.)
|- ( R = S -> ( R Or A <-> S Or A ) )
Theorem	soeq2 5055	Equality theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.)
|- ( A = B -> ( R Or A <-> R Or B ) )
Theorem	sonr 5056	A strict order relation is irreflexive. (Contributed by NM, 24-Nov-1995.)
|- ( ( R Or A /\ B e. A ) -> -. B R B )
Theorem	sotr 5057	A strict order relation is a transitive relation. (Contributed by NM, 21-Jan-1996.)
|- ( ( R Or A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( ( B R C /\ C R D ) -> B R D ) )
Theorem	solin 5058	A strict order relation is linear (satisfies trichotomy). (Contributed by NM, 21-Jan-1996.)
|- ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( B R C \/ B = C \/ C R B ) )
Theorem	so2nr 5059	A strict order relation has no 2-cycle loops. (Contributed by NM, 21-Jan-1996.)
|- ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> -. ( B R C /\ C R B ) )
Theorem	so3nr 5060	A strict order relation has no 3-cycle loops. (Contributed by NM, 21-Jan-1996.)
|- ( ( R Or A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> -. ( B R C /\ C R D /\ D R B ) )
Theorem	sotric 5061	A strict order relation satisfies strict trichotomy. (Contributed by NM, 19-Feb-1996.)
|- ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( B R C <-> -. ( B = C \/ C R B ) ) )
Theorem	sotrieq 5062	Trichotomy law for strict order relation. (Contributed by NM, 9-Apr-1996.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|- ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( B = C <-> -. ( B R C \/ C R B ) ) )
Theorem	sotrieq2 5063	Trichotomy law for strict order relation. (Contributed by NM, 5-May-1999.)
|- ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( B = C <-> ( -. B R C /\ -. C R B ) ) )
Theorem	sotr2 5064	A transitivity relation. (Read B <_ C and C < D implies B < D.) (Contributed by Mario Carneiro, 10-May-2013.)
|- ( ( R Or A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( ( -. C R B /\ C R D ) -> B R D ) )
Theorem	issod 5065*	An irreflexive, transitive, linear relation is a strict ordering. (Contributed by NM, 21-Jan-1996.) (Revised by Mario Carneiro, 9-Jul-2014.)
|- ( ph -> R Po A )   &    |- ( ( ph /\ ( x e. A /\ y e. A ) ) -> ( x R y \/ x = y \/ y R x ) )   =>    |- ( ph -> R Or A )
Theorem	issoi 5066*	An irreflexive, transitive, linear relation is a strict ordering. (Contributed by NM, 21-Jan-1996.) (Revised by Mario Carneiro, 9-Jul-2014.)
|- ( x e. A -> -. x R x )   &    |- ( ( x e. A /\ y e. A /\ z e. A ) -> ( ( x R y /\ y R z ) -> x R z ) )   &    |- ( ( x e. A /\ y e. A ) -> ( x R y \/ x = y \/ y R x ) )   =>    |- R Or A
Theorem	isso2i 5067*	Deduce strict ordering from its properties. (Contributed by NM, 29-Jan-1996.) (Revised by Mario Carneiro, 9-Jul-2014.)
|- ( ( x e. A /\ y e. A ) -> ( x R y <-> -. ( x = y \/ y R x ) ) )   &    |- ( ( x e. A /\ y e. A /\ z e. A ) -> ( ( x R y /\ y R z ) -> x R z ) )   =>    |- R Or A
Theorem	so0 5068	Any relation is a strict ordering of the empty set. (Contributed by NM, 16-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|- R Or (/)
Theorem	somo 5069*	A totally ordered set has at most one minimal element. (Contributed by Mario Carneiro, 24-Jun-2015.) (Revised by NM, 16-Jun-2017.)
|- ( R Or A -> E* x e. A A. y e. A -. y R x )
2.3.9  Founded and well-ordering relations
Syntax	wfr 5070	Extend wff notation to include the well-founded predicate. Read: ' R is a well-founded relation on A.'
wff R Fr A
Syntax	wse 5071	Extend wff notation to include the set-like predicate. Read: ' R is set-like on A.'
wff R Se A
Syntax	wwe 5072	Extend wff notation to include the well-ordering predicate. Read: ' R well-orders A.'
wff R We A
Definition	df-fr 5073*	Define the well-founded relation predicate. Definition 6.24(1) of [TakeutiZaring] p. 30. For alternate definitions, see dffr2 5079 and dffr3 5498. (Contributed by NM, 3-Apr-1994.)
|- ( R Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x A. z e. x -. z R y ) )
Definition	df-se 5074*	Define the set-like predicate. (Contributed by Mario Carneiro, 19-Nov-2014.)
|- ( R Se A <-> A. x e. A { y e. A | y R x } e. _V )
Definition	df-we 5075	Define the well-ordering predicate. For an alternate definition, see dfwe2 6981. (Contributed by NM, 3-Apr-1994.)
|- ( R We A <-> ( R Fr A /\ R Or A ) )
Theorem	fri 5076*	Property of well-founded relation (one direction of definition). (Contributed by NM, 18-Mar-1997.)
|- ( ( ( B e. C /\ R Fr A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E. x e. B A. y e. B -. y R x )
Theorem	seex 5077*	The R-preimage of an element of the base set in a set-like relation is a set. (Contributed by Mario Carneiro, 19-Nov-2014.)
|- ( ( R Se A /\ B e. A ) -> { x e. A | x R B } e. _V )
Theorem	exse 5078	Any relation on a set is set-like on it. (Contributed by Mario Carneiro, 22-Jun-2015.)
|- ( A e. V -> R Se A )
Theorem	dffr2 5079*	Alternate definition of well-founded relation. Similar to Definition 6.21 of [TakeutiZaring] p. 30. (Contributed by NM, 17-Feb-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Proof shortened by Mario Carneiro, 23-Jun-2015.)
|- ( R Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x { z e. x | z R y } = (/) ) )
Theorem	frc 5080*	Property of well-founded relation (one direction of definition using class variables). (Contributed by NM, 17-Feb-2004.) (Revised by Mario Carneiro, 19-Nov-2014.)
|- B e. _V   =>    |- ( ( R Fr A /\ B C_ A /\ B =/= (/) ) -> E. x e. B { y e. B | y R x } = (/) )
Theorem	frss 5081	Subset theorem for the well-founded predicate. Exercise 1 of [TakeutiZaring] p. 31. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|- ( A C_ B -> ( R Fr B -> R Fr A ) )
Theorem	sess1 5082	Subset theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
|- ( R C_ S -> ( S Se A -> R Se A ) )
Theorem	sess2 5083	Subset theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
|- ( A C_ B -> ( R Se B -> R Se A ) )
Theorem	freq1 5084	Equality theorem for the well-founded predicate. (Contributed by NM, 9-Mar-1997.)
|- ( R = S -> ( R Fr A <-> S Fr A ) )
Theorem	freq2 5085	Equality theorem for the well-founded predicate. (Contributed by NM, 3-Apr-1994.)
|- ( A = B -> ( R Fr A <-> R Fr B ) )
Theorem	seeq1 5086	Equality theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
|- ( R = S -> ( R Se A <-> S Se A ) )
Theorem	seeq2 5087	Equality theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
|- ( A = B -> ( R Se A <-> R Se B ) )
Theorem	nffr 5088	Bound-variable hypothesis builder for well-founded relations. (Contributed by Stefan O'Rear, 20-Jan-2015.) (Revised by Mario Carneiro, 14-Oct-2016.)
|- F/_ x R   &    |- F/_ x A   =>    |- F/ x R Fr A
Theorem	nfse 5089	Bound-variable hypothesis builder for set-like relations. (Contributed by Mario Carneiro, 24-Jun-2015.) (Revised by Mario Carneiro, 14-Oct-2016.)
|- F/_ x R   &    |- F/_ x A   =>    |- F/ x R Se A
Theorem	nfwe 5090	Bound-variable hypothesis builder for well-orderings. (Contributed by Stefan O'Rear, 20-Jan-2015.) (Revised by Mario Carneiro, 14-Oct-2016.)
|- F/_ x R   &    |- F/_ x A   =>    |- F/ x R We A
Theorem	frirr 5091	A well-founded relation is irreflexive. Special case of Proposition 6.23 of [TakeutiZaring] p. 30. (Contributed by NM, 2-Jan-1994.) (Revised by Mario Carneiro, 22-Jun-2015.)
|- ( ( R Fr A /\ B e. A ) -> -. B R B )
Theorem	fr2nr 5092	A well-founded relation has no 2-cycle loops. Special case of Proposition 6.23 of [TakeutiZaring] p. 30. (Contributed by NM, 30-May-1994.) (Revised by Mario Carneiro, 22-Jun-2015.)
|- ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> -. ( B R C /\ C R B ) )
Theorem	fr0 5093	Any relation is well-founded on the empty set. (Contributed by NM, 17-Sep-1993.)
|- R Fr (/)
Theorem	frminex 5094*	If an element of a well-founded set satisfies a property ph, then there is a minimal element that satisfies ph. (Contributed by Jeff Madsen, 18-Jun-2010.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
|- A e. _V   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( R Fr A -> ( E. x e. A ph -> E. x e. A ( ph /\ A. y e. A ( ps -> -. y R x ) ) ) )
Theorem	efrirr 5095	Irreflexivity of the epsilon relation: a class founded by epsilon is not a member of itself. (Contributed by NM, 18-Apr-1994.) (Revised by Mario Carneiro, 22-Jun-2015.)
|- ( _E Fr A -> -. A e. A )
Theorem	efrn2lp 5096	A set founded by epsilon contains no 2-cycle loops. (Contributed by NM, 19-Apr-1994.)
|- ( ( _E Fr A /\ ( B e. A /\ C e. A ) ) -> -. ( B e. C /\ C e. B ) )
Theorem	epse 5097	The epsilon relation is set-like on any class. (This is the origin of the term "set-like": a set-like relation "acts like" the epsilon relation of sets and their elements.) (Contributed by Mario Carneiro, 22-Jun-2015.)
|- _E Se A
Theorem	tz7.2 5098	Similar to Theorem 7.2 of [TakeutiZaring] p. 35, of except that the Axiom of Regularity is not required due to antecedent _E Fr A. (Contributed by NM, 4-May-1994.)
|- ( ( Tr A /\ _E Fr A /\ B e. A ) -> ( B C_ A /\ B =/= A ) )
Theorem	dfepfr 5099*	An alternate way of saying that the epsilon relation is well-founded. (Contributed by NM, 17-Feb-2004.) (Revised by Mario Carneiro, 23-Jun-2015.)
|- ( _E Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x ( x i^i y ) = (/) ) )
Theorem	epfrc 5100*	A subset of an epsilon-founded class has a minimal element. (Contributed by NM, 17-Feb-2004.) (Revised by David Abernethy, 22-Feb-2011.)
|- B e. _V   =>    |- ( ( _E Fr A /\ B C_ A /\ B =/= (/) ) -> E. x e. B ( B i^i x ) = (/) )