P. 384 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 38301-38400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rnresequniqs 38301	The range of a restriction is equal to the union of the quotient set. (Contributed by Peter Mazsa, 19-May-2018.)
⊢ ((𝑅 ↾ 𝐴) ∈ 𝑉 → ran (𝑅 ↾ 𝐴) = ∪ (𝐴 / 𝑅))
Theorem	n0el2 38302	Two ways of expressing that the empty set is not an element of a class. (Contributed by Peter Mazsa, 31-Jan-2018.)
⊢ (¬ ∅ ∈ 𝐴 ↔ dom (◡ E ↾ 𝐴) = 𝐴)
Theorem	cnvepresex 38303	Sethood condition for the restricted converse epsilon relation. (Contributed by Peter Mazsa, 24-Sep-2018.)
⊢ (𝐴 ∈ 𝑉 → (◡ E ↾ 𝐴) ∈ V)
Theorem	cnvepima 38304	The image of converse epsilon. (Contributed by Peter Mazsa, 22-Mar-2023.)
⊢ (𝐴 ∈ 𝑉 → (◡ E “ 𝐴) = ∪ 𝐴)
Theorem	inex3 38305	Sufficient condition for the intersection relation to be a set. (Contributed by Peter Mazsa, 24-Nov-2019.)
⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → (𝐴 ∩ 𝐵) ∈ V)
Theorem	inxpex 38306	Sufficient condition for an intersection with a Cartesian product to be a set. (Contributed by Peter Mazsa, 10-May-2019.)
⊢ ((𝑅 ∈ 𝑊 ∨ (𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉)) → (𝑅 ∩ (𝐴 × 𝐵)) ∈ V)
Theorem	eqres 38307	Converting a class constant definition by restriction (like df-ers 38640 or df-parts 38742) into a binary relation. (Contributed by Peter Mazsa, 1-Oct-2018.)
⊢ 𝑅 = (𝑆 ↾ 𝐶)    ⇒   ⊢ (𝐵 ∈ 𝑉 → (𝐴𝑅𝐵 ↔ (𝐴 ∈ 𝐶 ∧ 𝐴𝑆𝐵)))
Theorem	brrabga 38308*	The law of concretion for operation class abstraction. (Contributed by Peter Mazsa, 24-Oct-2022.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓))    &   ⊢ 𝑅 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (⟨𝐴, 𝐵⟩𝑅𝐶 ↔ 𝜓))
Theorem	brcnvrabga 38309*	The law of concretion for the converse of operation class abstraction. (Contributed by Peter Mazsa, 25-Oct-2022.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓))    &   ⊢ 𝑅 = ◡{⟨⟨𝑦, 𝑧⟩, 𝑥⟩ ∣ 𝜑}    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴𝑅⟨𝐵, 𝐶⟩ ↔ 𝜓))
Theorem	opideq 38310	Equality conditions for ordered pairs ⟨𝐴, 𝐴⟩ and ⟨𝐵, 𝐵⟩. (Contributed by Peter Mazsa, 22-Jul-2019.) (Revised by Thierry Arnoux, 16-Feb-2022.)
⊢ (𝐴 ∈ 𝑉 → (⟨𝐴, 𝐴⟩ = ⟨𝐵, 𝐵⟩ ↔ 𝐴 = 𝐵))
Theorem	iss2 38311	A subclass of the identity relation is the intersection of identity relation with Cartesian product of the domain and range of the class. (Contributed by Peter Mazsa, 22-Jul-2019.)
⊢ (𝐴 ⊆ I ↔ 𝐴 = ( I ∩ (dom 𝐴 × ran 𝐴)))
Theorem	eldmcnv 38312*	Elementhood in a domain of a converse. (Contributed by Peter Mazsa, 25-May-2018.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom ◡𝑅 ↔ ∃𝑢 𝑢𝑅𝐴))
Theorem	dfrel5 38313	Alternate definition of the relation predicate. (Contributed by Peter Mazsa, 6-Nov-2018.)
⊢ (Rel 𝑅 ↔ (𝑅 ↾ dom 𝑅) = 𝑅)
Theorem	dfrel6 38314	Alternate definition of the relation predicate. (Contributed by Peter Mazsa, 14-Mar-2019.)
⊢ (Rel 𝑅 ↔ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) = 𝑅)
Theorem	cnvresrn 38315	Converse restricted to range is converse. (Contributed by Peter Mazsa, 3-Sep-2021.)
⊢ (◡𝑅 ↾ ran 𝑅) = ◡𝑅
Theorem	relssinxpdmrn 38316	Subset of restriction, special case. (Contributed by Peter Mazsa, 10-Apr-2023.)
⊢ (Rel 𝑅 → (𝑅 ⊆ (𝑆 ∩ (dom 𝑅 × ran 𝑅)) ↔ 𝑅 ⊆ 𝑆))
Theorem	cnvref4 38317	Two ways to say that a relation is a subclass. (Contributed by Peter Mazsa, 11-Apr-2023.)
⊢ (Rel 𝑅 → ((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ (𝑆 ∩ (dom 𝑅 × ran 𝑅)) ↔ 𝑅 ⊆ 𝑆))
Theorem	cnvref5 38318*	Two ways to say that a relation is a subclass of the identity relation. (Contributed by Peter Mazsa, 26-Jun-2019.)
⊢ (Rel 𝑅 → (𝑅 ⊆ I ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑥 = 𝑦)))
Theorem	ecin0 38319*	Two ways of saying that the coset of 𝐴 and the coset of 𝐵 have no elements in common. (Contributed by Peter Mazsa, 1-Dec-2018.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (([𝐴]𝑅 ∩ [𝐵]𝑅) = ∅ ↔ ∀𝑥(𝐴𝑅𝑥 → ¬ 𝐵𝑅𝑥)))
Theorem	ecinn0 38320*	Two ways of saying that the coset of 𝐴 and the coset of 𝐵 have some elements in common. (Contributed by Peter Mazsa, 23-Jan-2019.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (([𝐴]𝑅 ∩ [𝐵]𝑅) ≠ ∅ ↔ ∃𝑥(𝐴𝑅𝑥 ∧ 𝐵𝑅𝑥)))
Theorem	ineleq 38321*	Equivalence of restricted universal quantifications. (Contributed by Peter Mazsa, 29-May-2018.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 = 𝑦 ∨ (𝐶 ∩ 𝐷) = ∅) ↔ ∀𝑥 ∈ 𝐴 ∀𝑧∀𝑦 ∈ 𝐵 ((𝑧 ∈ 𝐶 ∧ 𝑧 ∈ 𝐷) → 𝑥 = 𝑦))
Theorem	inecmo 38322*	Equivalence of a double restricted universal quantification and a restricted "at most one" inside a universal quantification. (Contributed by Peter Mazsa, 29-May-2018.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ (Rel 𝑅 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 = 𝑦 ∨ ([𝐵]𝑅 ∩ [𝐶]𝑅) = ∅) ↔ ∀𝑧∃*𝑥 ∈ 𝐴 𝐵𝑅𝑧))
Theorem	inecmo2 38323*	Equivalence of a double restricted universal quantification and a restricted "at most one" inside a universal quantification. (Contributed by Peter Mazsa, 29-May-2018.) (Revised by Peter Mazsa, 2-Sep-2021.)
⊢ ((∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ Rel 𝑅) ↔ (∀𝑥∃*𝑢 ∈ 𝐴 𝑢𝑅𝑥 ∧ Rel 𝑅))
Theorem	ineccnvmo 38324*	Equivalence of a double restricted universal quantification and a restricted "at most one" inside a universal quantification. (Contributed by Peter Mazsa, 2-Sep-2021.)
⊢ (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑦 = 𝑧 ∨ ([𝑦]◡𝐹 ∩ [𝑧]◡𝐹) = ∅) ↔ ∀𝑥∃*𝑦 ∈ 𝐵 𝑥𝐹𝑦)
Theorem	alrmomorn 38325	Equivalence of an "at most one" and an "at most one" restricted to the range inside a universal quantification. (Contributed by Peter Mazsa, 3-Sep-2021.)
⊢ (∀𝑥∃*𝑦 ∈ ran 𝑅 𝑥𝑅𝑦 ↔ ∀𝑥∃*𝑦 𝑥𝑅𝑦)
Theorem	alrmomodm 38326*	Equivalence of an "at most one" and an "at most one" restricted to the domain inside a universal quantification. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ (Rel 𝑅 → (∀𝑥∃*𝑢 ∈ dom 𝑅 𝑢𝑅𝑥 ↔ ∀𝑥∃*𝑢 𝑢𝑅𝑥))
Theorem	ineccnvmo2 38327*	Equivalence of a double universal quantification restricted to the range and an "at most one" inside a universal quantification. (Contributed by Peter Mazsa, 4-Sep-2021.)
⊢ (∀𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹(𝑥 = 𝑦 ∨ ([𝑥]◡𝐹 ∩ [𝑦]◡𝐹) = ∅) ↔ ∀𝑢∃*𝑥 𝑢𝐹𝑥)
Theorem	inecmo3 38328*	Equivalence of a double universal quantification restricted to the domain and an "at most one" inside a universal quantification. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ ((∀𝑢 ∈ dom 𝑅∀𝑣 ∈ dom 𝑅(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ Rel 𝑅) ↔ (∀𝑥∃*𝑢 𝑢𝑅𝑥 ∧ Rel 𝑅))
Theorem	moeu2 38329	Uniqueness is equivalent to non-existence or unique existence. Alternate definition of the at-most-one quantifier, in terms of the existential quantifier and the unique existential quantifier. (Contributed by Peter Mazsa, 19-Nov-2024.)
⊢ (∃*𝑥𝜑 ↔ (¬ ∃𝑥𝜑 ∨ ∃!𝑥𝜑))
Theorem	mopickr 38330	"At most one" picks a variable value, eliminating an existential quantifier. The proof begins with references *2.21 (pm2.21 123) and *14.26 (eupickbi 2629) from [WhiteheadRussell] p. 104 and p. 183. (Contributed by Peter Mazsa, 18-Nov-2024.) (Proof modification is discouraged.)
⊢ ((∃*𝑥𝜓 ∧ ∃𝑥(𝜑 ∧ 𝜓)) → (𝜓 → 𝜑))
Theorem	moantr 38331	Sufficient condition for transitivity of conjunctions inside existential quantifiers. (Contributed by Peter Mazsa, 2-Oct-2018.)
⊢ (∃*𝑥𝜓 → ((∃𝑥(𝜑 ∧ 𝜓) ∧ ∃𝑥(𝜓 ∧ 𝜒)) → ∃𝑥(𝜑 ∧ 𝜒)))
Theorem	brabidgaw 38332*	The law of concretion for a binary relation. Special case of brabga 5481. Version of brabidga 38333 with a disjoint variable condition, which does not require ax-13 2370. (Contributed by Peter Mazsa, 24-Nov-2018.) (Revised by GG, 2-Apr-2024.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}    ⇒   ⊢ (𝑥𝑅𝑦 ↔ 𝜑)
Theorem	brabidga 38333	The law of concretion for a binary relation. Special case of brabga 5481. Usage of this theorem is discouraged because it depends on ax-13 2370, see brabidgaw 38332 for a weaker version that does not require it. (Contributed by Peter Mazsa, 24-Nov-2018.) (New usage is discouraged.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}    ⇒   ⊢ (𝑥𝑅𝑦 ↔ 𝜑)
Theorem	inxp2 38334*	Intersection with a Cartesian product. (Contributed by Peter Mazsa, 18-Jul-2019.)
⊢ (𝑅 ∩ (𝐴 × 𝐵)) = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑥𝑅𝑦)}
Theorem	opabf 38335	A class abstraction of a collection of ordered pairs with a negated wff is the empty set. (Contributed by Peter Mazsa, 21-Oct-2019.) (Proof shortened by Thierry Arnoux, 18-Feb-2022.)
⊢ ¬ 𝜑    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = ∅
Theorem	ec0 38336	The empty-coset of a class is the empty set. (Contributed by Peter Mazsa, 19-May-2019.)
⊢ [𝐴]∅ = ∅
Theorem	brcnvin 38337	Intersection with a converse, binary relation. (Contributed by Peter Mazsa, 24-Mar-2024.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴(𝑅 ∩ ◡𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ 𝐵𝑆𝐴)))
21.26.3  Range Cartesian product
Definition	df-xrn 38338	Define the range Cartesian product of two classes. Definition from [Holmes] p. 40. Membership in this class is characterized by xrnss3v 38339 and brxrn 38341. This is Scott Fenton's df-txp 35827 with a different symbol, see https://github.com/metamath/set.mm/issues/2469 35827. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ (𝐴 ⋉ 𝐵) = ((◡(1st ↾ (V × V)) ∘ 𝐴) ∩ (◡(2nd ↾ (V × V)) ∘ 𝐵))
Theorem	xrnss3v 38339	A range Cartesian product is a subset of the class of ordered triples. This is Scott Fenton's txpss3v 35851 with a different symbol, see https://github.com/metamath/set.mm/issues/2469 35851. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ (𝐴 ⋉ 𝐵) ⊆ (V × (V × V))
Theorem	xrnrel 38340	A range Cartesian product is a relation. This is Scott Fenton's txprel 35852 with a different symbol, see https://github.com/metamath/set.mm/issues/2469 35852. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ Rel (𝐴 ⋉ 𝐵)
Theorem	brxrn 38341	Characterize a ternary relation over a range Cartesian product. Together with xrnss3v 38339, this characterizes elementhood in a range cross. (Contributed by Peter Mazsa, 27-Jun-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴(𝑅 ⋉ 𝑆)⟨𝐵, 𝐶⟩ ↔ (𝐴𝑅𝐵 ∧ 𝐴𝑆𝐶)))
Theorem	brxrn2 38342*	A characterization of the range Cartesian product. (Contributed by Peter Mazsa, 14-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → (𝐴(𝑅 ⋉ 𝑆)𝐵 ↔ ∃𝑥∃𝑦(𝐵 = ⟨𝑥, 𝑦⟩ ∧ 𝐴𝑅𝑥 ∧ 𝐴𝑆𝑦)))
Theorem	dfxrn2 38343*	Alternate definition of the range Cartesian product. (Contributed by Peter Mazsa, 20-Feb-2022.)
⊢ (𝑅 ⋉ 𝑆) = ◡{⟨⟨𝑥, 𝑦⟩, 𝑢⟩ ∣ (𝑢𝑅𝑥 ∧ 𝑢𝑆𝑦)}
Theorem	brxrncnvep 38344	The range product with converse epsilon relation. (Contributed by Peter Mazsa, 22-Jun-2020.) (Revised by Peter Mazsa, 22-Nov-2025.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴(𝑅 ⋉ ◡ E )⟨𝐵, 𝐶⟩ ↔ (𝐶 ∈ 𝐴 ∧ 𝐴𝑅𝐵)))
Theorem	dmxrn 38345	Domain of the range product. (Contributed by Peter Mazsa, 19-Apr-2020.) (Revised by Peter Mazsa, 22-Nov-2025.)
⊢ dom (𝑅 ⋉ 𝑆) = (dom 𝑅 ∩ dom 𝑆)
Theorem	dmcnvep 38346	Domain of converse epsilon relation. (Contributed by Peter Mazsa, 30-Jan-2018.) (Revised by Peter Mazsa, 23-Nov-2025.)
⊢ dom ◡ E = (V ∖ {∅})
Theorem	dmxrncnvep 38347	Domain of the range product with converse epsilon relation. (Contributed by Peter Mazsa, 23-Nov-2025.)
⊢ dom (𝑅 ⋉ ◡ E ) = (dom 𝑅 ∖ {∅})
Theorem	xrneq1 38348	Equality theorem for the range Cartesian product. (Contributed by Peter Mazsa, 16-Dec-2020.)
⊢ (𝐴 = 𝐵 → (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐶))
Theorem	xrneq1i 38349	Equality theorem for the range Cartesian product, inference form. (Contributed by Peter Mazsa, 16-Dec-2020.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐶)
Theorem	xrneq1d 38350	Equality theorem for the range Cartesian product, deduction form. (Contributed by Peter Mazsa, 7-Sep-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐶))
Theorem	xrneq2 38351	Equality theorem for the range Cartesian product. (Contributed by Peter Mazsa, 16-Dec-2020.)
⊢ (𝐴 = 𝐵 → (𝐶 ⋉ 𝐴) = (𝐶 ⋉ 𝐵))
Theorem	xrneq2i 38352	Equality theorem for the range Cartesian product, inference form. (Contributed by Peter Mazsa, 16-Dec-2020.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 ⋉ 𝐴) = (𝐶 ⋉ 𝐵)
Theorem	xrneq2d 38353	Equality theorem for the range Cartesian product, deduction form. (Contributed by Peter Mazsa, 7-Sep-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ⋉ 𝐴) = (𝐶 ⋉ 𝐵))
Theorem	xrneq12 38354	Equality theorem for the range Cartesian product. (Contributed by Peter Mazsa, 16-Dec-2020.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐷))
Theorem	xrneq12i 38355	Equality theorem for the range Cartesian product, inference form. (Contributed by Peter Mazsa, 16-Dec-2020.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐷)
Theorem	xrneq12d 38356	Equality theorem for the range Cartesian product, deduction form. (Contributed by Peter Mazsa, 18-Dec-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐷))
Theorem	elecxrn 38357*	Elementhood in the (𝑅 ⋉ 𝑆)-coset of 𝐴. (Contributed by Peter Mazsa, 18-Apr-2020.) (Revised by Peter Mazsa, 21-Sep-2021.)
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ [𝐴](𝑅 ⋉ 𝑆) ↔ ∃𝑥∃𝑦(𝐵 = ⟨𝑥, 𝑦⟩ ∧ 𝐴𝑅𝑥 ∧ 𝐴𝑆𝑦)))
Theorem	ecxrn 38358*	The (𝑅 ⋉ 𝑆)-coset of 𝐴. (Contributed by Peter Mazsa, 18-Apr-2020.) (Revised by Peter Mazsa, 21-Sep-2021.)
⊢ (𝐴 ∈ 𝑉 → [𝐴](𝑅 ⋉ 𝑆) = {⟨𝑦, 𝑧⟩ ∣ (𝐴𝑅𝑦 ∧ 𝐴𝑆𝑧)})
Theorem	disjressuc2 38359*	Double restricted quantification over the union of a set and its singleton. (Contributed by Peter Mazsa, 22-Aug-2023.)
⊢ (𝐴 ∈ 𝑉 → (∀𝑢 ∈ (𝐴 ∪ {𝐴})∀𝑣 ∈ (𝐴 ∪ {𝐴})(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ↔ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)))
Theorem	disjecxrn 38360	Two ways of saying that (𝑅 ⋉ 𝑆)-cosets are disjoint. (Contributed by Peter Mazsa, 19-Jun-2020.) (Revised by Peter Mazsa, 21-Aug-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (([𝐴](𝑅 ⋉ 𝑆) ∩ [𝐵](𝑅 ⋉ 𝑆)) = ∅ ↔ (([𝐴]𝑅 ∩ [𝐵]𝑅) = ∅ ∨ ([𝐴]𝑆 ∩ [𝐵]𝑆) = ∅)))
Theorem	disjecxrncnvep 38361	Two ways of saying that cosets are disjoint, special case of disjecxrn 38360. (Contributed by Peter Mazsa, 12-Jul-2020.) (Revised by Peter Mazsa, 25-Aug-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (([𝐴](𝑅 ⋉ ◡ E ) ∩ [𝐵](𝑅 ⋉ ◡ E )) = ∅ ↔ ((𝐴 ∩ 𝐵) = ∅ ∨ ([𝐴]𝑅 ∩ [𝐵]𝑅) = ∅)))
Theorem	disjsuc2 38362*	Double restricted quantification over the union of a set and its singleton. (Contributed by Peter Mazsa, 22-Aug-2023.)
⊢ (𝐴 ∈ 𝑉 → (∀𝑢 ∈ (𝐴 ∪ {𝐴})∀𝑣 ∈ (𝐴 ∪ {𝐴})(𝑢 = 𝑣 ∨ ([𝑢](𝑅 ⋉ ◡ E ) ∩ [𝑣](𝑅 ⋉ ◡ E )) = ∅) ↔ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢](𝑅 ⋉ ◡ E ) ∩ [𝑣](𝑅 ⋉ ◡ E )) = ∅) ∧ ∀𝑢 ∈ 𝐴 ((𝑢 ∩ 𝐴) = ∅ ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅))))
Theorem	xrninxp 38363*	Intersection of a range Cartesian product with a Cartesian product. (Contributed by Peter Mazsa, 7-Apr-2020.)
⊢ ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (𝐵 × 𝐶))) = ◡{⟨⟨𝑦, 𝑧⟩, 𝑢⟩ ∣ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑢(𝑅 ⋉ 𝑆)⟨𝑦, 𝑧⟩))}
Theorem	xrninxp2 38364*	Intersection of a range Cartesian product with a Cartesian product. (Contributed by Peter Mazsa, 8-Apr-2020.)
⊢ ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (𝐵 × 𝐶))) = {⟨𝑢, 𝑥⟩ ∣ (𝑥 ∈ (𝐵 × 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑢(𝑅 ⋉ 𝑆)𝑥))}
Theorem	xrninxpex 38365	Sufficient condition for the intersection of a range Cartesian product with a Cartesian product to be a set. (Contributed by Peter Mazsa, 12-Apr-2020.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (𝐵 × 𝐶))) ∈ V)
Theorem	inxpxrn 38366	Two ways to express the intersection of a range Cartesian product with a Cartesian product. (Contributed by Peter Mazsa, 10-Apr-2020.)
⊢ ((𝑅 ∩ (𝐴 × 𝐵)) ⋉ (𝑆 ∩ (𝐴 × 𝐶))) = ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (𝐵 × 𝐶)))
Theorem	br1cnvxrn2 38367*	The converse of a binary relation over a range Cartesian product. (Contributed by Peter Mazsa, 11-Jul-2021.)
⊢ (𝐵 ∈ 𝑉 → (𝐴◡(𝑅 ⋉ 𝑆)𝐵 ↔ ∃𝑦∃𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝐵𝑅𝑦 ∧ 𝐵𝑆𝑧)))
Theorem	elec1cnvxrn2 38368*	Elementhood in the converse range Cartesian product coset of 𝐴. (Contributed by Peter Mazsa, 11-Jul-2021.)
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ [𝐴]◡(𝑅 ⋉ 𝑆) ↔ ∃𝑦∃𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝐵𝑅𝑦 ∧ 𝐵𝑆𝑧)))
Theorem	rnxrn 38369*	Range of the range Cartesian product of classes. (Contributed by Peter Mazsa, 1-Jun-2020.)
⊢ ran (𝑅 ⋉ 𝑆) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑢𝑅𝑥 ∧ 𝑢𝑆𝑦)}
Theorem	rnxrnres 38370*	Range of a range Cartesian product with a restricted relation. (Contributed by Peter Mazsa, 5-Dec-2021.)
⊢ ran (𝑅 ⋉ (𝑆 ↾ 𝐴)) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑢𝑅𝑥 ∧ 𝑢𝑆𝑦)}
Theorem	rnxrncnvepres 38371*	Range of a range Cartesian product with a restriction of the converse epsilon relation. (Contributed by Peter Mazsa, 6-Dec-2021.)
⊢ ran (𝑅 ⋉ (◡ E ↾ 𝐴)) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ 𝑢 ∧ 𝑢𝑅𝑥)}
Theorem	rnxrnidres 38372*	Range of a range Cartesian product with a restriction of the identity relation. (Contributed by Peter Mazsa, 6-Dec-2021.)
⊢ ran (𝑅 ⋉ ( I ↾ 𝐴)) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑢 = 𝑦 ∧ 𝑢𝑅𝑥)}
Theorem	xrnres 38373	Two ways to express restriction of range Cartesian product, see also xrnres2 38374, xrnres3 38375. (Contributed by Peter Mazsa, 5-Jun-2021.)
⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = ((𝑅 ↾ 𝐴) ⋉ 𝑆)
Theorem	xrnres2 38374	Two ways to express restriction of range Cartesian product, see also xrnres 38373, xrnres3 38375. (Contributed by Peter Mazsa, 6-Sep-2021.)
⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = (𝑅 ⋉ (𝑆 ↾ 𝐴))
Theorem	xrnres3 38375	Two ways to express restriction of range Cartesian product, see also xrnres 38373, xrnres2 38374. (Contributed by Peter Mazsa, 28-Mar-2020.)
⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = ((𝑅 ↾ 𝐴) ⋉ (𝑆 ↾ 𝐴))
Theorem	xrnres4 38376	Two ways to express restriction of range Cartesian product. (Contributed by Peter Mazsa, 29-Dec-2020.)
⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (ran (𝑅 ↾ 𝐴) × ran (𝑆 ↾ 𝐴))))
Theorem	xrnresex 38377	Sufficient condition for a restricted range Cartesian product to be a set. (Contributed by Peter Mazsa, 16-Dec-2020.) (Revised by Peter Mazsa, 7-Sep-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ∧ (𝑆 ↾ 𝐴) ∈ 𝑋) → (𝑅 ⋉ (𝑆 ↾ 𝐴)) ∈ V)
Theorem	xrnidresex 38378	Sufficient condition for a range Cartesian product with restricted identity to be a set. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 ⋉ ( I ↾ 𝐴)) ∈ V)
Theorem	xrncnvepresex 38379	Sufficient condition for a range Cartesian product with restricted converse epsilon to be a set. (Contributed by Peter Mazsa, 16-Dec-2020.) (Revised by Peter Mazsa, 23-Sep-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 ⋉ (◡ E ↾ 𝐴)) ∈ V)
Theorem	dmxrncnvepres 38380	Domain of the range product with restricted converse epsilon relation. (Contributed by Peter Mazsa, 23-Nov-2025.)
⊢ dom (𝑅 ⋉ (◡ E ↾ 𝐴)) = (dom (𝑅 ↾ 𝐴) ∖ {∅})
Theorem	eldmxrncnvepres 38381	Element of the domain of the range product with restricted converse epsilon relation. (Contributed by Peter Mazsa, 23-Nov-2025.)
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ dom (𝑅 ⋉ (◡ E ↾ 𝐴)) ↔ (𝐵 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ∧ [𝐵]𝑅 ≠ ∅)))
Theorem	eldmxrncnvepres2 38382*	Element of the domain of the range product with restricted converse epsilon relation. This identifies the domain of the pet 38828 span (𝑅 ⋉ (' E | 𝐴)): a 𝐵 belongs to the domain of the span exactly when 𝐵 is in 𝐴 and has at least one 𝑥 ∈ 𝐵 and 𝑦 with 𝐵𝑅𝑦. (Contributed by Peter Mazsa, 23-Nov-2025.)
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ dom (𝑅 ⋉ (◡ E ↾ 𝐴)) ↔ (𝐵 ∈ 𝐴 ∧ ∃𝑥 𝑥 ∈ 𝐵 ∧ ∃𝑦 𝐵𝑅𝑦)))
Theorem	eceldmqsxrncnvepres 38383	An (𝑅 ⋉ (' E | 𝐴))-coset in its domain quotient. (Contributed by Peter Mazsa, 23-Nov-2025.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑅 ∈ 𝑋) → ([𝐵](𝑅 ⋉ (◡ E ↾ 𝐴)) ∈ (dom (𝑅 ⋉ (◡ E ↾ 𝐴)) / (𝑅 ⋉ (◡ E ↾ 𝐴))) ↔ (𝐵 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ∧ [𝐵]𝑅 ≠ ∅)))
Theorem	eceldmqsxrncnvepres2 38384*	An (𝑅 ⋉ (' E | 𝐴))-coset in its domain quotient. In the pet 38828 span (𝑅 ⋉ (' E | 𝐴)), a block [ B ] lies in the domain quotient exactly when its representative 𝐵 belongs to 𝐴 and actually fires at least one arrow (has some 𝑥 ∈ 𝐵 and some 𝑦 with 𝐵𝑅𝑦). (Contributed by Peter Mazsa, 23-Nov-2025.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑅 ∈ 𝑋) → ([𝐵](𝑅 ⋉ (◡ E ↾ 𝐴)) ∈ (dom (𝑅 ⋉ (◡ E ↾ 𝐴)) / (𝑅 ⋉ (◡ E ↾ 𝐴))) ↔ (𝐵 ∈ 𝐴 ∧ ∃𝑥 𝑥 ∈ 𝐵 ∧ ∃𝑦 𝐵𝑅𝑦)))
Theorem	brin2 38385	Binary relation on an intersection is a special case of binary relation on range Cartesian product. (Contributed by Peter Mazsa, 21-Aug-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴(𝑅 ∩ 𝑆)𝐵 ↔ 𝐴(𝑅 ⋉ 𝑆)⟨𝐵, 𝐵⟩))
Theorem	brin3 38386	Binary relation on an intersection is a special case of binary relation on range Cartesian product. (Contributed by Peter Mazsa, 21-Aug-2021.) (Avoid depending on this detail.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴(𝑅 ∩ 𝑆)𝐵 ↔ 𝐴(𝑅 ⋉ 𝑆){{𝐵}}))
21.26.4  Cosets by ` R `
Definition	df-coss 38387*	Define the class of cosets by 𝑅: 𝑥 and 𝑦 are cosets by 𝑅 iff there exists a set 𝑢 such that both 𝑢𝑅𝑥 and 𝑢𝑅𝑦 hold, i.e., both 𝑥 and 𝑦 are are elements of the 𝑅 -coset of 𝑢 (see dfcoss2 38389 and the comment of dfec2 8635). 𝑅 is usually a relation. This concept simplifies theorems relating partition and equivalence: the left side of these theorems relate to 𝑅, the right side relate to ≀ 𝑅 (see e.g. pet 38828). Without the definition of ≀ 𝑅 we should have to relate the right side of these theorems to a composition of a converse (cf. dfcoss3 38390) or to the range of a range Cartesian product of classes (cf. dfcoss4 38391), which would make the theorems complicated and confusing. Alternate definition is dfcoss2 38389. Technically, we can define it via composition (dfcoss3 38390) or as the range of a range Cartesian product (dfcoss4 38391), but neither of these definitions reveal directly how the cosets by 𝑅 relate to each other. We define functions (df-funsALTV 38658, df-funALTV 38659) and disjoints (dfdisjs 38685, dfdisjs2 38686, df-disjALTV 38682, dfdisjALTV2 38691) with the help of it as well. (Contributed by Peter Mazsa, 9-Jan-2018.)
⊢ ≀ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑢𝑅𝑥 ∧ 𝑢𝑅𝑦)}
Definition	df-coels 38388	Define the class of coelements on the class 𝐴, see also the alternate definition dfcoels 38406. Possible definitions are the special cases of dfcoss3 38390 and dfcoss4 38391. (Contributed by Peter Mazsa, 20-Nov-2019.)
⊢ ∼ 𝐴 = ≀ (◡ E ↾ 𝐴)
Theorem	dfcoss2 38389*	Alternate definition of the class of cosets by 𝑅: 𝑥 and 𝑦 are cosets by 𝑅 iff there exists a set 𝑢 such that both 𝑥 and 𝑦 are are elements of the 𝑅-coset of 𝑢 (see also the comment of dfec2 8635). 𝑅 is usually a relation. (Contributed by Peter Mazsa, 16-Jan-2018.)
⊢ ≀ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑥 ∈ [𝑢]𝑅 ∧ 𝑦 ∈ [𝑢]𝑅)}
Theorem	dfcoss3 38390	Alternate definition of the class of cosets by 𝑅 (see the comment of df-coss 38387). (Contributed by Peter Mazsa, 27-Dec-2018.)
⊢ ≀ 𝑅 = (𝑅 ∘ ◡𝑅)
Theorem	dfcoss4 38391	Alternate definition of the class of cosets by 𝑅 (see the comment of df-coss 38387). (Contributed by Peter Mazsa, 12-Jul-2021.)
⊢ ≀ 𝑅 = ran (𝑅 ⋉ 𝑅)
Theorem	cosscnv 38392*	Class of cosets by the converse of 𝑅 (Contributed by Peter Mazsa, 17-Jun-2020.)
⊢ ≀ ◡𝑅 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑥𝑅𝑢 ∧ 𝑦𝑅𝑢)}
Theorem	coss1cnvres 38393*	Class of cosets by the converse of a restriction. (Contributed by Peter Mazsa, 8-Jun-2020.)
⊢ ≀ ◡(𝑅 ↾ 𝐴) = {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ∃𝑥(𝑢𝑅𝑥 ∧ 𝑣𝑅𝑥))}
Theorem	coss2cnvepres 38394*	Special case of coss1cnvres 38393. (Contributed by Peter Mazsa, 8-Jun-2020.)
⊢ ≀ ◡(◡ E ↾ 𝐴) = {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ∃𝑥(𝑥 ∈ 𝑢 ∧ 𝑥 ∈ 𝑣))}
Theorem	cossex 38395	If 𝐴 is a set then the class of cosets by 𝐴 is a set. (Contributed by Peter Mazsa, 4-Jan-2019.)
⊢ (𝐴 ∈ 𝑉 → ≀ 𝐴 ∈ V)
Theorem	cosscnvex 38396	If 𝐴 is a set then the class of cosets by the converse of 𝐴 is a set. (Contributed by Peter Mazsa, 18-Oct-2019.)
⊢ (𝐴 ∈ 𝑉 → ≀ ◡𝐴 ∈ V)
Theorem	1cosscnvepresex 38397	Sufficient condition for a restricted converse epsilon coset to be a set. (Contributed by Peter Mazsa, 24-Sep-2021.)
⊢ (𝐴 ∈ 𝑉 → ≀ (◡ E ↾ 𝐴) ∈ V)
Theorem	1cossxrncnvepresex 38398	Sufficient condition for a restricted converse epsilon range Cartesian product to be a set. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) ∈ V)
Theorem	relcoss 38399	Cosets by 𝑅 is a relation. (Contributed by Peter Mazsa, 27-Dec-2018.)
⊢ Rel ≀ 𝑅
Theorem	relcoels 38400	Coelements on 𝐴 is a relation. (Contributed by Peter Mazsa, 5-Oct-2021.)
⊢ Rel ∼ 𝐴