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	dmtpop 6201	The domain of an unordered triple of ordered pairs. (Contributed by NM, 14-Sep-2011.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐷 ∈ V    &   ⊢ 𝐹 ∈ V    ⇒   ⊢ dom {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩, ⟨𝐸, 𝐹⟩} = {𝐴, 𝐶, 𝐸}
Theorem	cnvcnvsn 6202	Double converse of a singleton of an ordered pair. (Unlike cnvsn 6209, this does not need any sethood assumptions on 𝐴 and 𝐵.) (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ ◡◡{⟨𝐴, 𝐵⟩} = ◡{⟨𝐵, 𝐴⟩}
Theorem	dmsnsnsn 6203	The domain of the singleton of the singleton of a singleton. (Contributed by NM, 15-Sep-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ dom {{{𝐴}}} = {𝐴}
Theorem	rnsnopg 6204	The range of a singleton of an ordered pair is the singleton of the second member. (Contributed by NM, 24-Jul-2004.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ (𝐴 ∈ 𝑉 → ran {⟨𝐴, 𝐵⟩} = {𝐵})
Theorem	rnpropg 6205	The range of a pair of ordered pairs is the pair of second members. (Contributed by Thierry Arnoux, 3-Jan-2017.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ran {⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩} = {𝐶, 𝐷})
Theorem	cnvsng 6206	Converse of a singleton of an ordered pair. (Contributed by NM, 23-Jan-2015.) (Proof shortened by BJ, 12-Feb-2022.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ◡{⟨𝐴, 𝐵⟩} = {⟨𝐵, 𝐴⟩})
Theorem	rnsnop 6207	The range of a singleton of an ordered pair is the singleton of the second member. (Contributed by NM, 24-Jul-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ran {⟨𝐴, 𝐵⟩} = {𝐵}
Theorem	op1sta 6208	Extract the first member of an ordered pair. (See op2nda 6211 to extract the second member, op1stb 5438 for an alternate version, and op1st 7974 for the preferred version.) (Contributed by Raph Levien, 4-Dec-2003.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ∪ dom {⟨𝐴, 𝐵⟩} = 𝐴
Theorem	cnvsn 6209	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 6210	Extract the second member of an ordered pair. Theorem 5.12(ii) of [Monk1] p. 52. (See op1stb 5438 to extract the first member, op2nda 6211 for an alternate version, and op2nd 7975 for the preferred version.) (Contributed by NM, 25-Nov-2003.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ∩ ∩ ∩ ◡{⟨𝐴, 𝐵⟩} = 𝐵
Theorem	op2nda 6211	Extract the second member of an ordered pair. (See op1sta 6208 to extract the first member, op2ndb 6210 for an alternate version, and op2nd 7975 for the preferred version.) (Contributed by NM, 17-Feb-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ∪ ran {⟨𝐴, 𝐵⟩} = 𝐵
Theorem	opswap 6212	Swap the members of an ordered pair. (Contributed by NM, 14-Dec-2008.) (Revised by Mario Carneiro, 30-Aug-2015.)
⊢ ∪ ◡{⟨𝐴, 𝐵⟩} = ⟨𝐵, 𝐴⟩
Theorem	cnvresima 6213	An image under the converse of a restriction. (Contributed by Jeff Hankins, 12-Jul-2009.)
⊢ (◡(𝐹 ↾ 𝐴) “ 𝐵) = ((◡𝐹 “ 𝐵) ∩ 𝐴)
Theorem	resdm2 6214	A class restricted to its domain equals its double converse. (Contributed by NM, 8-Apr-2007.)
⊢ (𝐴 ↾ dom 𝐴) = ◡◡𝐴
Theorem	resdmres 6215	Restriction to the domain of a restriction. (Contributed by NM, 8-Apr-2007.)
⊢ (𝐴 ↾ dom (𝐴 ↾ 𝐵)) = (𝐴 ↾ 𝐵)
Theorem	resresdm 6216	A restriction by an arbitrary set is a restriction by its domain. (Contributed by AV, 16-Nov-2020.)
⊢ (𝐹 = (𝐸 ↾ 𝐴) → 𝐹 = (𝐸 ↾ dom 𝐹))
Theorem	imadmres 6217	The image of the domain of a restriction. (Contributed by NM, 8-Apr-2007.)
⊢ (𝐴 “ dom (𝐴 ↾ 𝐵)) = (𝐴 “ 𝐵)
Theorem	resdmss 6218	Subset relationship for the domain of a restriction. (Contributed by Scott Fenton, 9-Aug-2024.)
⊢ dom (𝐴 ↾ 𝐵) ⊆ 𝐵
Theorem	resdifdi 6219	Distributive law for restriction over difference. (Contributed by BTernaryTau, 15-Aug-2024.)
⊢ (𝐴 ↾ (𝐵 ∖ 𝐶)) = ((𝐴 ↾ 𝐵) ∖ (𝐴 ↾ 𝐶))
Theorem	resdifdir 6220	Distributive law for restriction over difference. (Contributed by BTernaryTau, 15-Aug-2024.)
⊢ ((𝐴 ∖ 𝐵) ↾ 𝐶) = ((𝐴 ↾ 𝐶) ∖ (𝐵 ↾ 𝐶))
Theorem	mptpreima 6221*	The preimage of a function in maps-to notation. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (◡𝐹 “ 𝐶) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶}
Theorem	mptiniseg 6222*	Converse singleton image of a function defined by maps-to. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (𝐶 ∈ 𝑉 → (◡𝐹 “ {𝐶}) = {𝑥 ∈ 𝐴 ∣ 𝐵 = 𝐶})
Theorem	dmmpt 6223	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 6224*	The domain of a mapping is a subset of its base class. (Contributed by Scott Fenton, 17-Jun-2013.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ dom 𝐹 ⊆ 𝐴
Theorem	dmmptg 6225*	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 6226*	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 6227*	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 6228*	Alternate definition of a class composition, using only one bound variable. (Contributed by NM, 19-Dec-2008.)
⊢ (𝐴 ∘ 𝐵) = ∪ 𝑥 ∈ V ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥}))
Theorem	dfco2a 6229*	Generalization of dfco2 6228, 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 6230	Class composition distributes over union. (Contributed by NM, 21-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (𝐴 ∘ (𝐵 ∪ 𝐶)) = ((𝐴 ∘ 𝐵) ∪ (𝐴 ∘ 𝐶))
Theorem	coundir 6231	Class composition distributes over union. (Contributed by NM, 21-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ((𝐴 ∪ 𝐵) ∘ 𝐶) = ((𝐴 ∘ 𝐶) ∪ (𝐵 ∘ 𝐶))
Theorem	cores 6232	Restricted first member of a class composition. (Contributed by NM, 12-Oct-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (ran 𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) ∘ 𝐵) = (𝐴 ∘ 𝐵))
Theorem	resco 6233	Associative law for the restriction of a composition. (Contributed by NM, 12-Dec-2006.)
⊢ ((𝐴 ∘ 𝐵) ↾ 𝐶) = (𝐴 ∘ (𝐵 ↾ 𝐶))
Theorem	imaco 6234	Image of the composition of two classes. (Contributed by Jason Orendorff, 12-Dec-2006.) (Proof shortened by Wolf Lammen, 16-May-2025.)
⊢ ((𝐴 ∘ 𝐵) “ 𝐶) = (𝐴 “ (𝐵 “ 𝐶))
Theorem	rnco 6235	The range of the composition of two classes. (Contributed by NM, 12-Dec-2006.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) Avoid ax-11 2190. (Revised by TM, 24-Jan-2026.)
⊢ ran (𝐴 ∘ 𝐵) = ran (𝐴 ↾ ran 𝐵)
Theorem	rncoOLD 6236	Obsolete version of rnco 6235 as of 24-Jan-2026. (Contributed by NM, 12-Dec-2006.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ran (𝐴 ∘ 𝐵) = ran (𝐴 ↾ ran 𝐵)
Theorem	rnco2 6237	The range of the composition of two classes. (Contributed by NM, 27-Mar-2008.)
⊢ ran (𝐴 ∘ 𝐵) = (𝐴 “ ran 𝐵)
Theorem	dmco 6238	The domain of a composition. Exercise 27 of [Enderton] p. 53. (Contributed by NM, 4-Feb-2004.)
⊢ dom (𝐴 ∘ 𝐵) = (◡𝐵 “ dom 𝐴)
Theorem	coeq0 6239	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 6230 and coundir 6231 to prune meaningless terms in the result. (Contributed by Stefan O'Rear, 8-Oct-2014.)
⊢ ((𝐴 ∘ 𝐵) = ∅ ↔ (dom 𝐴 ∩ ran 𝐵) = ∅)
Theorem	coiun 6240*	Composition with an indexed union. (Contributed by NM, 21-Dec-2008.)
⊢ (𝐴 ∘ ∪ 𝑥 ∈ 𝐶 𝐵) = ∪ 𝑥 ∈ 𝐶 (𝐴 ∘ 𝐵)
Theorem	cocnvcnv1 6241	A composition is not affected by a double converse of its first argument. (Contributed by NM, 8-Oct-2007.)
⊢ (◡◡𝐴 ∘ 𝐵) = (𝐴 ∘ 𝐵)
Theorem	cocnvcnv2 6242	A composition is not affected by a double converse of its second argument. (Contributed by NM, 8-Oct-2007.)
⊢ (𝐴 ∘ ◡◡𝐵) = (𝐴 ∘ 𝐵)
Theorem	cores2 6243	Absorption of a reverse (preimage) restriction of the second member of a class composition. (Contributed by NM, 11-Dec-2006.)
⊢ (dom 𝐴 ⊆ 𝐶 → (𝐴 ∘ ◡(◡𝐵 ↾ 𝐶)) = (𝐴 ∘ 𝐵))
Theorem	co02 6244	Composition with the empty set. Theorem 20 of [Suppes] p. 63. (Contributed by NM, 24-Apr-2004.)
⊢ (𝐴 ∘ ∅) = ∅
Theorem	co01 6245	Composition with the empty set. (Contributed by NM, 24-Apr-2004.)
⊢ (∅ ∘ 𝐴) = ∅
Theorem	coi1 6246	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 6247	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 6248	Composition with a restricted identity relation. (Contributed by FL, 19-Jun-2011.) (Revised by Stefan O'Rear, 7-Mar-2015.)
⊢ (𝐴 ∘ ( I ↾ 𝐵)) = (𝐴 ↾ 𝐵)
Theorem	coass 6249	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 6250	General form of relcnvtr 6251. (Contributed by Peter Mazsa, 17-Oct-2023.)
⊢ ((Rel 𝑅 ∧ Rel 𝑆 ∧ Rel 𝑇) → ((𝑅 ∘ 𝑆) ⊆ 𝑇 ↔ (◡𝑆 ∘ ◡𝑅) ⊆ ◡𝑇))
Theorem	relcnvtr 6251	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 6252	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	resssxp 6253	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 6254	The converse is a subset of the cartesian product of range and domain. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ ◡𝐴 ⊆ (ran 𝐴 × dom 𝐴)
Theorem	cossxp 6255	Composition as a subset of the Cartesian product of factors. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ (𝐴 ∘ 𝐵) ⊆ (dom 𝐵 × ran 𝐴)
Theorem	relrelss 6256	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 6257	The membership relation for a relation is inherited by class union. (Contributed by NM, 17-Sep-2006.)
⊢ ((Rel 𝑅 ∧ 𝐴 ∈ 𝑅) → ∪ 𝐴 ∈ ∪ 𝑅)
Theorem	relfld 6258	The double union of a relation is its field. (Contributed by NM, 17-Sep-2006.)
⊢ (Rel 𝑅 → ∪ ∪ 𝑅 = (dom 𝑅 ∪ ran 𝑅))
Theorem	relresfld 6259	Restriction of a relation to its field. (Contributed by FL, 15-Apr-2012.)
⊢ (Rel 𝑅 → (𝑅 ↾ ∪ ∪ 𝑅) = 𝑅)
Theorem	relcoi2 6260	Composition with the identity relation restricted to a relation's field. (Contributed by FL, 2-May-2011.)
⊢ (Rel 𝑅 → (( I ↾ ∪ ∪ 𝑅) ∘ 𝑅) = 𝑅)
Theorem	relcoi1 6261	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 6262	The double union of the converse of a class is its field. (Contributed by NM, 4-Jun-2008.)
⊢ ∪ ∪ ◡𝐴 = (dom 𝐴 ∪ ran 𝐴)
Theorem	relcnvfld 6263	if 𝑅 is a relation, its double union equals the double union of its converse. (Contributed by FL, 5-Jan-2009.)
⊢ (Rel 𝑅 → ∪ ∪ 𝑅 = ∪ ∪ ◡𝑅)
Theorem	dfdm2 6264	Alternate definition of domain df-dm 5655 that doesn't require dummy variables. (Contributed by NM, 2-Aug-2010.)
⊢ dom 𝐴 = ∪ ∪ (◡𝐴 ∘ 𝐴)
Theorem	unixp 6265	The double class union of a nonempty Cartesian product is the union of it members. (Contributed by NM, 17-Sep-2006.)
⊢ ((𝐴 × 𝐵) ≠ ∅ → ∪ ∪ (𝐴 × 𝐵) = (𝐴 ∪ 𝐵))
Theorem	unixp0 6266	A Cartesian product is empty iff its union is empty. (Contributed by NM, 20-Sep-2006.)
⊢ ((𝐴 × 𝐵) = ∅ ↔ ∪ (𝐴 × 𝐵) = ∅)
Theorem	unixpid 6267	Field of a Cartesian square. (Contributed by FL, 10-Oct-2009.)
⊢ ∪ ∪ (𝐴 × 𝐴) = 𝐴
Theorem	ressn 6268	Restriction of a class to a singleton. (Contributed by Mario Carneiro, 28-Dec-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ (𝐴 ↾ {𝐵}) = ({𝐵} × (𝐴 “ {𝐵}))
Theorem	cnviin 6269*	The converse of an intersection is the intersection of the converse. (Contributed by FL, 15-Oct-2012.)
⊢ (𝐴 ≠ ∅ → ◡∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑥 ∈ 𝐴 ◡𝐵)
Theorem	cnvpo 6270	The converse of a partial order is a partial order. (Contributed by NM, 15-Jun-2005.)
⊢ (𝑅 Po 𝐴 ↔ ◡𝑅 Po 𝐴)
Theorem	cnvso 6271	The converse of a strict order relation is a strict order relation. (Contributed by NM, 15-Jun-2005.)
⊢ (𝑅 Or 𝐴 ↔ ◡𝑅 Or 𝐴)
Theorem	xpco 6272	Composition of two Cartesian products. (Contributed by Thierry Arnoux, 17-Nov-2017.)
⊢ (𝐵 ≠ ∅ → ((𝐵 × 𝐶) ∘ (𝐴 × 𝐵)) = (𝐴 × 𝐶))
Theorem	xpcoid 6273	Composition of two Cartesian squares. (Contributed by Thierry Arnoux, 14-Jan-2018.)
⊢ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴)) = (𝐴 × 𝐴)
Theorem	elsnxp 6274*	Membership in a Cartesian product with a singleton. (Contributed by Thierry Arnoux, 10-Apr-2020.) (Proof shortened by JJ, 14-Jul-2021.)
⊢ (𝑋 ∈ 𝑉 → (𝑍 ∈ ({𝑋} × 𝐴) ↔ ∃𝑦 ∈ 𝐴 𝑍 = ⟨𝑋, 𝑦⟩))
Theorem	reu3op 6275*	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 6276*	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 6277*	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 6278*	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 6279	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 6280	Distribute proper substitution through a composition of relations. (Contributed by RP, 28-Jun-2020.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵 ∘ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∘ ⦋𝐴 / 𝑥⦌𝐶))
Theorem	snres0 6281	Condition for restriction of a singleton to be empty. (Contributed by Scott Fenton, 9-Aug-2024.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (({⟨𝐴, 𝐵⟩} ↾ 𝐶) = ∅ ↔ ¬ 𝐴 ∈ 𝐶)
Theorem	imaindm 6282	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 6283	The predecessors symbol.
class Pred(𝑅, 𝐴, 𝑋)
Definition	df-pred 6284	Define the predecessor class of a binary relation. This is the class of all elements 𝑦 of 𝐴 such that 𝑦𝑅𝑋 (see elpred 6301). (Contributed by Scott Fenton, 29-Jan-2011.)
⊢ Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (◡𝑅 “ {𝑋}))
Theorem	predeq123 6285	Equality theorem for the predecessor class. (Contributed by Scott Fenton, 13-Jun-2018.)
⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝑋 = 𝑌) → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑆, 𝐵, 𝑌))
Theorem	predeq1 6286	Equality theorem for the predecessor class. (Contributed by Scott Fenton, 2-Feb-2011.)
⊢ (𝑅 = 𝑆 → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑆, 𝐴, 𝑋))
Theorem	predeq2 6287	Equality theorem for the predecessor class. (Contributed by Scott Fenton, 2-Feb-2011.)
⊢ (𝐴 = 𝐵 → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐵, 𝑋))
Theorem	predeq3 6288	Equality theorem for the predecessor class. (Contributed by Scott Fenton, 2-Feb-2011.)
⊢ (𝑋 = 𝑌 → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐴, 𝑌))
Theorem	nfpred 6289	Bound-variable hypothesis builder for the predecessor class. (Contributed by Scott Fenton, 9-Jun-2018.)
⊢ Ⅎ𝑥𝑅    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝑋    ⇒   ⊢ Ⅎ𝑥Pred(𝑅, 𝐴, 𝑋)
Theorem	csbpredg 6290	Move class substitution in and out of the predecessor class of a relation. (Contributed by ML, 25-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌Pred(𝑅, 𝐷, 𝑋) = Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, ⦋𝐴 / 𝑥⦌𝑋))
Theorem	predpredss 6291	If 𝐴 is a subset of 𝐵, then their predecessor classes are also subsets. (Contributed by Scott Fenton, 2-Feb-2011.)
⊢ (𝐴 ⊆ 𝐵 → Pred(𝑅, 𝐴, 𝑋) ⊆ Pred(𝑅, 𝐵, 𝑋))
Theorem	predss 6292	The predecessor class of 𝐴 is a subset of 𝐴. (Contributed by Scott Fenton, 2-Feb-2011.)
⊢ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐴
Theorem	sspred 6293	Another subset/predecessor class relationship. (Contributed by Scott Fenton, 6-Feb-2011.)
⊢ ((𝐵 ⊆ 𝐴 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵) → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐵, 𝑋))
Theorem	dfpred2 6294*	An alternate definition of predecessor class when 𝑋 is a set. (Contributed by Scott Fenton, 8-Feb-2011.)
⊢ 𝑋 ∈ V    ⇒   ⊢ Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ {𝑦 ∣ 𝑦𝑅𝑋})
Theorem	dfpred3 6295*	An alternate definition of predecessor class when 𝑋 is a set. (Contributed by Scott Fenton, 13-Jun-2018.)
⊢ 𝑋 ∈ V    ⇒   ⊢ Pred(𝑅, 𝐴, 𝑋) = {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑋}
Theorem	dfpred3g 6296*	An alternate definition of predecessor class when 𝑋 is a set. (Contributed by Scott Fenton, 13-Jun-2018.)
⊢ (𝑋 ∈ 𝑉 → Pred(𝑅, 𝐴, 𝑋) = {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑋})
Theorem	elpredgg 6297	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 6298	Membership in a predecessor class. (Contributed by Scott Fenton, 17-Apr-2011.) (Proof shortened by BJ, 16-Oct-2024.)
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐴) → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ↔ 𝑌𝑅𝑋))
Theorem	elpredimg 6299	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 6300	Membership in a predecessor class - implicative version. (Contributed by Scott Fenton, 9-May-2012.) (Proof shortened by BJ, 16-Oct-2024.)
⊢ 𝑋 ∈ V    ⇒   ⊢ (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) → 𝑌𝑅𝑋)