P. 51 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 5001-5100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	resiun2 5001*	Distribution of restriction over indexed union. (Contributed by Mario Carneiro, 29-May-2015.)
⊢ (𝐶 ↾ ∪ 𝑥 ∈ 𝐴 𝐵) = ∪ 𝑥 ∈ 𝐴 (𝐶 ↾ 𝐵)
Theorem	dmres 5002	The domain of a restriction. Exercise 14 of [TakeutiZaring] p. 25. (Contributed by NM, 1-Aug-1994.)
⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴)
Theorem	ssdmres 5003	A domain restricted to a subclass equals the subclass. (Contributed by NM, 2-Mar-1997.)
⊢ (𝐴 ⊆ dom 𝐵 ↔ dom (𝐵 ↾ 𝐴) = 𝐴)
Theorem	dmresexg 5004	The domain of a restriction to a set exists. (Contributed by NM, 7-Apr-1995.)
⊢ (𝐵 ∈ 𝑉 → dom (𝐴 ↾ 𝐵) ∈ V)
Theorem	resss 5005	A class includes its restriction. Exercise 15 of [TakeutiZaring] p. 25. (Contributed by NM, 2-Aug-1994.)
⊢ (𝐴 ↾ 𝐵) ⊆ 𝐴
Theorem	rescom 5006	Commutative law for restriction. (Contributed by NM, 27-Mar-1998.)
⊢ ((𝐴 ↾ 𝐵) ↾ 𝐶) = ((𝐴 ↾ 𝐶) ↾ 𝐵)
Theorem	ssres 5007	Subclass theorem for restriction. (Contributed by NM, 16-Aug-1994.)
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ↾ 𝐶) ⊆ (𝐵 ↾ 𝐶))
Theorem	ssres2 5008	Subclass theorem for restriction. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ↾ 𝐴) ⊆ (𝐶 ↾ 𝐵))
Theorem	relres 5009	A restriction is a relation. Exercise 12 of [TakeutiZaring] p. 25. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ Rel (𝐴 ↾ 𝐵)
Theorem	resabs1 5010	Absorption law for restriction. Exercise 17 of [TakeutiZaring] p. 25. (Contributed by NM, 9-Aug-1994.)
⊢ (𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ 𝐵))
Theorem	resabs1d 5011	Absorption law for restriction, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ 𝐵))
Theorem	resabs2 5012	Absorption law for restriction. (Contributed by NM, 27-Mar-1998.)
⊢ (𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐵) ↾ 𝐶) = (𝐴 ↾ 𝐵))
Theorem	residm 5013	Idempotent law for restriction. (Contributed by NM, 27-Mar-1998.)
⊢ ((𝐴 ↾ 𝐵) ↾ 𝐵) = (𝐴 ↾ 𝐵)
Theorem	resima 5014	A restriction to an image. (Contributed by NM, 29-Sep-2004.)
⊢ ((𝐴 ↾ 𝐵) “ 𝐵) = (𝐴 “ 𝐵)
Theorem	resima2 5015	Image under a restricted class. (Contributed by FL, 31-Aug-2009.)
⊢ (𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) “ 𝐵) = (𝐴 “ 𝐵))
Theorem	xpssres 5016	Restriction of a constant function (or other cross product). (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ (𝐶 ⊆ 𝐴 → ((𝐴 × 𝐵) ↾ 𝐶) = (𝐶 × 𝐵))
Theorem	elres 5017*	Membership in a restriction. (Contributed by Scott Fenton, 17-Mar-2011.)
⊢ (𝐴 ∈ (𝐵 ↾ 𝐶) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐵))
Theorem	elsnres 5018*	Memebership in restriction to a singleton. (Contributed by Scott Fenton, 17-Mar-2011.)
⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐴 ∈ (𝐵 ↾ {𝐶}) ↔ ∃𝑦(𝐴 = ⟨𝐶, 𝑦⟩ ∧ ⟨𝐶, 𝑦⟩ ∈ 𝐵))
Theorem	relssres 5019	Simplification law for restriction. (Contributed by NM, 16-Aug-1994.)
⊢ ((Rel 𝐴 ∧ dom 𝐴 ⊆ 𝐵) → (𝐴 ↾ 𝐵) = 𝐴)
Theorem	resdm 5020	A relation restricted to its domain equals itself. (Contributed by NM, 12-Dec-2006.)
⊢ (Rel 𝐴 → (𝐴 ↾ dom 𝐴) = 𝐴)
Theorem	resexg 5021	The restriction of a set is a set. (Contributed by NM, 28-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ↾ 𝐵) ∈ V)
Theorem	resex 5022	The restriction of a set is a set. (Contributed by Jeff Madsen, 19-Jun-2011.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ↾ 𝐵) ∈ V
Theorem	resindm 5023	When restricting a relation, intersecting with the domain of the relation has no effect. (Contributed by FL, 6-Oct-2008.)
⊢ (Rel 𝐴 → (𝐴 ↾ (𝐵 ∩ dom 𝐴)) = (𝐴 ↾ 𝐵))
Theorem	resdmdfsn 5024	Restricting a relation to its domain without a set is the same as restricting the relation to the universe without this set. (Contributed by AV, 2-Dec-2018.)
⊢ (Rel 𝑅 → (𝑅 ↾ (V ∖ {𝑋})) = (𝑅 ↾ (dom 𝑅 ∖ {𝑋})))
Theorem	resopab 5025*	Restriction of a class abstraction of ordered pairs. (Contributed by NM, 5-Nov-2002.)
⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ↾ 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
Theorem	resiexg 5026	The existence of a restricted identity function, proved without using the Axiom of Replacement. (Contributed by NM, 13-Jan-2007.)
⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) ∈ V)
Theorem	iss 5027	A subclass of the identity function is the identity function restricted to its domain. (Contributed by NM, 13-Dec-2003.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (𝐴 ⊆ I ↔ 𝐴 = ( I ↾ dom 𝐴))
Theorem	resopab2 5028*	Restriction of a class abstraction of ordered pairs. (Contributed by NM, 24-Aug-2007.)
⊢ (𝐴 ⊆ 𝐵 → ({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)} ↾ 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)})
Theorem	resmpt 5029*	Restriction of the mapping operation. (Contributed by Mario Carneiro, 15-Jul-2013.)
⊢ (𝐵 ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ 𝐶))
Theorem	resmpt3 5030*	Unconditional restriction of the mapping operation. (Contributed by Stefan O'Rear, 24-Jan-2015.) (Proof shortened by Mario Carneiro, 22-Mar-2015.)
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ (𝐴 ∩ 𝐵) ↦ 𝐶)
Theorem	resmptf 5031	Restriction of the mapping operation. (Contributed by Thierry Arnoux, 28-Mar-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐵 ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ 𝐶))
Theorem	resmptd 5032*	Restriction of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ 𝐶))
Theorem	dfres2 5033*	Alternate definition of the restriction operation. (Contributed by Mario Carneiro, 5-Nov-2013.)
⊢ (𝑅 ↾ 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑥𝑅𝑦)}
Theorem	opabresid 5034*	The restricted identity relation expressed as an ordered-pair class abstraction. (Contributed by FL, 25-Apr-2012.)
⊢ ( I ↾ 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑥)}
Theorem	mptresid 5035*	The restricted identity relation expressed in maps-to notation. (Contributed by FL, 25-Apr-2012.)
⊢ ( I ↾ 𝐴) = (𝑥 ∈ 𝐴 ↦ 𝑥)
Theorem	dmresi 5036	The domain of a restricted identity function. (Contributed by NM, 27-Aug-2004.)
⊢ dom ( I ↾ 𝐴) = 𝐴
Theorem	restidsing 5037	Restriction of the identity to a singleton. (Contributed by FL, 2-Aug-2009.) (Proof shortened by JJ, 25-Aug-2021.) (Proof shortened by Peter Mazsa, 6-Oct-2022.)
⊢ ( I ↾ {𝐴}) = ({𝐴} × {𝐴})
Theorem	resid 5038	Any relation restricted to the universe is itself. (Contributed by NM, 16-Mar-2004.)
⊢ (Rel 𝐴 → (𝐴 ↾ V) = 𝐴)
Theorem	imaeq1 5039	Equality theorem for image. (Contributed by NM, 14-Aug-1994.)
⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))
Theorem	imaeq2 5040	Equality theorem for image. (Contributed by NM, 14-Aug-1994.)
⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))
Theorem	imaeq1i 5041	Equality theorem for image. (Contributed by NM, 21-Dec-2008.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 “ 𝐶) = (𝐵 “ 𝐶)
Theorem	imaeq2i 5042	Equality theorem for image. (Contributed by NM, 21-Dec-2008.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 “ 𝐴) = (𝐶 “ 𝐵)
Theorem	imaeq1d 5043	Equality theorem for image. (Contributed by FL, 15-Dec-2006.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))
Theorem	imaeq2d 5044	Equality theorem for image. (Contributed by FL, 15-Dec-2006.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))
Theorem	imaeq12d 5045	Equality theorem for image. (Contributed by Mario Carneiro, 4-Dec-2016.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 “ 𝐶) = (𝐵 “ 𝐷))
Theorem	dfima2 5046*	Alternate definition of image. Compare definition (d) of [Enderton] p. 44. (Contributed by NM, 19-Apr-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (𝐴 “ 𝐵) = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑥𝐴𝑦}
Theorem	dfima3 5047*	Alternate definition of image. Compare definition (d) of [Enderton] p. 44. (Contributed by NM, 14-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (𝐴 “ 𝐵) = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)}
Theorem	elimag 5048*	Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by NM, 20-Jan-2007.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ (𝐵 “ 𝐶) ↔ ∃𝑥 ∈ 𝐶 𝑥𝐵𝐴))
Theorem	elima 5049*	Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by NM, 19-Apr-2004.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ (𝐵 “ 𝐶) ↔ ∃𝑥 ∈ 𝐶 𝑥𝐵𝐴)
Theorem	elima2 5050*	Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by NM, 11-Aug-2004.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ (𝐵 “ 𝐶) ↔ ∃𝑥(𝑥 ∈ 𝐶 ∧ 𝑥𝐵𝐴))
Theorem	elima3 5051*	Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by NM, 14-Aug-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ (𝐵 “ 𝐶) ↔ ∃𝑥(𝑥 ∈ 𝐶 ∧ ⟨𝑥, 𝐴⟩ ∈ 𝐵))
Theorem	nfima 5052	Bound-variable hypothesis builder for image. (Contributed by NM, 30-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝐴 “ 𝐵)
Theorem	nfimad 5053	Deduction version of bound-variable hypothesis builder nfima 5052. (Contributed by FL, 15-Dec-2006.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥(𝐴 “ 𝐵))
Theorem	imadmrn 5054	The image of the domain of a class is the range of the class. (Contributed by NM, 14-Aug-1994.)
⊢ (𝐴 “ dom 𝐴) = ran 𝐴
Theorem	imassrn 5055	The image of a class is a subset of its range. Theorem 3.16(xi) of [Monk1] p. 39. (Contributed by NM, 31-Mar-1995.)
⊢ (𝐴 “ 𝐵) ⊆ ran 𝐴
Theorem	mptima 5056*	Image of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) “ 𝐶) = ran (𝑥 ∈ (𝐴 ∩ 𝐶) ↦ 𝐵)
Theorem	mptimass 5057*	Image of a function in maps-to notation for a subset. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝐶 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) “ 𝐶) = ran (𝑥 ∈ 𝐶 ↦ 𝐵))
Theorem	imaexg 5058	The image of a set is a set. Theorem 3.17 of [Monk1] p. 39. (Contributed by NM, 24-Jul-1995.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 “ 𝐵) ∈ V)
Theorem	imaex 5059	The image of a set is a set. Theorem 3.17 of [Monk1] p. 39. (Contributed by JJ, 24-Sep-2021.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 “ 𝐵) ∈ V
Theorem	imai 5060	Image under the identity relation. Theorem 3.16(viii) of [Monk1] p. 38. (Contributed by NM, 30-Apr-1998.)
⊢ ( I “ 𝐴) = 𝐴
Theorem	rnresi 5061	The range of the restricted identity function. (Contributed by NM, 27-Aug-2004.)
⊢ ran ( I ↾ 𝐴) = 𝐴
Theorem	resiima 5062	The image of a restriction of the identity function. (Contributed by FL, 31-Dec-2006.)
⊢ (𝐵 ⊆ 𝐴 → (( I ↾ 𝐴) “ 𝐵) = 𝐵)
Theorem	ima0 5063	Image of the empty set. Theorem 3.16(ii) of [Monk1] p. 38. (Contributed by NM, 20-May-1998.)
⊢ (𝐴 “ ∅) = ∅
Theorem	0ima 5064	Image under the empty relation. (Contributed by FL, 11-Jan-2007.)
⊢ (∅ “ 𝐴) = ∅
Theorem	csbima12g 5065	Move class substitution in and out of the image of a function. (Contributed by FL, 15-Dec-2006.) (Proof shortened by Mario Carneiro, 4-Dec-2016.)
⊢ (𝐴 ∈ 𝐶 → ⦋𝐴 / 𝑥⦌(𝐹 “ 𝐵) = (⦋𝐴 / 𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌𝐵))
Theorem	imadisj 5066	A class whose image under another is empty is disjoint with the other's domain. (Contributed by FL, 24-Jan-2007.)
⊢ ((𝐴 “ 𝐵) = ∅ ↔ (dom 𝐴 ∩ 𝐵) = ∅)
Theorem	cnvimass 5067	A preimage under any class is included in the domain of the class. (Contributed by FL, 29-Jan-2007.)
⊢ (◡𝐴 “ 𝐵) ⊆ dom 𝐴
Theorem	cnvimarndm 5068	The preimage of the range of a class is the domain of the class. (Contributed by Jeff Hankins, 15-Jul-2009.)
⊢ (◡𝐴 “ ran 𝐴) = dom 𝐴
Theorem	imasng 5069*	The image of a singleton. (Contributed by NM, 8-May-2005.)
⊢ (𝐴 ∈ 𝐵 → (𝑅 “ {𝐴}) = {𝑦 ∣ 𝐴𝑅𝑦})
Theorem	elrelimasn 5070	Elementhood in the image of a singleton. (Contributed by Mario Carneiro, 3-Nov-2015.)
⊢ (Rel 𝑅 → (𝐵 ∈ (𝑅 “ {𝐴}) ↔ 𝐴𝑅𝐵))
Theorem	elimasn 5071	Membership in an image of a singleton. (Contributed by NM, 15-Mar-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐶 ∈ (𝐴 “ {𝐵}) ↔ ⟨𝐵, 𝐶⟩ ∈ 𝐴)
Theorem	elimasng 5072	Membership in an image of a singleton. (Contributed by Raph Levien, 21-Oct-2006.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐶 ∈ (𝐴 “ {𝐵}) ↔ ⟨𝐵, 𝐶⟩ ∈ 𝐴))
Theorem	args 5073*	Two ways to express the class of unique-valued arguments of 𝐹, which is the same as the domain of 𝐹 whenever 𝐹 is a function. The left-hand side of the equality is from Definition 10.2 of [Quine] p. 65. Quine uses the notation "arg 𝐹 " for this class (for which we have no separate notation). (Contributed by NM, 8-May-2005.)
⊢ {𝑥 ∣ ∃𝑦(𝐹 “ {𝑥}) = {𝑦}} = {𝑥 ∣ ∃!𝑦 𝑥𝐹𝑦}
Theorem	eliniseg 5074	Membership in an initial segment. The idiom (◡𝐴 “ {𝐵}), meaning {𝑥 ∣ 𝑥𝐴𝐵}, is used to specify an initial segment in (for example) Definition 6.21 of [TakeutiZaring] p. 30. (Contributed by NM, 28-Apr-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐵 ∈ 𝑉 → (𝐶 ∈ (◡𝐴 “ {𝐵}) ↔ 𝐶𝐴𝐵))
Theorem	epini 5075	Any set is equal to its preimage under the converse epsilon relation. (Contributed by Mario Carneiro, 9-Mar-2013.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (◡ E “ {𝐴}) = 𝐴
Theorem	iniseg 5076*	An idiom that signifies an initial segment of an ordering, used, for example, in Definition 6.21 of [TakeutiZaring] p. 30. (Contributed by NM, 28-Apr-2004.)
⊢ (𝐵 ∈ 𝑉 → (◡𝐴 “ {𝐵}) = {𝑥 ∣ 𝑥𝐴𝐵})
Theorem	dfse2 5077*	Alternate definition of set-like relation. (Contributed by Mario Carneiro, 23-Jun-2015.)
⊢ (𝑅 Se 𝐴 ↔ ∀𝑥 ∈ 𝐴 (𝐴 ∩ (◡𝑅 “ {𝑥})) ∈ V)
Theorem	exse2 5078	Any set relation is set-like. (Contributed by Mario Carneiro, 22-Jun-2015.)
⊢ (𝑅 ∈ 𝑉 → 𝑅 Se 𝐴)
Theorem	imass1 5079	Subset theorem for image. (Contributed by NM, 16-Mar-2004.)
⊢ (𝐴 ⊆ 𝐵 → (𝐴 “ 𝐶) ⊆ (𝐵 “ 𝐶))
Theorem	imass2 5080	Subset theorem for image. Exercise 22(a) of [Enderton] p. 53. (Contributed by NM, 22-Mar-1998.)
⊢ (𝐴 ⊆ 𝐵 → (𝐶 “ 𝐴) ⊆ (𝐶 “ 𝐵))
Theorem	ndmima 5081	The image of a singleton outside the domain is empty. (Contributed by NM, 22-May-1998.)
⊢ (¬ 𝐴 ∈ dom 𝐵 → (𝐵 “ {𝐴}) = ∅)
Theorem	relcnv 5082	A converse is a relation. Theorem 12 of [Suppes] p. 62. (Contributed by NM, 29-Oct-1996.)
⊢ Rel ◡𝐴
Theorem	relbrcnvg 5083	When 𝑅 is a relation, the sethood assumptions on brcnv 4882 can be omitted. (Contributed by Mario Carneiro, 28-Apr-2015.)
⊢ (Rel 𝑅 → (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴))
Theorem	eliniseg2 5084	Eliminate the class existence constraint in eliniseg 5074. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by Mario Carneiro, 17-Nov-2015.)
⊢ (Rel 𝐴 → (𝐶 ∈ (◡𝐴 “ {𝐵}) ↔ 𝐶𝐴𝐵))
Theorem	relbrcnv 5085	When 𝑅 is a relation, the sethood assumptions on brcnv 4882 can be omitted. (Contributed by Mario Carneiro, 28-Apr-2015.)
⊢ Rel 𝑅    ⇒   ⊢ (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴)
Theorem	cotr 5086*	Two ways of saying a relation is transitive. Definition of transitivity in [Schechter] p. 51. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
Theorem	issref 5087*	Two ways to state a relation is reflexive. Adapted from Tarski. (Contributed by FL, 15-Jan-2012.) (Revised by NM, 30-Mar-2016.)
⊢ (( I ↾ 𝐴) ⊆ 𝑅 ↔ ∀𝑥 ∈ 𝐴 𝑥𝑅𝑥)
Theorem	cnvsym 5088*	Two ways of saying a relation is symmetric. Similar to definition of symmetry in [Schechter] p. 51. (Contributed by NM, 28-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (◡𝑅 ⊆ 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥))
Theorem	intasym 5089*	Two ways of saying a relation is antisymmetric. Definition of antisymmetry in [Schechter] p. 51. (Contributed by NM, 9-Sep-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ((𝑅 ∩ ◡𝑅) ⊆ I ↔ ∀𝑥∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦))
Theorem	asymref 5090*	Two ways of saying a relation is antisymmetric and reflexive. ∪ ∪ 𝑅 is the field of a relation by relfld 5233. (Contributed by NM, 6-May-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ((𝑅 ∩ ◡𝑅) = ( I ↾ ∪ ∪ 𝑅) ↔ ∀𝑥 ∈ ∪ ∪ 𝑅∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) ↔ 𝑥 = 𝑦))
Theorem	intirr 5091*	Two ways of saying a relation is irreflexive. Definition of irreflexivity in [Schechter] p. 51. (Contributed by NM, 9-Sep-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ((𝑅 ∩ I ) = ∅ ↔ ∀𝑥 ¬ 𝑥𝑅𝑥)
Theorem	brcodir 5092*	Two ways of saying that two elements have an upper bound. (Contributed by Mario Carneiro, 3-Nov-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴(◡𝑅 ∘ 𝑅)𝐵 ↔ ∃𝑧(𝐴𝑅𝑧 ∧ 𝐵𝑅𝑧)))
Theorem	codir 5093*	Two ways of saying a relation is directed. (Contributed by Mario Carneiro, 22-Nov-2013.)
⊢ ((𝐴 × 𝐵) ⊆ (◡𝑅 ∘ 𝑅) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∃𝑧(𝑥𝑅𝑧 ∧ 𝑦𝑅𝑧))
Theorem	qfto 5094*	A quantifier-free way of expressing the total order predicate. (Contributed by Mario Carneiro, 22-Nov-2013.)
⊢ ((𝐴 × 𝐵) ⊆ (𝑅 ∪ ◡𝑅) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑥))
Theorem	xpidtr 5095	A square cross product (𝐴 × 𝐴) is a transitive relation. (Contributed by FL, 31-Jul-2009.)
⊢ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴)
Theorem	trin2 5096	The intersection of two transitive classes is transitive. (Contributed by FL, 31-Jul-2009.)
⊢ (((𝑅 ∘ 𝑅) ⊆ 𝑅 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ((𝑅 ∩ 𝑆) ∘ (𝑅 ∩ 𝑆)) ⊆ (𝑅 ∩ 𝑆))
Theorem	poirr2 5097	A partial order relation is irreflexive. (Contributed by Mario Carneiro, 2-Nov-2015.)
⊢ (𝑅 Po 𝐴 → (𝑅 ∩ ( I ↾ 𝐴)) = ∅)
Theorem	trinxp 5098	The relation induced by a transitive relation on a part of its field is transitive. (Taking the intersection of a relation with a square cross product is a way to restrict it to a subset of its field.) (Contributed by FL, 31-Jul-2009.)
⊢ ((𝑅 ∘ 𝑅) ⊆ 𝑅 → ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ (𝑅 ∩ (𝐴 × 𝐴)))
Theorem	soirri 5099	A strict order relation is irreflexive. (Contributed by NM, 10-Feb-1996.) (Revised by Mario Carneiro, 10-May-2013.)
⊢ 𝑅 Or 𝑆    &   ⊢ 𝑅 ⊆ (𝑆 × 𝑆)    ⇒   ⊢ ¬ 𝐴𝑅𝐴
Theorem	sotri 5100	A strict order relation is a transitive relation. (Contributed by NM, 10-Feb-1996.) (Revised by Mario Carneiro, 10-May-2013.)
⊢ 𝑅 Or 𝑆    &   ⊢ 𝑅 ⊆ (𝑆 × 𝑆)    ⇒   ⊢ ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶)