P. 45 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 4401-4500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	brabga 4401*	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 4402*	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 4403*	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 4404*	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 4405*	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 4406*	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 4407*	The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopabg 4405 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 4408*	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 4409*	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 4410*	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 4411*	The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopab 4409 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 4412*	The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopab 4409 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 4413	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 4414	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 4415	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 4416*	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 4417	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 4418*	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 4419*	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 4420*	Membership in an ordered-pair class abstraction defined by a binary relation. (Contributed by AV, 16-Feb-2021.) (Proof shortened by SN, 11-Dec-2024.)
|- ( A e. { <. x , y >. | x R y } -> A e. R )
Theorem	elopabran 4421*	Membership in an ordered-pair class abstraction defined by a restricted binary relation. (Contributed by AV, 16-Feb-2021.)
|- ( A e. { <. x , y >. | ( x R y /\ ps ) } -> A e. R )
2.3.6  Power class of union and intersection
Theorem	pwin 4422	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 4423	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 4424	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 4425	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 4426	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 4427	Extend class notation to include the epsilon relation.
class _E
Syntax	cid 4428	Extend the definition of a class to include identity relation.
class _I
Definition	df-eprel 4429*	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 4430. Thus, 5 _E { 1 , 5 }. (Contributed by NM, 13-Aug-1995.)
|- _E = { <. x , y >. | x e. y }
Theorem	epelg 4430	The epsilon relation and membership are the same. General version of epel 4432. (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 4431	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 4432	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 4433*	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 4776), 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 4434	Extend wff notation to include the strict partial ordering predicate. Read: ' R is a partial order on A.'
wff R Po A
Syntax	wor 4435	Extend wff notation to include the strict linear ordering predicate. Read: ' R orders A.'
wff R Or A
Definition	df-po 4436*	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 4437*	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 4438	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 4439	Equality theorem for partial ordering predicate. (Contributed by NM, 27-Mar-1997.)
|- ( R = S -> ( R Po A <-> S Po A ) )
Theorem	poeq2 4440	Equality theorem for partial ordering predicate. (Contributed by NM, 27-Mar-1997.)
|- ( A = B -> ( R Po A <-> R Po B ) )
Theorem	nfpo 4441	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 4442	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 4443	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 4444*	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 4445*	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 4446*	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 4447	A partial order relation is irreflexive. (Contributed by NM, 27-Mar-1997.)
|- ( ( R Po A /\ B e. A ) -> -. B R B )
Theorem	potr 4448	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 4449	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 4450	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 4451	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 4452*	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 4453	A strict linear order is a strict partial order. (Contributed by NM, 28-Mar-1997.)
|- ( R Or A -> R Po A )
Theorem	soss 4454	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 4455	Equality theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.)
|- ( R = S -> ( R Or A <-> S Or A ) )
Theorem	soeq2 4456	Equality theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.)
|- ( A = B -> ( R Or A <-> R Or B ) )
Theorem	sonr 4457	A strict order relation is irreflexive. (Contributed by NM, 24-Nov-1995.)
|- ( ( R Or A /\ B e. A ) -> -. B R B )
Theorem	sotr 4458	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 4459*	An irreflexive, transitive, trichotomous relation is a linear ordering (in the sense of df-iso 4437). (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 4460	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 4461	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 4462	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 4463	One direction of sotritric 4464 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 4464	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 4465	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 4466	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 4467	Extend wff notation to include the well-founded predicate.
wff FrFor R A S
Syntax	wfr 4468	Extend wff notation to include the well-founded predicate. Read: ' R is a well-founded relation on A.'
wff R Fr A
Syntax	wse 4469	Extend wff notation to include the set-like predicate. Read: ' R is set-like on A.'
wff R Se A
Syntax	wwe 4470	Extend wff notation to include the well-ordering predicate. Read: ' R well-orders A.'
wff R We A
Definition	df-frfor 4471*	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 4472*	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 4473*	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 4474*	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 4663). 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 4475*	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 4476	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 4477	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 4478	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 4479	Equality theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
|- ( R = S -> ( R Se A <-> S Se A ) )
Theorem	seeq2 4480	Equality theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
|- ( A = B -> ( R Se A <-> R Se B ) )
Theorem	nfse 4481	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 4482	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 4483	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 4484	Equality theorem for the well-founded predicate. (Contributed by NM, 9-Mar-1997.)
|- ( R = S -> ( R Fr A <-> S Fr A ) )
Theorem	frforeq2 4485	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 4486	Equality theorem for the well-founded predicate. (Contributed by NM, 3-Apr-1994.)
|- ( A = B -> ( R Fr A <-> R Fr B ) )
Theorem	frforeq3 4487	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 4488	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 4489	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 4490	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 4491	Any relation is well-founded on the empty set. (Contributed by NM, 17-Sep-1993.)
|- R Fr (/)
Theorem	frind 4492*	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 4493	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 4494	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 4495	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	weeq1 4496	Equality theorem for the well-ordering predicate. (Contributed by NM, 9-Mar-1997.)
|- ( R = S -> ( R We A <-> S We A ) )
Theorem	weeq2 4497	Equality theorem for the well-ordering predicate. (Contributed by NM, 3-Apr-1994.)
|- ( A = B -> ( R We A <-> R We B ) )
Theorem	wefr 4498	A well-ordering is well-founded. (Contributed by NM, 22-Apr-1994.)
|- ( R We A -> R Fr A )
Theorem	wepo 4499	A well-ordering is a partial ordering. (Contributed by Jim Kingdon, 23-Sep-2021.)
|- ( ( R We A /\ A e. V ) -> R Po A )
Theorem	wetrep 4500*	An epsilon well-ordering is a transitive relation. (Contributed by NM, 22-Apr-1994.)
|- ( ( _E We A /\ ( x e. A /\ y e. A /\ z e. A ) ) -> ( ( x e. y /\ y e. z ) -> x e. z ) )