P. 63 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 6201-6300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	op1sta 6201	Extract the first member of an ordered pair. (See op2nda 6204 to extract the second member, op1stb 5434 for an alternate version, and op1st 7979 for the preferred version.) (Contributed by Raph Levien, 4-Dec-2003.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ∪ dom {⟨𝐴, 𝐵⟩} = 𝐴
Theorem	cnvsn 6202	Converse of a singleton of an ordered pair. (Contributed by NM, 11-May-1998.) (Revised by Mario Carneiro, 26-Apr-2015.) (Proof shortened by BJ, 12-Feb-2022.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ◡{⟨𝐴, 𝐵⟩} = {⟨𝐵, 𝐴⟩}
Theorem	op2ndb 6203	Extract the second member of an ordered pair. Theorem 5.12(ii) of [Monk1] p. 52. (See op1stb 5434 to extract the first member, op2nda 6204 for an alternate version, and op2nd 7980 for the preferred version.) (Contributed by NM, 25-Nov-2003.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ∩ ∩ ∩ ◡{⟨𝐴, 𝐵⟩} = 𝐵
Theorem	op2nda 6204	Extract the second member of an ordered pair. (See op1sta 6201 to extract the first member, op2ndb 6203 for an alternate version, and op2nd 7980 for the preferred version.) (Contributed by NM, 17-Feb-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ∪ ran {⟨𝐴, 𝐵⟩} = 𝐵
Theorem	opswap 6205	Swap the members of an ordered pair. (Contributed by NM, 14-Dec-2008.) (Revised by Mario Carneiro, 30-Aug-2015.)
⊢ ∪ ◡{⟨𝐴, 𝐵⟩} = ⟨𝐵, 𝐴⟩
Theorem	cnvresima 6206	An image under the converse of a restriction. (Contributed by Jeff Hankins, 12-Jul-2009.)
⊢ (◡(𝐹 ↾ 𝐴) “ 𝐵) = ((◡𝐹 “ 𝐵) ∩ 𝐴)
Theorem	resdm2 6207	A class restricted to its domain equals its double converse. (Contributed by NM, 8-Apr-2007.)
⊢ (𝐴 ↾ dom 𝐴) = ◡◡𝐴
Theorem	resdmres 6208	Restriction to the domain of a restriction. (Contributed by NM, 8-Apr-2007.)
⊢ (𝐴 ↾ dom (𝐴 ↾ 𝐵)) = (𝐴 ↾ 𝐵)
Theorem	resresdm 6209	A restriction by an arbitrary set is a restriction by its domain. (Contributed by AV, 16-Nov-2020.)
⊢ (𝐹 = (𝐸 ↾ 𝐴) → 𝐹 = (𝐸 ↾ dom 𝐹))
Theorem	imadmres 6210	The image of the domain of a restriction. (Contributed by NM, 8-Apr-2007.)
⊢ (𝐴 “ dom (𝐴 ↾ 𝐵)) = (𝐴 “ 𝐵)
Theorem	resdmss 6211	Subset relationship for the domain of a restriction. (Contributed by Scott Fenton, 9-Aug-2024.)
⊢ dom (𝐴 ↾ 𝐵) ⊆ 𝐵
Theorem	resdifdi 6212	Distributive law for restriction over difference. (Contributed by BTernaryTau, 15-Aug-2024.)
⊢ (𝐴 ↾ (𝐵 ∖ 𝐶)) = ((𝐴 ↾ 𝐵) ∖ (𝐴 ↾ 𝐶))
Theorem	resdifdir 6213	Distributive law for restriction over difference. (Contributed by BTernaryTau, 15-Aug-2024.)
⊢ ((𝐴 ∖ 𝐵) ↾ 𝐶) = ((𝐴 ↾ 𝐶) ∖ (𝐵 ↾ 𝐶))
Theorem	mptpreima 6214*	The preimage of a function in maps-to notation. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (◡𝐹 “ 𝐶) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶}
Theorem	mptiniseg 6215*	Converse singleton image of a function defined by maps-to. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (𝐶 ∈ 𝑉 → (◡𝐹 “ {𝐶}) = {𝑥 ∈ 𝐴 ∣ 𝐵 = 𝐶})
Theorem	dmmpt 6216	The domain of the mapping operation in general. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 22-Mar-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ dom 𝐹 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V}
Theorem	dmmptss 6217*	The domain of a mapping is a subset of its base class. (Contributed by Scott Fenton, 17-Jun-2013.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ dom 𝐹 ⊆ 𝐴
Theorem	dmmptg 6218*	The domain of the mapping operation is the stated domain, if the function value is always a set. (Contributed by Mario Carneiro, 9-Feb-2013.) (Revised by Mario Carneiro, 14-Sep-2013.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴)
Theorem	rnmpt0f 6219*	The range of a function in maps-to notation is empty if and only if its domain is empty. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (𝜑 → (ran 𝐹 = ∅ ↔ 𝐴 = ∅))
Theorem	rnmptn0 6220*	The range of a function in maps-to notation is nonempty if the domain is nonempty. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    ⇒   ⊢ (𝜑 → ran 𝐹 ≠ ∅)
Theorem	dfco2 6221*	Alternate definition of a class composition, using only one bound variable. (Contributed by NM, 19-Dec-2008.)
⊢ (𝐴 ∘ 𝐵) = ∪ 𝑥 ∈ V ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥}))
Theorem	dfco2a 6222*	Generalization of dfco2 6221, where 𝐶 can have any value between dom 𝐴 ∩ ran 𝐵 and V. (Contributed by NM, 21-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ((dom 𝐴 ∩ ran 𝐵) ⊆ 𝐶 → (𝐴 ∘ 𝐵) = ∪ 𝑥 ∈ 𝐶 ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥})))
Theorem	coundi 6223	Class composition distributes over union. (Contributed by NM, 21-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (𝐴 ∘ (𝐵 ∪ 𝐶)) = ((𝐴 ∘ 𝐵) ∪ (𝐴 ∘ 𝐶))
Theorem	coundir 6224	Class composition distributes over union. (Contributed by NM, 21-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ((𝐴 ∪ 𝐵) ∘ 𝐶) = ((𝐴 ∘ 𝐶) ∪ (𝐵 ∘ 𝐶))
Theorem	cores 6225	Restricted first member of a class composition. (Contributed by NM, 12-Oct-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (ran 𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) ∘ 𝐵) = (𝐴 ∘ 𝐵))
Theorem	resco 6226	Associative law for the restriction of a composition. (Contributed by NM, 12-Dec-2006.)
⊢ ((𝐴 ∘ 𝐵) ↾ 𝐶) = (𝐴 ∘ (𝐵 ↾ 𝐶))
Theorem	imaco 6227	Image of the composition of two classes. (Contributed by Jason Orendorff, 12-Dec-2006.) (Proof shortened by Wolf Lammen, 16-May-2025.)
⊢ ((𝐴 ∘ 𝐵) “ 𝐶) = (𝐴 “ (𝐵 “ 𝐶))
Theorem	rnco 6228	The range of the composition of two classes. (Contributed by NM, 12-Dec-2006.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ ran (𝐴 ∘ 𝐵) = ran (𝐴 ↾ ran 𝐵)
Theorem	rnco2 6229	The range of the composition of two classes. (Contributed by NM, 27-Mar-2008.)
⊢ ran (𝐴 ∘ 𝐵) = (𝐴 “ ran 𝐵)
Theorem	dmco 6230	The domain of a composition. Exercise 27 of [Enderton] p. 53. (Contributed by NM, 4-Feb-2004.)
⊢ dom (𝐴 ∘ 𝐵) = (◡𝐵 “ dom 𝐴)
Theorem	coeq0 6231	A composition of two relations is empty iff there is no overlap between the range of the second and the domain of the first. Useful in combination with coundi 6223 and coundir 6224 to prune meaningless terms in the result. (Contributed by Stefan O'Rear, 8-Oct-2014.)
⊢ ((𝐴 ∘ 𝐵) = ∅ ↔ (dom 𝐴 ∩ ran 𝐵) = ∅)
Theorem	coiun 6232*	Composition with an indexed union. (Contributed by NM, 21-Dec-2008.)
⊢ (𝐴 ∘ ∪ 𝑥 ∈ 𝐶 𝐵) = ∪ 𝑥 ∈ 𝐶 (𝐴 ∘ 𝐵)
Theorem	cocnvcnv1 6233	A composition is not affected by a double converse of its first argument. (Contributed by NM, 8-Oct-2007.)
⊢ (◡◡𝐴 ∘ 𝐵) = (𝐴 ∘ 𝐵)
Theorem	cocnvcnv2 6234	A composition is not affected by a double converse of its second argument. (Contributed by NM, 8-Oct-2007.)
⊢ (𝐴 ∘ ◡◡𝐵) = (𝐴 ∘ 𝐵)
Theorem	cores2 6235	Absorption of a reverse (preimage) restriction of the second member of a class composition. (Contributed by NM, 11-Dec-2006.)
⊢ (dom 𝐴 ⊆ 𝐶 → (𝐴 ∘ ◡(◡𝐵 ↾ 𝐶)) = (𝐴 ∘ 𝐵))
Theorem	co02 6236	Composition with the empty set. Theorem 20 of [Suppes] p. 63. (Contributed by NM, 24-Apr-2004.)
⊢ (𝐴 ∘ ∅) = ∅
Theorem	co01 6237	Composition with the empty set. (Contributed by NM, 24-Apr-2004.)
⊢ (∅ ∘ 𝐴) = ∅
Theorem	coi1 6238	Composition with the identity relation. Part of Theorem 3.7(i) of [Monk1] p. 36. (Contributed by NM, 22-Apr-2004.)
⊢ (Rel 𝐴 → (𝐴 ∘ I ) = 𝐴)
Theorem	coi2 6239	Composition with the identity relation. Part of Theorem 3.7(i) of [Monk1] p. 36. (Contributed by NM, 22-Apr-2004.)
⊢ (Rel 𝐴 → ( I ∘ 𝐴) = 𝐴)
Theorem	coires1 6240	Composition with a restricted identity relation. (Contributed by FL, 19-Jun-2011.) (Revised by Stefan O'Rear, 7-Mar-2015.)
⊢ (𝐴 ∘ ( I ↾ 𝐵)) = (𝐴 ↾ 𝐵)
Theorem	coass 6241	Associative law for class composition. Theorem 27 of [Suppes] p. 64. Also Exercise 21 of [Enderton] p. 53. Interestingly, this law holds for any classes whatsoever, not just functions or even relations. (Contributed by NM, 27-Jan-1997.)
⊢ ((𝐴 ∘ 𝐵) ∘ 𝐶) = (𝐴 ∘ (𝐵 ∘ 𝐶))
Theorem	relcnvtrg 6242	General form of relcnvtr 6243. (Contributed by Peter Mazsa, 17-Oct-2023.)
⊢ ((Rel 𝑅 ∧ Rel 𝑆 ∧ Rel 𝑇) → ((𝑅 ∘ 𝑆) ⊆ 𝑇 ↔ (◡𝑆 ∘ ◡𝑅) ⊆ ◡𝑇))
Theorem	relcnvtr 6243	A relation is transitive iff its converse is transitive. (Contributed by FL, 19-Sep-2011.) (Proof shortened by Peter Mazsa, 17-Oct-2023.)
⊢ (Rel 𝑅 → ((𝑅 ∘ 𝑅) ⊆ 𝑅 ↔ (◡𝑅 ∘ ◡𝑅) ⊆ ◡𝑅))
Theorem	relssdmrn 6244	A relation is included in the Cartesian product of its domain and range. Exercise 4.12(t) of [Mendelson] p. 235. (Contributed by NM, 3-Aug-1994.) (Proof shortened by SN, 23-Dec-2024.)
⊢ (Rel 𝐴 → 𝐴 ⊆ (dom 𝐴 × ran 𝐴))
Theorem	relssdmrnOLD 6245	Obsolete version of relssdmrn 6244 as of 23-Dec-2024. (Contributed by NM, 3-Aug-1994.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (Rel 𝐴 → 𝐴 ⊆ (dom 𝐴 × ran 𝐴))
Theorem	resssxp 6246	If the 𝑅-image of a class 𝐴 is a subclass of 𝐵, then the restriction of 𝑅 to 𝐴 is a subset of the Cartesian product of 𝐴 and 𝐵. (Contributed by RP, 24-Dec-2019.)
⊢ ((𝑅 “ 𝐴) ⊆ 𝐵 ↔ (𝑅 ↾ 𝐴) ⊆ (𝐴 × 𝐵))
Theorem	cnvssrndm 6247	The converse is a subset of the cartesian product of range and domain. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ ◡𝐴 ⊆ (ran 𝐴 × dom 𝐴)
Theorem	cossxp 6248	Composition as a subset of the Cartesian product of factors. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ (𝐴 ∘ 𝐵) ⊆ (dom 𝐵 × ran 𝐴)
Theorem	relrelss 6249	Two ways to describe the structure of a two-place operation. (Contributed by NM, 17-Dec-2008.)
⊢ ((Rel 𝐴 ∧ Rel dom 𝐴) ↔ 𝐴 ⊆ ((V × V) × V))
Theorem	unielrel 6250	The membership relation for a relation is inherited by class union. (Contributed by NM, 17-Sep-2006.)
⊢ ((Rel 𝑅 ∧ 𝐴 ∈ 𝑅) → ∪ 𝐴 ∈ ∪ 𝑅)
Theorem	relfld 6251	The double union of a relation is its field. (Contributed by NM, 17-Sep-2006.)
⊢ (Rel 𝑅 → ∪ ∪ 𝑅 = (dom 𝑅 ∪ ran 𝑅))
Theorem	relresfld 6252	Restriction of a relation to its field. (Contributed by FL, 15-Apr-2012.)
⊢ (Rel 𝑅 → (𝑅 ↾ ∪ ∪ 𝑅) = 𝑅)
Theorem	relcoi2 6253	Composition with the identity relation restricted to a relation's field. (Contributed by FL, 2-May-2011.)
⊢ (Rel 𝑅 → (( I ↾ ∪ ∪ 𝑅) ∘ 𝑅) = 𝑅)
Theorem	relcoi1 6254	Composition with the identity relation restricted to a relation's field. (Contributed by FL, 8-May-2011.) (Proof shortened by OpenAI, 3-Jul-2020.)
⊢ (Rel 𝑅 → (𝑅 ∘ ( I ↾ ∪ ∪ 𝑅)) = 𝑅)
Theorem	unidmrn 6255	The double union of the converse of a class is its field. (Contributed by NM, 4-Jun-2008.)
⊢ ∪ ∪ ◡𝐴 = (dom 𝐴 ∪ ran 𝐴)
Theorem	relcnvfld 6256	if 𝑅 is a relation, its double union equals the double union of its converse. (Contributed by FL, 5-Jan-2009.)
⊢ (Rel 𝑅 → ∪ ∪ 𝑅 = ∪ ∪ ◡𝑅)
Theorem	dfdm2 6257	Alternate definition of domain df-dm 5651 that doesn't require dummy variables. (Contributed by NM, 2-Aug-2010.)
⊢ dom 𝐴 = ∪ ∪ (◡𝐴 ∘ 𝐴)
Theorem	unixp 6258	The double class union of a nonempty Cartesian product is the union of it members. (Contributed by NM, 17-Sep-2006.)
⊢ ((𝐴 × 𝐵) ≠ ∅ → ∪ ∪ (𝐴 × 𝐵) = (𝐴 ∪ 𝐵))
Theorem	unixp0 6259	A Cartesian product is empty iff its union is empty. (Contributed by NM, 20-Sep-2006.)
⊢ ((𝐴 × 𝐵) = ∅ ↔ ∪ (𝐴 × 𝐵) = ∅)
Theorem	unixpid 6260	Field of a Cartesian square. (Contributed by FL, 10-Oct-2009.)
⊢ ∪ ∪ (𝐴 × 𝐴) = 𝐴
Theorem	ressn 6261	Restriction of a class to a singleton. (Contributed by Mario Carneiro, 28-Dec-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ (𝐴 ↾ {𝐵}) = ({𝐵} × (𝐴 “ {𝐵}))
Theorem	cnviin 6262*	The converse of an intersection is the intersection of the converse. (Contributed by FL, 15-Oct-2012.)
⊢ (𝐴 ≠ ∅ → ◡∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑥 ∈ 𝐴 ◡𝐵)
Theorem	cnvpo 6263	The converse of a partial order is a partial order. (Contributed by NM, 15-Jun-2005.)
⊢ (𝑅 Po 𝐴 ↔ ◡𝑅 Po 𝐴)
Theorem	cnvso 6264	The converse of a strict order relation is a strict order relation. (Contributed by NM, 15-Jun-2005.)
⊢ (𝑅 Or 𝐴 ↔ ◡𝑅 Or 𝐴)
Theorem	xpco 6265	Composition of two Cartesian products. (Contributed by Thierry Arnoux, 17-Nov-2017.)
⊢ (𝐵 ≠ ∅ → ((𝐵 × 𝐶) ∘ (𝐴 × 𝐵)) = (𝐴 × 𝐶))
Theorem	xpcoid 6266	Composition of two Cartesian squares. (Contributed by Thierry Arnoux, 14-Jan-2018.)
⊢ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴)) = (𝐴 × 𝐴)
Theorem	elsnxp 6267*	Membership in a Cartesian product with a singleton. (Contributed by Thierry Arnoux, 10-Apr-2020.) (Proof shortened by JJ, 14-Jul-2021.)
⊢ (𝑋 ∈ 𝑉 → (𝑍 ∈ ({𝑋} × 𝐴) ↔ ∃𝑦 ∈ 𝐴 𝑍 = ⟨𝑋, 𝑦⟩))
Theorem	reu3op 6268*	There is a unique ordered pair fulfilling a wff iff there are uniquely two sets fulfilling a corresponding wff. (Contributed by AV, 1-Jul-2023.)
⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜓 ↔ 𝜒))    ⇒   ⊢ (∃!𝑝 ∈ (𝑋 × 𝑌)𝜓 ↔ (∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 𝜒 ∧ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑌 (𝜒 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))
Theorem	reuop 6269*	There is a unique ordered pair fulfilling a wff iff there are uniquely two sets fulfilling a corresponding wff. (Contributed by AV, 23-Jun-2023.)
⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜓 ↔ 𝜒))    &   ⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → (𝜓 ↔ 𝜃))    ⇒   ⊢ (∃!𝑝 ∈ (𝑋 × 𝑌)𝜓 ↔ ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))
Theorem	opreu2reurex 6270*	There is a unique ordered pair fulfilling a wff iff there are uniquely two sets fulfilling a corresponding wff. (Contributed by AV, 24-Jun-2023.) (Revised by AV, 1-Jul-2023.)
⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜑 ↔ 𝜒))    ⇒   ⊢ (∃!𝑝 ∈ (𝐴 × 𝐵)𝜑 ↔ (∃!𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ ∃!𝑏 ∈ 𝐵 ∃𝑎 ∈ 𝐴 𝜒))
Theorem	opreu2reu 6271*	If there is a unique ordered pair fulfilling a wff, then there is a double restricted unique existential qualification fulfilling a corresponding wff. (Contributed by AV, 25-Jun-2023.) (Revised by AV, 2-Jul-2023.)
⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜑 ↔ 𝜒))    ⇒   ⊢ (∃!𝑝 ∈ (𝐴 × 𝐵)𝜑 → ∃!𝑎 ∈ 𝐴 ∃!𝑏 ∈ 𝐵 𝜒)
Theorem	dfpo2 6272	Quantifier-free definition of a partial ordering. (Contributed by Scott Fenton, 22-Feb-2013.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ (𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅))
Theorem	csbcog 6273	Distribute proper substitution through a composition of relations. (Contributed by RP, 28-Jun-2020.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵 ∘ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∘ ⦋𝐴 / 𝑥⦌𝐶))
Theorem	snres0 6274	Condition for restriction of a singleton to be empty. (Contributed by Scott Fenton, 9-Aug-2024.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (({⟨𝐴, 𝐵⟩} ↾ 𝐶) = ∅ ↔ ¬ 𝐴 ∈ 𝐶)
Theorem	imaindm 6275	The image is unaffected by intersection with the domain. (Contributed by Scott Fenton, 17-Dec-2021.)
⊢ (𝑅 “ 𝐴) = (𝑅 “ (𝐴 ∩ dom 𝑅))
2.3.11  The Predecessor Class
Syntax	cpred 6276	The predecessors symbol.
class Pred(𝑅, 𝐴, 𝑋)
Definition	df-pred 6277	Define the predecessor class of a binary relation. This is the class of all elements 𝑦 of 𝐴 such that 𝑦𝑅𝑋 (see elpred 6294). (Contributed by Scott Fenton, 29-Jan-2011.)
⊢ Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (◡𝑅 “ {𝑋}))
Theorem	predeq123 6278	Equality theorem for the predecessor class. (Contributed by Scott Fenton, 13-Jun-2018.)
⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝑋 = 𝑌) → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑆, 𝐵, 𝑌))
Theorem	predeq1 6279	Equality theorem for the predecessor class. (Contributed by Scott Fenton, 2-Feb-2011.)
⊢ (𝑅 = 𝑆 → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑆, 𝐴, 𝑋))
Theorem	predeq2 6280	Equality theorem for the predecessor class. (Contributed by Scott Fenton, 2-Feb-2011.)
⊢ (𝐴 = 𝐵 → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐵, 𝑋))
Theorem	predeq3 6281	Equality theorem for the predecessor class. (Contributed by Scott Fenton, 2-Feb-2011.)
⊢ (𝑋 = 𝑌 → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐴, 𝑌))
Theorem	nfpred 6282	Bound-variable hypothesis builder for the predecessor class. (Contributed by Scott Fenton, 9-Jun-2018.)
⊢ Ⅎ𝑥𝑅    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝑋    ⇒   ⊢ Ⅎ𝑥Pred(𝑅, 𝐴, 𝑋)
Theorem	csbpredg 6283	Move class substitution in and out of the predecessor class of a relation. (Contributed by ML, 25-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌Pred(𝑅, 𝐷, 𝑋) = Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, ⦋𝐴 / 𝑥⦌𝑋))
Theorem	predpredss 6284	If 𝐴 is a subset of 𝐵, then their predecessor classes are also subsets. (Contributed by Scott Fenton, 2-Feb-2011.)
⊢ (𝐴 ⊆ 𝐵 → Pred(𝑅, 𝐴, 𝑋) ⊆ Pred(𝑅, 𝐵, 𝑋))
Theorem	predss 6285	The predecessor class of 𝐴 is a subset of 𝐴. (Contributed by Scott Fenton, 2-Feb-2011.)
⊢ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐴
Theorem	sspred 6286	Another subset/predecessor class relationship. (Contributed by Scott Fenton, 6-Feb-2011.)
⊢ ((𝐵 ⊆ 𝐴 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵) → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐵, 𝑋))
Theorem	dfpred2 6287*	An alternate definition of predecessor class when 𝑋 is a set. (Contributed by Scott Fenton, 8-Feb-2011.)
⊢ 𝑋 ∈ V    ⇒   ⊢ Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ {𝑦 ∣ 𝑦𝑅𝑋})
Theorem	dfpred3 6288*	An alternate definition of predecessor class when 𝑋 is a set. (Contributed by Scott Fenton, 13-Jun-2018.)
⊢ 𝑋 ∈ V    ⇒   ⊢ Pred(𝑅, 𝐴, 𝑋) = {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑋}
Theorem	dfpred3g 6289*	An alternate definition of predecessor class when 𝑋 is a set. (Contributed by Scott Fenton, 13-Jun-2018.)
⊢ (𝑋 ∈ 𝑉 → Pred(𝑅, 𝐴, 𝑋) = {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑋})
Theorem	elpredgg 6290	Membership in a predecessor class. (Contributed by Scott Fenton, 17-Apr-2011.) Generalize to closed form. (Revised by BJ, 16-Oct-2024.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ↔ (𝑌 ∈ 𝐴 ∧ 𝑌𝑅𝑋)))
Theorem	elpredg 6291	Membership in a predecessor class. (Contributed by Scott Fenton, 17-Apr-2011.) (Proof shortened by BJ, 16-Oct-2024.)
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐴) → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ↔ 𝑌𝑅𝑋))
Theorem	elpredimg 6292	Membership in a predecessor class - implicative version. (Contributed by Scott Fenton, 13-Apr-2011.) (Revised by NM, 5-Apr-2016.) (Proof shortened by BJ, 16-Oct-2024.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋)) → 𝑌𝑅𝑋)
Theorem	elpredim 6293	Membership in a predecessor class - implicative version. (Contributed by Scott Fenton, 9-May-2012.) (Proof shortened by BJ, 16-Oct-2024.)
⊢ 𝑋 ∈ V    ⇒   ⊢ (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) → 𝑌𝑅𝑋)
Theorem	elpred 6294	Membership in a predecessor class. (Contributed by Scott Fenton, 4-Feb-2011.) (Proof shortened by BJ, 16-Oct-2024.)
⊢ 𝑌 ∈ V    ⇒   ⊢ (𝑋 ∈ 𝐷 → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ↔ (𝑌 ∈ 𝐴 ∧ 𝑌𝑅𝑋)))
Theorem	predexg 6295	The predecessor class exists when 𝐴 does. (Contributed by Scott Fenton, 8-Feb-2011.) Generalize to closed form. (Revised by BJ, 27-Oct-2024.)
⊢ (𝐴 ∈ 𝑉 → Pred(𝑅, 𝐴, 𝑋) ∈ V)
Theorem	dffr4 6296*	Alternate definition of well-founded relation. (Contributed by Scott Fenton, 2-Feb-2011.)
⊢ (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 Pred(𝑅, 𝑥, 𝑦) = ∅))
Theorem	predel 6297	Membership in the predecessor class implies membership in the base class. (Contributed by Scott Fenton, 11-Feb-2011.)
⊢ (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) → 𝑌 ∈ 𝐴)
Theorem	predtrss 6298	If 𝑅 is transitive over 𝐴 and 𝑌𝑅𝑋, then Pred(𝑅, 𝐴, 𝑌) is a subclass of Pred(𝑅, 𝐴, 𝑋). (Contributed by Scott Fenton, 28-Oct-2024.)
⊢ ((((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∧ 𝑋 ∈ 𝐴) → Pred(𝑅, 𝐴, 𝑌) ⊆ Pred(𝑅, 𝐴, 𝑋))
Theorem	predpo 6299	Property of the predecessor class for partial orders. (Contributed by Scott Fenton, 28-Apr-2012.) (Proof shortened by Scott Fenton, 28-Oct-2024.)
⊢ ((𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) → Pred(𝑅, 𝐴, 𝑌) ⊆ Pred(𝑅, 𝐴, 𝑋)))
Theorem	predso 6300	Property of the predecessor class for strict total orders. (Contributed by Scott Fenton, 11-Feb-2011.)
⊢ ((𝑅 Or 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) → Pred(𝑅, 𝐴, 𝑌) ⊆ Pred(𝑅, 𝐴, 𝑋)))