P. 44 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 4301-4400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	opabidw 4301*	The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. Version of opabid 4300 with a disjoint variable condition. (Contributed by NM, 14-Apr-1995.) (Revised by GG, 26-Jan-2024.)
|- ( <. x , y >. e. { <. x , y >. | ph } <-> ph )
Theorem	elopab 4302*	Membership in a class abstraction of ordered pairs. (Contributed by NM, 24-Mar-1998.)
|- ( A e. { <. x , y >. | ph } <-> E. x E. y ( A = <. x , y >. /\ ph ) )
Theorem	opelopabsbALT 4303*	The law of concretion in terms of substitutions. Less general than opelopabsb 4304, but having a much shorter proof. (Contributed by NM, 30-Sep-2002.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( <. z , w >. e. { <. x , y >. | ph } <-> [ w / y ] [ z / x ] ph )
Theorem	opelopabsb 4304*	The law of concretion in terms of substitutions. (Contributed by NM, 30-Sep-2002.) (Revised by Mario Carneiro, 18-Nov-2016.)
|- ( <. A , B >. e. { <. x , y >. | ph } <-> [. A / x ]. [. B / y ]. ph )
Theorem	brabsb 4305*	The law of concretion in terms of substitutions. (Contributed by NM, 17-Mar-2008.)
|- R = { <. x , y >. | ph }   =>    |- ( A R B <-> [. A / x ]. [. B / y ]. ph )
Theorem	opelopabt 4306*	Closed theorem form of opelopab 4316. (Contributed by NM, 19-Feb-2013.)
|- ( ( A. x A. y ( x = A -> ( ph <-> ps ) ) /\ A. x A. y ( y = B -> ( ps <-> ch ) ) /\ ( A e. V /\ B e. W ) ) -> ( <. A , B >. e. { <. x , y >. | ph } <-> ch ) )
Theorem	opelopabga 4307*	The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 19-Dec-2013.)
|- ( ( x = A /\ y = B ) -> ( ph <-> ps ) )   =>    |- ( ( A e. V /\ B e. W ) -> ( <. A , B >. e. { <. x , y >. | ph } <-> ps ) )
Theorem	brabga 4308*	The law of concretion for a binary relation. (Contributed by Mario Carneiro, 19-Dec-2013.)
|- ( ( x = A /\ y = B ) -> ( ph <-> ps ) )   &    |- R = { <. x , y >. | ph }   =>    |- ( ( A e. V /\ B e. W ) -> ( A R B <-> ps ) )
Theorem	opelopab2a 4309*	Ordered pair membership in an ordered pair class abstraction. (Contributed by Mario Carneiro, 19-Dec-2013.)
|- ( ( x = A /\ y = B ) -> ( ph <-> ps ) )   =>    |- ( ( A e. C /\ B e. D ) -> ( <. A , B >. e. { <. x , y >. | ( ( x e. C /\ y e. D ) /\ ph ) } <-> ps ) )
Theorem	opelopaba 4310*	The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 19-Dec-2013.)
|- A e. _V   &    |- B e. _V   &    |- ( ( x = A /\ y = B ) -> ( ph <-> ps ) )   =>    |- ( <. A , B >. e. { <. x , y >. | ph } <-> ps )
Theorem	braba 4311*	The law of concretion for a binary relation. (Contributed by NM, 19-Dec-2013.)
|- A e. _V   &    |- B e. _V   &    |- ( ( x = A /\ y = B ) -> ( ph <-> ps ) )   &    |- R = { <. x , y >. | ph }   =>    |- ( A R B <-> ps )
Theorem	opelopabg 4312*	The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro, 19-Dec-2013.)
|- ( x = A -> ( ph <-> ps ) )   &    |- ( y = B -> ( ps <-> ch ) )   =>    |- ( ( A e. V /\ B e. W ) -> ( <. A , B >. e. { <. x , y >. | ph } <-> ch ) )
Theorem	brabg 4313*	The law of concretion for a binary relation. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 19-Dec-2013.)
|- ( x = A -> ( ph <-> ps ) )   &    |- ( y = B -> ( ps <-> ch ) )   &    |- R = { <. x , y >. | ph }   =>    |- ( ( A e. C /\ B e. D ) -> ( A R B <-> ch ) )
Theorem	opelopabgf 4314*	The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopabg 4312 uses bound-variable hypotheses in place of distinct variable conditions. (Contributed by Alexander van der Vekens, 8-Jul-2018.)
|- F/ x ps   &    |- F/ y ch   &    |- ( x = A -> ( ph <-> ps ) )   &    |- ( y = B -> ( ps <-> ch ) )   =>    |- ( ( A e. V /\ B e. W ) -> ( <. A , B >. e. { <. x , y >. | ph } <-> ch ) )
Theorem	opelopab2 4315*	Ordered pair membership in an ordered pair class abstraction. (Contributed by NM, 14-Oct-2007.) (Revised by Mario Carneiro, 19-Dec-2013.)
|- ( x = A -> ( ph <-> ps ) )   &    |- ( y = B -> ( ps <-> ch ) )   =>    |- ( ( A e. C /\ B e. D ) -> ( <. A , B >. e. { <. x , y >. | ( ( x e. C /\ y e. D ) /\ ph ) } <-> ch ) )
Theorem	opelopab 4316*	The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by NM, 16-May-1995.)
|- A e. _V   &    |- B e. _V   &    |- ( x = A -> ( ph <-> ps ) )   &    |- ( y = B -> ( ps <-> ch ) )   =>    |- ( <. A , B >. e. { <. x , y >. | ph } <-> ch )
Theorem	brab 4317*	The law of concretion for a binary relation. (Contributed by NM, 16-Aug-1999.)
|- A e. _V   &    |- B e. _V   &    |- ( x = A -> ( ph <-> ps ) )   &    |- ( y = B -> ( ps <-> ch ) )   &    |- R = { <. x , y >. | ph }   =>    |- ( A R B <-> ch )
Theorem	opelopabaf 4318*	The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopab 4316 uses bound-variable hypotheses in place of distinct variable conditions. (Contributed by Mario Carneiro, 19-Dec-2013.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
|- F/ x ps   &    |- F/ y ps   &    |- A e. _V   &    |- B e. _V   &    |- ( ( x = A /\ y = B ) -> ( ph <-> ps ) )   =>    |- ( <. A , B >. e. { <. x , y >. | ph } <-> ps )
Theorem	opelopabf 4319*	The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopab 4316 uses bound-variable hypotheses in place of distinct variable conditions. (Contributed by NM, 19-Dec-2008.)
|- F/ x ps   &    |- F/ y ch   &    |- A e. _V   &    |- B e. _V   &    |- ( x = A -> ( ph <-> ps ) )   &    |- ( y = B -> ( ps <-> ch ) )   =>    |- ( <. A , B >. e. { <. x , y >. | ph } <-> ch )
Theorem	ssopab2 4320	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 4321	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 4322	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 4323*	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 4324	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	opabm 4325*	Inhabited ordered pair class abstraction. (Contributed by Jim Kingdon, 29-Sep-2018.)
|- ( E. z z e. { <. x , y >. | ph } <-> E. x E. y ph )
Theorem	iunopab 4326*	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 }
2.3.6  Power class of union and intersection
Theorem	pwin 4327	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 4328	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	pwssunim 4329	The power class of the union of two classes is a subset of the union of their power classes, if one class is a subclass of the other. One direction of Exercise 4.12(l) of [Mendelson] p. 235. (Contributed by Jim Kingdon, 30-Sep-2018.)
|- ( ( A C_ B \/ B C_ A ) -> ~P ( A u. B ) C_ ( ~P A u. ~P B ) )
Theorem	pwundifss 4330	Break up the power class of a union into a union of smaller classes. (Contributed by Jim Kingdon, 30-Sep-2018.)
|- ( ( ~P ( A u. B ) \ ~P A ) u. ~P A ) C_ ~P ( A u. B )
Theorem	pwunim 4331	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 Jim Kingdon, 30-Sep-2018.)
|- ( ( A C_ B \/ B C_ A ) -> ~P ( A u. B ) = ( ~P A u. ~P B ) )
2.3.7  Epsilon and identity relations
Syntax	cep 4332	Extend class notation to include the epsilon relation.
class _E
Syntax	cid 4333	Extend the definition of a class to include identity relation.
class _I
Definition	df-eprel 4334*	Define the 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 4335. Thus, 5 _E { 1 , 5 }. (Contributed by NM, 13-Aug-1995.)
|- _E = { <. x , y >. | x e. y }
Theorem	epelg 4335	The epsilon relation and membership are the same. General version of epel 4337. (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 4336	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 4337	The epsilon relation and the membership relation are the same. (Contributed by NM, 13-Aug-1995.)
|- ( x _E y <-> x e. y )
Definition	df-id 4338*	Define the identity relation. Definition 9.15 of [Quine] p. 64. For example, 5 _I 5 and -. 4 _I 5. (Contributed by NM, 13-Aug-1995.)
|- _I = { <. x , y >. | x = y }
2.3.8  Partial and total orderings We have not yet defined relations (df-rel 4680), but here we introduce a few related notions we will use to develop ordinals. The class variable R is no different from other class variables, but it reminds us that typically it represents what we will later call a "relation".
Syntax	wpo 4339	Extend wff notation to include the strict partial ordering predicate. Read: ' R is a partial order on A.'
wff R Po A
Syntax	wor 4340	Extend wff notation to include the strict linear ordering predicate. Read: ' R orders A.'
wff R Or A
Definition	df-po 4341*	Define the strict partial order predicate. Definition of [Enderton] p. 168. The expression R Po A means R is a partial order on A. (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-iso 4342*	Define the strict linear order predicate. The expression R Or A is true if relationship R orders A. The property x R y -> ( x R z \/ z R y ) is called weak linearity by Proposition 11.2.3 of [HoTT], p. (varies). If we assumed excluded middle, it would be equivalent to trichotomy, x R y \/ x = y \/ y R x. (Contributed by NM, 21-Jan-1996.) (Revised by Jim Kingdon, 4-Oct-2018.)
|- ( R Or A <-> ( R Po A /\ A. x e. A A. y e. A A. z e. A ( x R y -> ( x R z \/ z R y ) ) ) )
Theorem	poss 4343	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 4344	Equality theorem for partial ordering predicate. (Contributed by NM, 27-Mar-1997.)
|- ( R = S -> ( R Po A <-> S Po A ) )
Theorem	poeq2 4345	Equality theorem for partial ordering predicate. (Contributed by NM, 27-Mar-1997.)
|- ( A = B -> ( R Po A <-> R Po B ) )
Theorem	nfpo 4346	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 4347	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 4348	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 4349*	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 4350*	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 4351*	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 4352	A partial order relation is irreflexive. (Contributed by NM, 27-Mar-1997.)
|- ( ( R Po A /\ B e. A ) -> -. B R B )
Theorem	potr 4353	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 4354	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 4355	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 4356	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 4357*	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 4358	A strict linear order is a strict partial order. (Contributed by NM, 28-Mar-1997.)
|- ( R Or A -> R Po A )
Theorem	soss 4359	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 4360	Equality theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.)
|- ( R = S -> ( R Or A <-> S Or A ) )
Theorem	soeq2 4361	Equality theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.)
|- ( A = B -> ( R Or A <-> R Or B ) )
Theorem	sonr 4362	A strict order relation is irreflexive. (Contributed by NM, 24-Nov-1995.)
|- ( ( R Or A /\ B e. A ) -> -. B R B )
Theorem	sotr 4363	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	issod 4364*	An irreflexive, transitive, trichotomous relation is a linear ordering (in the sense of df-iso 4342). (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	sowlin 4365	A strict order relation satisfies weak linearity. (Contributed by Jim Kingdon, 6-Oct-2018.)
|- ( ( R Or A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( B R C -> ( B R D \/ D R C ) ) )
Theorem	so2nr 4366	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 4367	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	sotricim 4368	One direction of sotritric 4369 holds for all weakly linear orders. (Contributed by Jim Kingdon, 28-Sep-2019.)
|- ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( B R C -> -. ( B = C \/ C R B ) ) )
Theorem	sotritric 4369	A trichotomy relationship, given a trichotomous order. (Contributed by Jim Kingdon, 28-Sep-2019.)
|- R Or A   &    |- ( ( B e. A /\ C e. A ) -> ( B R C \/ B = C \/ C R B ) )   =>    |- ( ( B e. A /\ C e. A ) -> ( B R C <-> -. ( B = C \/ C R B ) ) )
Theorem	sotritrieq 4370	A trichotomy relationship, given a trichotomous order. (Contributed by Jim Kingdon, 13-Dec-2019.)
|- R Or A   &    |- ( ( B e. A /\ C e. A ) -> ( B R C \/ B = C \/ C R B ) )   =>    |- ( ( B e. A /\ C e. A ) -> ( B = C <-> -. ( B R C \/ C R B ) ) )
Theorem	so0 4371	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 (/)
2.3.9  Founded and set-like relations
Syntax	wfrfor 4372	Extend wff notation to include the well-founded predicate.
wff FrFor R A S
Syntax	wfr 4373	Extend wff notation to include the well-founded predicate. Read: ' R is a well-founded relation on A.'
wff R Fr A
Syntax	wse 4374	Extend wff notation to include the set-like predicate. Read: ' R is set-like on A.'
wff R Se A
Syntax	wwe 4375	Extend wff notation to include the well-ordering predicate. Read: ' R well-orders A.'
wff R We A
Definition	df-frfor 4376*	Define the well-founded relation predicate where A might be a proper class. By passing in S we allow it potentially to be a proper class rather than a set. (Contributed by Jim Kingdon and Mario Carneiro, 22-Sep-2021.)
|- (FrFor R A S <-> ( A. x e. A ( A. y e. A ( y R x -> y e. S ) -> x e. S ) -> A C_ S ) )
Definition	df-frind 4377*	Define the well-founded relation predicate. In the presence of excluded middle, there are a variety of equivalent ways to define this. In our case, this definition, in terms of an inductive principle, works better than one along the lines of "there is an element which is minimal when A is ordered by R". Because s is constrained to be a set (not a proper class) here, sometimes it may be necessary to use FrFor directly rather than via Fr. (Contributed by Jim Kingdon and Mario Carneiro, 21-Sep-2021.)
|- ( R Fr A <-> A. sFrFor R A s )
Definition	df-se 4378*	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-wetr 4379*	Define the well-ordering predicate. It is unusual to define "well-ordering" in the absence of excluded middle, but we mean an ordering which is like the ordering which we have for ordinals (for example, it does not entail trichotomy because ordinals do not have that as seen at ordtriexmid 4567). Given excluded middle, well-ordering is usually defined to require trichotomy (and the definition of Fr is typically also different). (Contributed by Mario Carneiro and Jim Kingdon, 23-Sep-2021.)
|- ( R We A <-> ( R Fr A /\ A. x e. A A. y e. A A. z e. A ( ( x R y /\ y R z ) -> x R z ) ) )
Theorem	seex 4380*	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 4381	Any relation on a set is set-like on it. (Contributed by Mario Carneiro, 22-Jun-2015.)
|- ( A e. V -> R Se A )
Theorem	sess1 4382	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 4383	Subset theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
|- ( A C_ B -> ( R Se B -> R Se A ) )
Theorem	seeq1 4384	Equality theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
|- ( R = S -> ( R Se A <-> S Se A ) )
Theorem	seeq2 4385	Equality theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
|- ( A = B -> ( R Se A <-> R Se B ) )
Theorem	nfse 4386	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	epse 4387	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	frforeq1 4388	Equality theorem for the well-founded predicate. (Contributed by Jim Kingdon, 22-Sep-2021.)
|- ( R = S -> (FrFor R A T <-> FrFor S A T ) )
Theorem	freq1 4389	Equality theorem for the well-founded predicate. (Contributed by NM, 9-Mar-1997.)
|- ( R = S -> ( R Fr A <-> S Fr A ) )
Theorem	frforeq2 4390	Equality theorem for the well-founded predicate. (Contributed by Jim Kingdon, 22-Sep-2021.)
|- ( A = B -> (FrFor R A T <-> FrFor R B T ) )
Theorem	freq2 4391	Equality theorem for the well-founded predicate. (Contributed by NM, 3-Apr-1994.)
|- ( A = B -> ( R Fr A <-> R Fr B ) )
Theorem	frforeq3 4392	Equality theorem for the well-founded predicate. (Contributed by Jim Kingdon, 22-Sep-2021.)
|- ( S = T -> (FrFor R A S <-> FrFor R A T ) )
Theorem	nffrfor 4393	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 S   =>    |- F/ xFrFor R A S
Theorem	nffr 4394	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	frirrg 4395	A well-founded relation is irreflexive. This is the case where A exists. (Contributed by Jim Kingdon, 21-Sep-2021.)
|- ( ( R Fr A /\ A e. V /\ B e. A ) -> -. B R B )
Theorem	fr0 4396	Any relation is well-founded on the empty set. (Contributed by NM, 17-Sep-1993.)
|- R Fr (/)
Theorem	frind 4397*	Induction over a well-founded set. (Contributed by Jim Kingdon, 28-Sep-2021.)
|- ( x = y -> ( ph <-> ps ) )   &    |- ( ( ch /\ x e. A ) -> ( A. y e. A ( y R x -> ps ) -> ph ) )   &    |- ( ch -> R Fr A )   &    |- ( ch -> A e. V )   =>    |- ( ( ch /\ x e. A ) -> ph )
Theorem	efrirr 4398	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	tz7.2 4399	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	nfwe 4400	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