P. 61 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 6001-6100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mptss 6001*	Sufficient condition for inclusion among two functions in maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) ⊆ (𝑥 ∈ 𝐵 ↦ 𝐶))
Theorem	elidinxp 6002*	Characterization of the elements of the intersection of the identity relation with a Cartesian product. (Contributed by Peter Mazsa, 9-Sep-2022.)
⊢ (𝐶 ∈ ( I ∩ (𝐴 × 𝐵)) ↔ ∃𝑥 ∈ (𝐴 ∩ 𝐵)𝐶 = ⟨𝑥, 𝑥⟩)
Theorem	elidinxpid 6003*	Characterization of the elements of the intersection of the identity relation with a Cartesian square. (Contributed by Peter Mazsa, 9-Sep-2022.)
⊢ (𝐵 ∈ ( I ∩ (𝐴 × 𝐴)) ↔ ∃𝑥 ∈ 𝐴 𝐵 = ⟨𝑥, 𝑥⟩)
Theorem	elrid 6004*	Characterization of the elements of a restricted identity relation. (Contributed by BJ, 28-Aug-2022.) (Proof shortened by Peter Mazsa, 9-Sep-2022.)
⊢ (𝐴 ∈ ( I ↾ 𝑋) ↔ ∃𝑥 ∈ 𝑋 𝐴 = ⟨𝑥, 𝑥⟩)
Theorem	idinxpres 6005	The intersection of the identity relation with a cartesian product is the restriction of the identity relation to the intersection of the factors. (Contributed by FL, 2-Aug-2009.) (Proof shortened by Peter Mazsa, 9-Sep-2022.) Generalize statement from cartesian square (now idinxpresid 6006) to cartesian product. (Revised by BJ, 23-Dec-2023.)
⊢ ( I ∩ (𝐴 × 𝐵)) = ( I ↾ (𝐴 ∩ 𝐵))
Theorem	idinxpresid 6006	The intersection of the identity relation with the cartesian square of a class is the restriction of the identity relation to that class. (Contributed by FL, 2-Aug-2009.) (Proof shortened by Peter Mazsa, 9-Sep-2022.) (Proof shortened by BJ, 23-Dec-2023.)
⊢ ( I ∩ (𝐴 × 𝐴)) = ( I ↾ 𝐴)
Theorem	idssxp 6007	A diagonal set as a subset of a Cartesian square. (Contributed by Thierry Arnoux, 29-Dec-2019.) (Proof shortened by BJ, 9-Sep-2022.)
⊢ ( I ↾ 𝐴) ⊆ (𝐴 × 𝐴)
Theorem	opabresid 6008*	The restricted identity relation expressed as an ordered-pair class abstraction. (Contributed by FL, 25-Apr-2012.)
⊢ ( I ↾ 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑥)}
Theorem	mptresid 6009*	The restricted identity relation expressed in maps-to notation. (Contributed by FL, 25-Apr-2012.)
⊢ ( I ↾ 𝐴) = (𝑥 ∈ 𝐴 ↦ 𝑥)
Theorem	dmresi 6010	The domain of a restricted identity function. (Contributed by NM, 27-Aug-2004.)
⊢ dom ( I ↾ 𝐴) = 𝐴
Theorem	restidsing 6011	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	iresn0n0 6012	The identity function restricted to a class 𝐴 is empty iff the class 𝐴 is empty. (Contributed by AV, 30-Jan-2024.)
⊢ (𝐴 = ∅ ↔ ( I ↾ 𝐴) = ∅)
Theorem	imaeq1 6013	Equality theorem for image. (Contributed by NM, 14-Aug-1994.)
⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))
Theorem	imaeq2 6014	Equality theorem for image. (Contributed by NM, 14-Aug-1994.)
⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))
Theorem	imaeq1i 6015	Equality theorem for image. (Contributed by NM, 21-Dec-2008.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 “ 𝐶) = (𝐵 “ 𝐶)
Theorem	imaeq2i 6016	Equality theorem for image. (Contributed by NM, 21-Dec-2008.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 “ 𝐴) = (𝐶 “ 𝐵)
Theorem	imaeq1d 6017	Equality theorem for image. (Contributed by FL, 15-Dec-2006.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))
Theorem	imaeq2d 6018	Equality theorem for image. (Contributed by FL, 15-Dec-2006.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))
Theorem	imaeq12d 6019	Equality theorem for image. (Contributed by Mario Carneiro, 4-Dec-2016.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 “ 𝐶) = (𝐵 “ 𝐷))
Theorem	dfima2 6020*	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.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ (𝐴 “ 𝐵) = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑥𝐴𝑦}
Theorem	dfima3 6021*	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 6022*	Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by NM, 20-Jan-2007.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ (𝐵 “ 𝐶) ↔ ∃𝑥 ∈ 𝐶 𝑥𝐵𝐴))
Theorem	elima 6023*	Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by NM, 19-Apr-2004.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ (𝐵 “ 𝐶) ↔ ∃𝑥 ∈ 𝐶 𝑥𝐵𝐴)
Theorem	elima2 6024*	Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by NM, 11-Aug-2004.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ (𝐵 “ 𝐶) ↔ ∃𝑥(𝑥 ∈ 𝐶 ∧ 𝑥𝐵𝐴))
Theorem	elima3 6025*	Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by NM, 14-Aug-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ (𝐵 “ 𝐶) ↔ ∃𝑥(𝑥 ∈ 𝐶 ∧ ⟨𝑥, 𝐴⟩ ∈ 𝐵))
Theorem	nfima 6026	Bound-variable hypothesis builder for image. (Contributed by NM, 30-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝐴 “ 𝐵)
Theorem	nfimad 6027	Deduction version of bound-variable hypothesis builder nfima 6026. (Contributed by FL, 15-Dec-2006.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥(𝐴 “ 𝐵))
Theorem	imadmrn 6028	The image of the domain of a class is the range of the class. (Contributed by NM, 14-Aug-1994.)
⊢ (𝐴 “ dom 𝐴) = ran 𝐴
Theorem	imassrn 6029	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 6030*	Image of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) “ 𝐶) = ran (𝑥 ∈ (𝐴 ∩ 𝐶) ↦ 𝐵)
Theorem	imai 6031	Image under the identity relation. Theorem 3.16(viii) of [Monk1] p. 38. (Contributed by NM, 30-Apr-1998.)
⊢ ( I “ 𝐴) = 𝐴
Theorem	rnresi 6032	The range of the restricted identity function. (Contributed by NM, 27-Aug-2004.)
⊢ ran ( I ↾ 𝐴) = 𝐴
Theorem	resiima 6033	The image of a restriction of the identity function. (Contributed by FL, 31-Dec-2006.)
⊢ (𝐵 ⊆ 𝐴 → (( I ↾ 𝐴) “ 𝐵) = 𝐵)
Theorem	ima0 6034	Image of the empty set. Theorem 3.16(ii) of [Monk1] p. 38. (Contributed by NM, 20-May-1998.)
⊢ (𝐴 “ ∅) = ∅
Theorem	0ima 6035	Image under the empty relation. (Contributed by FL, 11-Jan-2007.)
⊢ (∅ “ 𝐴) = ∅
Theorem	csbima12 6036	Move class substitution in and out of the image of a function. (Contributed by FL, 15-Dec-2006.) (Revised by NM, 20-Aug-2018.)
⊢ ⦋𝐴 / 𝑥⦌(𝐹 “ 𝐵) = (⦋𝐴 / 𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌𝐵)
Theorem	imadisj 6037	A class whose image under another is empty is disjoint with the other's domain. (Contributed by FL, 24-Jan-2007.)
⊢ ((𝐴 “ 𝐵) = ∅ ↔ (dom 𝐴 ∩ 𝐵) = ∅)
Theorem	cnvimass 6038	A preimage under any class is included in the domain of the class. (Contributed by FL, 29-Jan-2007.)
⊢ (◡𝐴 “ 𝐵) ⊆ dom 𝐴
Theorem	cnvimarndm 6039	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 6040*	The image of a singleton. (Contributed by NM, 8-May-2005.)
⊢ (𝐴 ∈ 𝐵 → (𝑅 “ {𝐴}) = {𝑦 ∣ 𝐴𝑅𝑦})
Theorem	relimasn 6041*	The image of a singleton. (Contributed by NM, 20-May-1998.)
⊢ (Rel 𝑅 → (𝑅 “ {𝐴}) = {𝑦 ∣ 𝐴𝑅𝑦})
Theorem	elrelimasn 6042	Elementhood in the image of a singleton. (Contributed by Mario Carneiro, 3-Nov-2015.)
⊢ (Rel 𝑅 → (𝐵 ∈ (𝑅 “ {𝐴}) ↔ 𝐴𝑅𝐵))
Theorem	elimasng1 6043	Membership in an image of a singleton. (Contributed by Raph Levien, 21-Oct-2006.) Revise to use df-br 5111 and to prove elimasn1 6044 from it. (Revised by BJ, 16-Oct-2024.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐶 ∈ (𝐴 “ {𝐵}) ↔ 𝐵𝐴𝐶))
Theorem	elimasn1 6044	Membership in an image of a singleton. (Contributed by NM, 15-Mar-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) Use df-br 5111 and shorten proof. (Revised by BJ, 16-Oct-2024.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐶 ∈ (𝐴 “ {𝐵}) ↔ 𝐵𝐴𝐶)
Theorem	elimasng 6045	Membership in an image of a singleton. (Contributed by Raph Levien, 21-Oct-2006.) TODO: replace existing usages by usages of elimasng1 6043, remove, and relabel elimasng1 6043 to "elimasng".
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐶 ∈ (𝐴 “ {𝐵}) ↔ ⟨𝐵, 𝐶⟩ ∈ 𝐴))
Theorem	elimasn 6046	Membership in an image of a singleton. (Contributed by NM, 15-Mar-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Proof shortened by BJ, 16-Oct-2024.) TODO: replace existing usages by usages of elimasn1 6044, remove, and relabel elimasn1 6044 to "elimasn".
⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐶 ∈ (𝐴 “ {𝐵}) ↔ ⟨𝐵, 𝐶⟩ ∈ 𝐴)
Theorem	elimasngOLD 6047	Obsolete version of elimasng 6045 as of 16-Oct-2024. (Contributed by Raph Levien, 21-Oct-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐶 ∈ (𝐴 “ {𝐵}) ↔ ⟨𝐵, 𝐶⟩ ∈ 𝐴))
Theorem	elimasni 6048	Membership in an image of a singleton. (Contributed by NM, 5-Aug-2010.)
⊢ (𝐶 ∈ (𝐴 “ {𝐵}) → 𝐵𝐴𝐶)
Theorem	args 6049*	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). Observe the resemblance to the alternate definition dffv4 6844 of function value, which is based on the idea in Quine's definition. (Contributed by NM, 8-May-2005.)
⊢ {𝑥 ∣ ∃𝑦(𝐹 “ {𝑥}) = {𝑦}} = {𝑥 ∣ ∃!𝑦 𝑥𝐹𝑦}
Theorem	elinisegg 6050	Membership in the inverse image of a singleton. (Contributed by NM, 28-Apr-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) Put in closed form and shorten proof. (Revised by BJ, 16-Oct-2024.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐶 ∈ (◡𝐴 “ {𝐵}) ↔ 𝐶𝐴𝐵))
Theorem	eliniseg 6051	Membership in the inverse image of a singleton. An application is to express initial segments for an order relation. See 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	epin 6052	Any set is equal to its preimage under the converse membership relation. (Contributed by Mario Carneiro, 9-Mar-2013.) Put in closed form. (Revised by BJ, 16-Oct-2024.)
⊢ (𝐴 ∈ 𝑉 → (◡ E “ {𝐴}) = 𝐴)
Theorem	epini 6053	Any set is equal to its preimage under the converse membership relation. (Contributed by Mario Carneiro, 9-Mar-2013.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (◡ E “ {𝐴}) = 𝐴
Theorem	iniseg 6054*	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	inisegn0 6055	Nonemptiness of an initial segment in terms of range. (Contributed by Stefan O'Rear, 18-Jan-2015.)
⊢ (𝐴 ∈ ran 𝐹 ↔ (◡𝐹 “ {𝐴}) ≠ ∅)
Theorem	dffr3 6056*	Alternate definition of well-founded relation. Definition 6.21 of [TakeutiZaring] p. 30. (Contributed by NM, 23-Apr-2004.) (Revised by Mario Carneiro, 23-Jun-2015.)
⊢ (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅))
Theorem	dfse2 6057*	Alternate definition of set-like relation. (Contributed by Mario Carneiro, 23-Jun-2015.)
⊢ (𝑅 Se 𝐴 ↔ ∀𝑥 ∈ 𝐴 (𝐴 ∩ (◡𝑅 “ {𝑥})) ∈ V)
Theorem	imass1 6058	Subset theorem for image. (Contributed by NM, 16-Mar-2004.)
⊢ (𝐴 ⊆ 𝐵 → (𝐴 “ 𝐶) ⊆ (𝐵 “ 𝐶))
Theorem	imass2 6059	Subset theorem for image. Exercise 22(a) of [Enderton] p. 53. (Contributed by NM, 22-Mar-1998.)
⊢ (𝐴 ⊆ 𝐵 → (𝐶 “ 𝐴) ⊆ (𝐶 “ 𝐵))
Theorem	ndmima 6060	The image of a singleton outside the domain is empty. (Contributed by NM, 22-May-1998.) (Proof shortened by OpenAI, 3-Jul-2020.)
⊢ (¬ 𝐴 ∈ dom 𝐵 → (𝐵 “ {𝐴}) = ∅)
Theorem	relcnv 6061	A converse is a relation. Theorem 12 of [Suppes] p. 62. (Contributed by NM, 29-Oct-1996.)
⊢ Rel ◡𝐴
Theorem	relbrcnvg 6062	When 𝑅 is a relation, the sethood assumptions on brcnv 5843 can be omitted. (Contributed by Mario Carneiro, 28-Apr-2015.)
⊢ (Rel 𝑅 → (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴))
Theorem	eliniseg2 6063	Eliminate the class existence constraint in eliniseg 6051. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by Mario Carneiro, 17-Nov-2015.)
⊢ (Rel 𝐴 → (𝐶 ∈ (◡𝐴 “ {𝐵}) ↔ 𝐶𝐴𝐵))
Theorem	relbrcnv 6064	When 𝑅 is a relation, the sethood assumptions on brcnv 5843 can be omitted. (Contributed by Mario Carneiro, 28-Apr-2015.)
⊢ Rel 𝑅    ⇒   ⊢ (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴)
Theorem	relco 6065	A composition is a relation. Exercise 24 of [TakeutiZaring] p. 25. (Contributed by NM, 26-Jan-1997.)
⊢ Rel (𝐴 ∘ 𝐵)
Theorem	cotrg 6066*	Two ways of saying that the composition of two relations is included in a third relation. See its special instance cotr 6069 for the main application. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) Generalized from its special instance cotr 6069. (Revised by Richard Penner, 24-Dec-2019.) (Proof shortened by SN, 19-Dec-2024.) Avoid ax-11 2154. (Revised by BTernaryTau, 29-Dec-2024.)
⊢ ((𝐴 ∘ 𝐵) ⊆ 𝐶 ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))
Theorem	cotrgOLD 6067*	Obsolete version of cotrg 6066 as of 29-Dec-2024. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) Generalized from its special instance cotr 6069. (Revised by Richard Penner, 24-Dec-2019.) (Proof shortened by SN, 19-Dec-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∘ 𝐵) ⊆ 𝐶 ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))
Theorem	cotrgOLDOLD 6068*	Obsolete version of cotrg 6066 as of 19-Dec-2024. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) Generalized from its special instance cotr 6069. (Revised by Richard Penner, 24-Dec-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∘ 𝐵) ⊆ 𝐶 ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))
Theorem	cotr 6069*	Two ways of saying a relation is transitive. Definition of transitivity in [Schechter] p. 51. Special instance of cotrg 6066. (Contributed by NM, 27-Dec-1996.)
⊢ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
Theorem	idrefALT 6070*	Alternate proof of idref 7097 not relying on definitions related to functions. Two ways to state that a relation is reflexive on a class. (Contributed by FL, 15-Jan-2012.) (Proof shortened by Mario Carneiro, 3-Nov-2015.) (Revised by NM, 30-Mar-2016.) (Proof shortened by BJ, 28-Aug-2022.) The "proof modification is discouraged" tag is here only because this is an *ALT result. (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (( I ↾ 𝐴) ⊆ 𝑅 ↔ ∀𝑥 ∈ 𝐴 𝑥𝑅𝑥)
Theorem	cnvsym 6071*	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.) (Proof shortened by SN, 23-Dec-2024.) Avoid ax-11 2154. (Revised by BTernaryTau, 29-Dec-2024.)
⊢ (◡𝑅 ⊆ 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥))
Theorem	cnvsymOLD 6072*	Obsolete proof of cnvsym 6071 as of 29-Dec-2024. (Contributed by NM, 28-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Proof shortened by SN, 23-Dec-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (◡𝑅 ⊆ 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥))
Theorem	cnvsymOLDOLD 6073*	Obsolete proof of cnvsym 6071 as of 23-Dec-2024. (Contributed by NM, 28-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (◡𝑅 ⊆ 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥))
Theorem	intasym 6074*	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 6075*	Two ways of saying a relation is antisymmetric and reflexive. ∪ ∪ 𝑅 is the field of a relation by relfld 6232. (Contributed by NM, 6-May-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ((𝑅 ∩ ◡𝑅) = ( I ↾ ∪ ∪ 𝑅) ↔ ∀𝑥 ∈ ∪ ∪ 𝑅∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) ↔ 𝑥 = 𝑦))
Theorem	asymref2 6076*	Two ways of saying a relation is antisymmetric and reflexive. (Contributed by NM, 6-May-2008.) (Proof shortened by Mario Carneiro, 4-Dec-2016.)
⊢ ((𝑅 ∩ ◡𝑅) = ( I ↾ ∪ ∪ 𝑅) ↔ (∀𝑥 ∈ ∪ ∪ 𝑅𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦)))
Theorem	intirr 6077*	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 6078*	Two ways of saying that two elements have an upper bound. (Contributed by Mario Carneiro, 3-Nov-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴(◡𝑅 ∘ 𝑅)𝐵 ↔ ∃𝑧(𝐴𝑅𝑧 ∧ 𝐵𝑅𝑧)))
Theorem	codir 6079*	Two ways of saying a relation is directed. (Contributed by Mario Carneiro, 22-Nov-2013.)
⊢ ((𝐴 × 𝐵) ⊆ (◡𝑅 ∘ 𝑅) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∃𝑧(𝑥𝑅𝑧 ∧ 𝑦𝑅𝑧))
Theorem	qfto 6080*	A quantifier-free way of expressing the total order predicate. (Contributed by Mario Carneiro, 22-Nov-2013.)
⊢ ((𝐴 × 𝐵) ⊆ (𝑅 ∪ ◡𝑅) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑥))
Theorem	xpidtr 6081	A Cartesian square is a transitive relation. (Contributed by FL, 31-Jul-2009.)
⊢ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴)
Theorem	trin2 6082	The intersection of two transitive classes is transitive. (Contributed by FL, 31-Jul-2009.)
⊢ (((𝑅 ∘ 𝑅) ⊆ 𝑅 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ((𝑅 ∩ 𝑆) ∘ (𝑅 ∩ 𝑆)) ⊆ (𝑅 ∩ 𝑆))
Theorem	poirr2 6083	A partial order is irreflexive. (Contributed by Mario Carneiro, 2-Nov-2015.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ (𝑅 Po 𝐴 → (𝑅 ∩ ( I ↾ 𝐴)) = ∅)
Theorem	trinxp 6084	The relation induced by a transitive relation on a part of its field is transitive. (Taking the intersection of a relation with a Cartesian square is a way to restrict it to a subset of its field.) (Contributed by FL, 31-Jul-2009.)
⊢ ((𝑅 ∘ 𝑅) ⊆ 𝑅 → ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ (𝑅 ∩ (𝐴 × 𝐴)))
Theorem	soirri 6085	A strict order relation is irreflexive. (Contributed by NM, 10-Feb-1996.) (Revised by Mario Carneiro, 10-May-2013.)
⊢ 𝑅 Or 𝑆    &   ⊢ 𝑅 ⊆ (𝑆 × 𝑆)    ⇒   ⊢ ¬ 𝐴𝑅𝐴
Theorem	sotri 6086	A strict order relation is a transitive relation. (Contributed by NM, 10-Feb-1996.) (Revised by Mario Carneiro, 10-May-2013.)
⊢ 𝑅 Or 𝑆    &   ⊢ 𝑅 ⊆ (𝑆 × 𝑆)    ⇒   ⊢ ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶)
Theorem	son2lpi 6087	A strict order relation has no 2-cycle loops. (Contributed by NM, 10-Feb-1996.) (Revised by Mario Carneiro, 10-May-2013.)
⊢ 𝑅 Or 𝑆    &   ⊢ 𝑅 ⊆ (𝑆 × 𝑆)    ⇒   ⊢ ¬ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐴)
Theorem	sotri2 6088	A transitivity relation. (Read 𝐴 ≤ 𝐵 and 𝐵 < 𝐶 implies 𝐴 < 𝐶.) (Contributed by Mario Carneiro, 10-May-2013.)
⊢ 𝑅 Or 𝑆    &   ⊢ 𝑅 ⊆ (𝑆 × 𝑆)    ⇒   ⊢ ((𝐴 ∈ 𝑆 ∧ ¬ 𝐵𝑅𝐴 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶)
Theorem	sotri3 6089	A transitivity relation. (Read 𝐴 < 𝐵 and 𝐵 ≤ 𝐶 implies 𝐴 < 𝐶.) (Contributed by Mario Carneiro, 10-May-2013.)
⊢ 𝑅 Or 𝑆    &   ⊢ 𝑅 ⊆ (𝑆 × 𝑆)    ⇒   ⊢ ((𝐶 ∈ 𝑆 ∧ 𝐴𝑅𝐵 ∧ ¬ 𝐶𝑅𝐵) → 𝐴𝑅𝐶)
Theorem	poleloe 6090	Express "less than or equals" for general strict orders. (Contributed by Stefan O'Rear, 17-Jan-2015.)
⊢ (𝐵 ∈ 𝑉 → (𝐴(𝑅 ∪ I )𝐵 ↔ (𝐴𝑅𝐵 ∨ 𝐴 = 𝐵)))
Theorem	poltletr 6091	Transitive law for general strict orders. (Contributed by Stefan O'Rear, 17-Jan-2015.)
⊢ ((𝑅 Po 𝑋 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝑅𝐵 ∧ 𝐵(𝑅 ∪ I )𝐶) → 𝐴𝑅𝐶))
Theorem	somin1 6092	Property of a minimum in a strict order. (Contributed by Stefan O'Rear, 17-Jan-2015.)
⊢ ((𝑅 Or 𝑋 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → if(𝐴𝑅𝐵, 𝐴, 𝐵)(𝑅 ∪ I )𝐴)
Theorem	somincom 6093	Commutativity of minimum in a total order. (Contributed by Stefan O'Rear, 17-Jan-2015.)
⊢ ((𝑅 Or 𝑋 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → if(𝐴𝑅𝐵, 𝐴, 𝐵) = if(𝐵𝑅𝐴, 𝐵, 𝐴))
Theorem	somin2 6094	Property of a minimum in a strict order. (Contributed by Stefan O'Rear, 17-Jan-2015.)
⊢ ((𝑅 Or 𝑋 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → if(𝐴𝑅𝐵, 𝐴, 𝐵)(𝑅 ∪ I )𝐵)
Theorem	soltmin 6095	Being less than a minimum, for a general total order. (Contributed by Stefan O'Rear, 17-Jan-2015.)
⊢ ((𝑅 Or 𝑋 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑅if(𝐵𝑅𝐶, 𝐵, 𝐶) ↔ (𝐴𝑅𝐵 ∧ 𝐴𝑅𝐶)))
Theorem	cnvopab 6096*	The converse of a class abstraction of ordered pairs. (Contributed by NM, 11-Dec-2003.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ◡{⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑦, 𝑥⟩ ∣ 𝜑}
Theorem	mptcnv 6097*	The converse of a mapping function. (Contributed by Thierry Arnoux, 16-Jan-2017.)
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑦 ∈ 𝐶 ∧ 𝑥 = 𝐷)))    ⇒   ⊢ (𝜑 → ◡(𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐶 ↦ 𝐷))
Theorem	cnv0 6098	The converse of the empty set. (Contributed by NM, 6-Apr-1998.) Remove dependency on ax-sep 5261, ax-nul 5268, ax-pr 5389. (Revised by KP, 25-Oct-2021.)
⊢ ◡∅ = ∅
Theorem	cnvi 6099	The converse of the identity relation. Theorem 3.7(ii) of [Monk1] p. 36. (Contributed by NM, 26-Apr-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ◡ I = I
Theorem	cnvun 6100	The converse of a union is the union of converses. Theorem 16 of [Suppes] p. 62. (Contributed by NM, 25-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ◡(𝐴 ∪ 𝐵) = (◡𝐴 ∪ ◡𝐵)