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	idinxpresid 6001	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 6002	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 6003*	The restricted identity relation expressed as an ordered-pair class abstraction. (Contributed by FL, 25-Apr-2012.)
⊢ ( I ↾ 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑥)}
Theorem	mptresid 6004*	The restricted identity relation expressed in maps-to notation. (Contributed by FL, 25-Apr-2012.)
⊢ ( I ↾ 𝐴) = (𝑥 ∈ 𝐴 ↦ 𝑥)
Theorem	dmresi 6005	The domain of a restricted identity function. (Contributed by NM, 27-Aug-2004.)
⊢ dom ( I ↾ 𝐴) = 𝐴
Theorem	restidsing 6006	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 6007	The identity function restricted to a class 𝐴 is empty iff the class 𝐴 is empty. (Contributed by AV, 30-Jan-2024.)
⊢ (𝐴 = ∅ ↔ ( I ↾ 𝐴) = ∅)
Theorem	imaeq1 6008	Equality theorem for image. (Contributed by NM, 14-Aug-1994.)
⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))
Theorem	imaeq2 6009	Equality theorem for image. (Contributed by NM, 14-Aug-1994.)
⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))
Theorem	imaeq1i 6010	Equality theorem for image. (Contributed by NM, 21-Dec-2008.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 “ 𝐶) = (𝐵 “ 𝐶)
Theorem	imaeq2i 6011	Equality theorem for image. (Contributed by NM, 21-Dec-2008.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 “ 𝐴) = (𝐶 “ 𝐵)
Theorem	imaeq1d 6012	Equality theorem for image. (Contributed by FL, 15-Dec-2006.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))
Theorem	imaeq2d 6013	Equality theorem for image. (Contributed by FL, 15-Dec-2006.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))
Theorem	imaeq12d 6014	Equality theorem for image. (Contributed by Mario Carneiro, 4-Dec-2016.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 “ 𝐶) = (𝐵 “ 𝐷))
Theorem	dfima2 6015*	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 6016*	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 6017*	Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by NM, 20-Jan-2007.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ (𝐵 “ 𝐶) ↔ ∃𝑥 ∈ 𝐶 𝑥𝐵𝐴))
Theorem	elima 6018*	Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by NM, 19-Apr-2004.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ (𝐵 “ 𝐶) ↔ ∃𝑥 ∈ 𝐶 𝑥𝐵𝐴)
Theorem	elima2 6019*	Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by NM, 11-Aug-2004.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ (𝐵 “ 𝐶) ↔ ∃𝑥(𝑥 ∈ 𝐶 ∧ 𝑥𝐵𝐴))
Theorem	elima3 6020*	Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by NM, 14-Aug-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ (𝐵 “ 𝐶) ↔ ∃𝑥(𝑥 ∈ 𝐶 ∧ ⟨𝑥, 𝐴⟩ ∈ 𝐵))
Theorem	nfima 6021	Bound-variable hypothesis builder for image. (Contributed by NM, 30-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝐴 “ 𝐵)
Theorem	nfimad 6022	Deduction version of bound-variable hypothesis builder nfima 6021. (Contributed by FL, 15-Dec-2006.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥(𝐴 “ 𝐵))
Theorem	imadmrn 6023	The image of the domain of a class is the range of the class. (Contributed by NM, 14-Aug-1994.)
⊢ (𝐴 “ dom 𝐴) = ran 𝐴
Theorem	imassrn 6024	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 6025*	Image of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) “ 𝐶) = ran (𝑥 ∈ (𝐴 ∩ 𝐶) ↦ 𝐵)
Theorem	mptimass 6026*	Image of a function in maps-to notation for a subset. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝐶 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) “ 𝐶) = ran (𝑥 ∈ 𝐶 ↦ 𝐵))
Theorem	imai 6027	Image under the identity relation. Theorem 3.16(viii) of [Monk1] p. 38. (Contributed by NM, 30-Apr-1998.)
⊢ ( I “ 𝐴) = 𝐴
Theorem	rnresi 6028	The range of the restricted identity function. (Contributed by NM, 27-Aug-2004.)
⊢ ran ( I ↾ 𝐴) = 𝐴
Theorem	resiima 6029	The image of a restriction of the identity function. (Contributed by FL, 31-Dec-2006.)
⊢ (𝐵 ⊆ 𝐴 → (( I ↾ 𝐴) “ 𝐵) = 𝐵)
Theorem	ima0 6030	Image of the empty set. Theorem 3.16(ii) of [Monk1] p. 38. (Contributed by NM, 20-May-1998.)
⊢ (𝐴 “ ∅) = ∅
Theorem	0ima 6031	Image under the empty relation. (Contributed by FL, 11-Jan-2007.)
⊢ (∅ “ 𝐴) = ∅
Theorem	csbima12 6032	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 6033	A class whose image under another is empty is disjoint with the other's domain. (Contributed by FL, 24-Jan-2007.)
⊢ ((𝐴 “ 𝐵) = ∅ ↔ (dom 𝐴 ∩ 𝐵) = ∅)
Theorem	imadisjlnd 6034	Deduction form of one negated side of imadisj 6033. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → (dom 𝐴 ∩ 𝐵) ≠ ∅)    ⇒   ⊢ (𝜑 → (𝐴 “ 𝐵) ≠ ∅)
Theorem	cnvimass 6035	A preimage under any class is included in the domain of the class. (Contributed by FL, 29-Jan-2007.)
⊢ (◡𝐴 “ 𝐵) ⊆ dom 𝐴
Theorem	cnvimarndm 6036	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 6037*	The image of a singleton. (Contributed by NM, 8-May-2005.)
⊢ (𝐴 ∈ 𝐵 → (𝑅 “ {𝐴}) = {𝑦 ∣ 𝐴𝑅𝑦})
Theorem	relimasn 6038*	The image of a singleton. (Contributed by NM, 20-May-1998.)
⊢ (Rel 𝑅 → (𝑅 “ {𝐴}) = {𝑦 ∣ 𝐴𝑅𝑦})
Theorem	elrelimasn 6039	Elementhood in the image of a singleton. (Contributed by Mario Carneiro, 3-Nov-2015.)
⊢ (Rel 𝑅 → (𝐵 ∈ (𝑅 “ {𝐴}) ↔ 𝐴𝑅𝐵))
Theorem	elimasng1 6040	Membership in an image of a singleton. (Contributed by Raph Levien, 21-Oct-2006.) Revise to use df-br 5094 and to prove elimasn1 6041 from it. (Revised by BJ, 16-Oct-2024.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐶 ∈ (𝐴 “ {𝐵}) ↔ 𝐵𝐴𝐶))
Theorem	elimasn1 6041	Membership in an image of a singleton. (Contributed by NM, 15-Mar-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) Use df-br 5094 and shorten proof. (Revised by BJ, 16-Oct-2024.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐶 ∈ (𝐴 “ {𝐵}) ↔ 𝐵𝐴𝐶)
Theorem	elimasng 6042	Membership in an image of a singleton. (Contributed by Raph Levien, 21-Oct-2006.) TODO: replace existing usages by usages of elimasng1 6040, remove, and relabel elimasng1 6040 to "elimasng".
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐶 ∈ (𝐴 “ {𝐵}) ↔ ⟨𝐵, 𝐶⟩ ∈ 𝐴))
Theorem	elimasn 6043	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 6041, remove, and relabel elimasn1 6041 to "elimasn".
⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐶 ∈ (𝐴 “ {𝐵}) ↔ ⟨𝐵, 𝐶⟩ ∈ 𝐴)
Theorem	elimasni 6044	Membership in an image of a singleton. (Contributed by NM, 5-Aug-2010.)
⊢ (𝐶 ∈ (𝐴 “ {𝐵}) → 𝐵𝐴𝐶)
Theorem	args 6045*	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 6825 of function value, which is based on the idea in Quine's definition. (Contributed by NM, 8-May-2005.)
⊢ {𝑥 ∣ ∃𝑦(𝐹 “ {𝑥}) = {𝑦}} = {𝑥 ∣ ∃!𝑦 𝑥𝐹𝑦}
Theorem	elinisegg 6046	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 6047	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 6048	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 6049	Any set is equal to its preimage under the converse membership relation. (Contributed by Mario Carneiro, 9-Mar-2013.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (◡ E “ {𝐴}) = 𝐴
Theorem	iniseg 6050*	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 6051	Nonemptiness of an initial segment in terms of range. (Contributed by Stefan O'Rear, 18-Jan-2015.)
⊢ (𝐴 ∈ ran 𝐹 ↔ (◡𝐹 “ {𝐴}) ≠ ∅)
Theorem	dffr3 6052*	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 6053*	Alternate definition of set-like relation. (Contributed by Mario Carneiro, 23-Jun-2015.)
⊢ (𝑅 Se 𝐴 ↔ ∀𝑥 ∈ 𝐴 (𝐴 ∩ (◡𝑅 “ {𝑥})) ∈ V)
Theorem	imass1 6054	Subset theorem for image. (Contributed by NM, 16-Mar-2004.)
⊢ (𝐴 ⊆ 𝐵 → (𝐴 “ 𝐶) ⊆ (𝐵 “ 𝐶))
Theorem	imass2 6055	Subset theorem for image. Exercise 22(a) of [Enderton] p. 53. (Contributed by NM, 22-Mar-1998.)
⊢ (𝐴 ⊆ 𝐵 → (𝐶 “ 𝐴) ⊆ (𝐶 “ 𝐵))
Theorem	ndmima 6056	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 6057	A converse is a relation. Theorem 12 of [Suppes] p. 62. (Contributed by NM, 29-Oct-1996.)
⊢ Rel ◡𝐴
Theorem	relbrcnvg 6058	When 𝑅 is a relation, the sethood assumptions on brcnv 5826 can be omitted. (Contributed by Mario Carneiro, 28-Apr-2015.)
⊢ (Rel 𝑅 → (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴))
Theorem	eliniseg2 6059	Eliminate the class existence constraint in eliniseg 6047. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by Mario Carneiro, 17-Nov-2015.)
⊢ (Rel 𝐴 → (𝐶 ∈ (◡𝐴 “ {𝐵}) ↔ 𝐶𝐴𝐵))
Theorem	relbrcnv 6060	When 𝑅 is a relation, the sethood assumptions on brcnv 5826 can be omitted. (Contributed by Mario Carneiro, 28-Apr-2015.)
⊢ Rel 𝑅    ⇒   ⊢ (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴)
Theorem	relco 6061	A composition is a relation. Exercise 24 of [TakeutiZaring] p. 25. (Contributed by NM, 26-Jan-1997.)
⊢ Rel (𝐴 ∘ 𝐵)
Theorem	cotrg 6062*	Two ways of saying that the composition of two relations is included in a third relation. See its special instance cotr 6063 for the main application. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) Generalized from its special instance cotr 6063. (Revised by Richard Penner, 24-Dec-2019.) (Proof shortened by SN, 19-Dec-2024.) Avoid ax-11 2162. (Revised by BTernaryTau, 29-Dec-2024.)
⊢ ((𝐴 ∘ 𝐵) ⊆ 𝐶 ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))
Theorem	cotr 6063*	Two ways of saying a relation is transitive. Definition of transitivity in [Schechter] p. 51. Special instance of cotrg 6062. (Contributed by NM, 27-Dec-1996.)
⊢ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
Theorem	idrefALT 6064*	Alternate proof of idref 7085 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 6065*	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 2162. (Revised by BTernaryTau, 29-Dec-2024.)
⊢ (◡𝑅 ⊆ 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥))
Theorem	intasym 6066*	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 6067*	Two ways of saying a relation is antisymmetric and reflexive. ∪ ∪ 𝑅 is the field of a relation by relfld 6227. (Contributed by NM, 6-May-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ((𝑅 ∩ ◡𝑅) = ( I ↾ ∪ ∪ 𝑅) ↔ ∀𝑥 ∈ ∪ ∪ 𝑅∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) ↔ 𝑥 = 𝑦))
Theorem	asymref2 6068*	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 6069*	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 6070*	Two ways of saying that two elements have an upper bound. (Contributed by Mario Carneiro, 3-Nov-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴(◡𝑅 ∘ 𝑅)𝐵 ↔ ∃𝑧(𝐴𝑅𝑧 ∧ 𝐵𝑅𝑧)))
Theorem	codir 6071*	Two ways of saying a relation is directed. (Contributed by Mario Carneiro, 22-Nov-2013.)
⊢ ((𝐴 × 𝐵) ⊆ (◡𝑅 ∘ 𝑅) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∃𝑧(𝑥𝑅𝑧 ∧ 𝑦𝑅𝑧))
Theorem	qfto 6072*	A quantifier-free way of expressing the total order predicate. (Contributed by Mario Carneiro, 22-Nov-2013.)
⊢ ((𝐴 × 𝐵) ⊆ (𝑅 ∪ ◡𝑅) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑥))
Theorem	xpidtr 6073	A Cartesian square is a transitive relation. (Contributed by FL, 31-Jul-2009.)
⊢ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴)
Theorem	trin2 6074	The intersection of two transitive classes is transitive. (Contributed by FL, 31-Jul-2009.)
⊢ (((𝑅 ∘ 𝑅) ⊆ 𝑅 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ((𝑅 ∩ 𝑆) ∘ (𝑅 ∩ 𝑆)) ⊆ (𝑅 ∩ 𝑆))
Theorem	poirr2 6075	A partial order is irreflexive. (Contributed by Mario Carneiro, 2-Nov-2015.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ (𝑅 Po 𝐴 → (𝑅 ∩ ( I ↾ 𝐴)) = ∅)
Theorem	trinxp 6076	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 6077	A strict order relation is irreflexive. (Contributed by NM, 10-Feb-1996.) (Revised by Mario Carneiro, 10-May-2013.)
⊢ 𝑅 Or 𝑆    &   ⊢ 𝑅 ⊆ (𝑆 × 𝑆)    ⇒   ⊢ ¬ 𝐴𝑅𝐴
Theorem	sotri 6078	A strict order relation is a transitive relation. (Contributed by NM, 10-Feb-1996.) (Revised by Mario Carneiro, 10-May-2013.)
⊢ 𝑅 Or 𝑆    &   ⊢ 𝑅 ⊆ (𝑆 × 𝑆)    ⇒   ⊢ ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶)
Theorem	son2lpi 6079	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 6080	A transitivity relation. (Read 𝐴 ≤ 𝐵 and 𝐵 < 𝐶 implies 𝐴 < 𝐶.) (Contributed by Mario Carneiro, 10-May-2013.)
⊢ 𝑅 Or 𝑆    &   ⊢ 𝑅 ⊆ (𝑆 × 𝑆)    ⇒   ⊢ ((𝐴 ∈ 𝑆 ∧ ¬ 𝐵𝑅𝐴 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶)
Theorem	sotri3 6081	A transitivity relation. (Read 𝐴 < 𝐵 and 𝐵 ≤ 𝐶 implies 𝐴 < 𝐶.) (Contributed by Mario Carneiro, 10-May-2013.)
⊢ 𝑅 Or 𝑆    &   ⊢ 𝑅 ⊆ (𝑆 × 𝑆)    ⇒   ⊢ ((𝐶 ∈ 𝑆 ∧ 𝐴𝑅𝐵 ∧ ¬ 𝐶𝑅𝐵) → 𝐴𝑅𝐶)
Theorem	poleloe 6082	Express "less than or equals" for general strict orders. (Contributed by Stefan O'Rear, 17-Jan-2015.)
⊢ (𝐵 ∈ 𝑉 → (𝐴(𝑅 ∪ I )𝐵 ↔ (𝐴𝑅𝐵 ∨ 𝐴 = 𝐵)))
Theorem	poltletr 6083	Transitive law for general strict orders. (Contributed by Stefan O'Rear, 17-Jan-2015.)
⊢ ((𝑅 Po 𝑋 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝑅𝐵 ∧ 𝐵(𝑅 ∪ I )𝐶) → 𝐴𝑅𝐶))
Theorem	somin1 6084	Property of a minimum in a strict order. (Contributed by Stefan O'Rear, 17-Jan-2015.)
⊢ ((𝑅 Or 𝑋 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → if(𝐴𝑅𝐵, 𝐴, 𝐵)(𝑅 ∪ I )𝐴)
Theorem	somincom 6085	Commutativity of minimum in a total order. (Contributed by Stefan O'Rear, 17-Jan-2015.)
⊢ ((𝑅 Or 𝑋 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → if(𝐴𝑅𝐵, 𝐴, 𝐵) = if(𝐵𝑅𝐴, 𝐵, 𝐴))
Theorem	somin2 6086	Property of a minimum in a strict order. (Contributed by Stefan O'Rear, 17-Jan-2015.)
⊢ ((𝑅 Or 𝑋 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → if(𝐴𝑅𝐵, 𝐴, 𝐵)(𝑅 ∪ I )𝐵)
Theorem	soltmin 6087	Being less than a minimum, for a general total order. (Contributed by Stefan O'Rear, 17-Jan-2015.)
⊢ ((𝑅 Or 𝑋 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑅if(𝐵𝑅𝐶, 𝐵, 𝐶) ↔ (𝐴𝑅𝐵 ∧ 𝐴𝑅𝐶)))
Theorem	cnvopab 6088*	The converse of a class abstraction of ordered pairs. (Contributed by NM, 11-Dec-2003.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) Avoid ax-10 2146, ax-12 2182. (Revised by SN, 7-Jun-2025.)
⊢ ◡{⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑦, 𝑥⟩ ∣ 𝜑}
Theorem	cnvopabOLD 6089*	Obsolete version of cnvopab 6088 as of 7-Jun-2025. (Contributed by NM, 11-Dec-2003.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ◡{⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑦, 𝑥⟩ ∣ 𝜑}
Theorem	mptcnv 6090*	The converse of a mapping function. (Contributed by Thierry Arnoux, 16-Jan-2017.)
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑦 ∈ 𝐶 ∧ 𝑥 = 𝐷)))    ⇒   ⊢ (𝜑 → ◡(𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐶 ↦ 𝐷))
Theorem	cnv0 6091	The converse of the empty set. (Contributed by NM, 6-Apr-1998.) Remove dependency on ax-sep 5236, ax-nul 5246, ax-pr 5372. (Revised by KP, 25-Oct-2021.) Avoid ax-12 2182. (Revised by TM, 31-Jan-2026.)
⊢ ◡∅ = ∅
Theorem	cnv0OLD 6092	Obsolete version of cnv0 6091 as of 31-Jan-2026. (Contributed by NM, 6-Apr-1998.) Remove dependency on ax-sep 5236, ax-nul 5246, ax-pr 5372. (Revised by KP, 25-Oct-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ◡∅ = ∅
Theorem	cnvi 6093	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 6094	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.)
⊢ ◡(𝐴 ∪ 𝐵) = (◡𝐴 ∪ ◡𝐵)
Theorem	cnvdif 6095	Distributive law for converse over class difference. (Contributed by Mario Carneiro, 26-Jun-2014.)
⊢ ◡(𝐴 ∖ 𝐵) = (◡𝐴 ∖ ◡𝐵)
Theorem	cnvin 6096	Distributive law for converse over intersection. Theorem 15 of [Suppes] p. 62. (Contributed by NM, 25-Mar-1998.) (Revised by Mario Carneiro, 26-Jun-2014.)
⊢ ◡(𝐴 ∩ 𝐵) = (◡𝐴 ∩ ◡𝐵)
Theorem	rnun 6097	Distributive law for range over union. Theorem 8 of [Suppes] p. 60. (Contributed by NM, 24-Mar-1998.)
⊢ ran (𝐴 ∪ 𝐵) = (ran 𝐴 ∪ ran 𝐵)
Theorem	rnin 6098	The range of an intersection belongs the intersection of ranges. Theorem 9 of [Suppes] p. 60. (Contributed by NM, 15-Sep-2004.)
⊢ ran (𝐴 ∩ 𝐵) ⊆ (ran 𝐴 ∩ ran 𝐵)
Theorem	rniun 6099	The range of an indexed union. (Contributed by Mario Carneiro, 29-May-2015.)
⊢ ran ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 ran 𝐵
Theorem	rnuni 6100*	The range of a union. Part of Exercise 8 of [Enderton] p. 41. (Contributed by NM, 17-Mar-2004.) (Revised by Mario Carneiro, 29-May-2015.)
⊢ ran ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 ran 𝑥