P. 389 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 38801-38900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	inex3 38801	Sufficient condition for the intersection relation to be a set. (Contributed by Peter Mazsa, 24-Nov-2019.)
⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → (𝐴 ∩ 𝐵) ∈ V)
Theorem	inxpex 38802	Sufficient condition for an intersection with a Cartesian product to be a set. (Contributed by Peter Mazsa, 10-May-2019.)
⊢ ((𝑅 ∈ 𝑊 ∨ (𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉)) → (𝑅 ∩ (𝐴 × 𝐵)) ∈ V)
Theorem	eqres 38803	Converting a class constant definition by restriction (like df-ers 39211 or df-parts 39331) into a binary relation. (Contributed by Peter Mazsa, 1-Oct-2018.)
⊢ 𝑅 = (𝑆 ↾ 𝐶)    ⇒   ⊢ (𝐵 ∈ 𝑉 → (𝐴𝑅𝐵 ↔ (𝐴 ∈ 𝐶 ∧ 𝐴𝑆𝐵)))
Theorem	brrabga 38804*	The law of concretion for operation class abstraction. (Contributed by Peter Mazsa, 24-Oct-2022.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓))    &   ⊢ 𝑅 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (⟨𝐴, 𝐵⟩𝑅𝐶 ↔ 𝜓))
Theorem	brcnvrabga 38805*	The law of concretion for the converse of operation class abstraction. (Contributed by Peter Mazsa, 25-Oct-2022.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓))    &   ⊢ 𝑅 = ◡{⟨⟨𝑦, 𝑧⟩, 𝑥⟩ ∣ 𝜑}    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴𝑅⟨𝐵, 𝐶⟩ ↔ 𝜓))
Theorem	opideq 38806	Equality conditions for ordered pairs ⟨𝐴, 𝐴⟩ and ⟨𝐵, 𝐵⟩. (Contributed by Peter Mazsa, 22-Jul-2019.) (Revised by Thierry Arnoux, 16-Feb-2022.)
⊢ (𝐴 ∈ 𝑉 → (⟨𝐴, 𝐴⟩ = ⟨𝐵, 𝐵⟩ ↔ 𝐴 = 𝐵))
Theorem	iss2 38807	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 38808*	Elementhood in a domain of a converse. (Contributed by Peter Mazsa, 25-May-2018.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom ◡𝑅 ↔ ∃𝑢 𝑢𝑅𝐴))
Theorem	dfrel5 38809	Alternate definition of the relation predicate. (Contributed by Peter Mazsa, 6-Nov-2018.)
⊢ (Rel 𝑅 ↔ (𝑅 ↾ dom 𝑅) = 𝑅)
Theorem	dfrel6 38810	Alternate definition of the relation predicate. (Contributed by Peter Mazsa, 14-Mar-2019.)
⊢ (Rel 𝑅 ↔ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) = 𝑅)
Theorem	cnvresrn 38811	Converse restricted to range is converse. (Contributed by Peter Mazsa, 3-Sep-2021.)
⊢ (◡𝑅 ↾ ran 𝑅) = ◡𝑅
Theorem	relssinxpdmrn 38812	Subset of restriction, special case. (Contributed by Peter Mazsa, 10-Apr-2023.)
⊢ (Rel 𝑅 → (𝑅 ⊆ (𝑆 ∩ (dom 𝑅 × ran 𝑅)) ↔ 𝑅 ⊆ 𝑆))
Theorem	cnvref4 38813	Two ways to say that a relation is a subclass. (Contributed by Peter Mazsa, 11-Apr-2023.)
⊢ (Rel 𝑅 → ((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ (𝑆 ∩ (dom 𝑅 × ran 𝑅)) ↔ 𝑅 ⊆ 𝑆))
Theorem	cnvref5 38814*	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 38815*	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 38816*	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 38817*	Equivalence of restricted universal quantifications. (Contributed by Peter Mazsa, 29-May-2018.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 = 𝑦 ∨ (𝐶 ∩ 𝐷) = ∅) ↔ ∀𝑥 ∈ 𝐴 ∀𝑧∀𝑦 ∈ 𝐵 ((𝑧 ∈ 𝐶 ∧ 𝑧 ∈ 𝐷) → 𝑥 = 𝑦))
Theorem	inecmo 38818*	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 38819*	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 38820*	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 38821	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 38822*	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	ralmo 38823*	"At most one" can be restricted to the range. (Contributed by Peter Mazsa, 2-Feb-2026.)
⊢ (∀𝑥∃*𝑢 𝑢𝑅𝑥 ↔ ∀𝑥 ∈ ran 𝑅∃*𝑢 𝑢𝑅𝑥)
Theorem	ralrnmo 38824*	On the range, "at most one" becomes "exactly one". (Contributed by Peter Mazsa, 27-Sep-2018.) (Revised by Peter Mazsa, 2-Feb-2026.)
⊢ (∀𝑥 ∈ ran 𝑅∃*𝑢 𝑢𝑅𝑥 ↔ ∀𝑥 ∈ ran 𝑅∃!𝑢 𝑢𝑅𝑥)
Theorem	dmqsex 38825	Sethood of the domain quotient under sethood of 𝑅. (Contributed by Peter Mazsa, 2-Nov-2018.)
⊢ (𝑅 ∈ 𝑉 → (dom 𝑅 / 𝑅) ∈ V)
Theorem	raldmqsmo 38826*	On the quotient carrier, "at most one" and "exactly one" coincide for coset witnesses. (Contributed by Peter Mazsa, 6-Feb-2026.)
⊢ (∀𝑢 ∈ (dom 𝑅 / 𝑅)∃*𝑡 ∈ dom 𝑅 𝑢 = [𝑡]𝑅 ↔ ∀𝑢 ∈ (dom 𝑅 / 𝑅)∃!𝑡 ∈ dom 𝑅 𝑢 = [𝑡]𝑅)
Theorem	ralrmo3 38827*	Pull a restricted universal quantifier into the body (for ∃*). (Contributed by Peter Mazsa, 9-May-2019.)
⊢ (∀𝑦 ∈ 𝐵 ∃*𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦∃*𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 ∧ 𝜑))
Theorem	raldmqseu 38828*	Equivalence between "exactly one" on the quotient carrier and "at most one" globally. Provides a type-safe way to talk about unique representatives either as ∃! on the intended carrier or as a global ∃* statement. (Contributed by Peter Mazsa, 6-Feb-2026.)
⊢ (𝑅 ∈ 𝑉 → (∀𝑢 ∈ (dom 𝑅 / 𝑅)∃!𝑡 ∈ dom 𝑅 𝑢 = [𝑡]𝑅 ↔ ∀𝑢∃*𝑡 ∈ dom 𝑅 𝑢 = [𝑡]𝑅))
Theorem	rsp3 38829*	From a restricted universal statement over 𝐴, specialize to an arbitrary element 𝑦 ∈ 𝐴, cf. rsp 3249. (Contributed by Peter Mazsa, 9-Feb-2026.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝑦 ∈ 𝐴 → 𝜓))
Theorem	rsp3eq 38830*	From a restricted universal statement over 𝐴, specialize to an arbitrary element class, cf. rsp3 38829. (Contributed by Peter Mazsa, 9-Feb-2026.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ((𝑦 = 𝐵 ∧ 𝐵 ∈ 𝐴) → 𝜓))
Theorem	ineccnvmo2 38831*	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 38832*	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 38833	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 38834	"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 2662) from [WhiteheadRussell] p. 104 and p. 183. (Contributed by Peter Mazsa, 18-Nov-2024.) (Proof modification is discouraged.)
⊢ ((∃*𝑥𝜓 ∧ ∃𝑥(𝜑 ∧ 𝜓)) → (𝜓 → 𝜑))
Theorem	moantr 38835	Sufficient condition for transitivity of conjunctions inside existential quantifiers. (Contributed by Peter Mazsa, 2-Oct-2018.)
⊢ (∃*𝑥𝜓 → ((∃𝑥(𝜑 ∧ 𝜓) ∧ ∃𝑥(𝜓 ∧ 𝜒)) → ∃𝑥(𝜑 ∧ 𝜒)))
Theorem	brabidgaw 38836*	The law of concretion for a binary relation. Special case of brabga 5503. Version of brabidga 38837 with a disjoint variable condition, which does not require ax-13 2402. (Contributed by Peter Mazsa, 24-Nov-2018.) (Revised by GG, 2-Apr-2024.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}    ⇒   ⊢ (𝑥𝑅𝑦 ↔ 𝜑)
Theorem	brabidga 38837	The law of concretion for a binary relation. Special case of brabga 5503. Usage of this theorem is discouraged because it depends on ax-13 2402, see brabidgaw 38836 for a weaker version that does not require it. (Contributed by Peter Mazsa, 24-Nov-2018.) (New usage is discouraged.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}    ⇒   ⊢ (𝑥𝑅𝑦 ↔ 𝜑)
Theorem	inxp2 38838*	Intersection with a Cartesian product. (Contributed by Peter Mazsa, 18-Jul-2019.)
⊢ (𝑅 ∩ (𝐴 × 𝐵)) = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑥𝑅𝑦)}
Theorem	opabf 38839	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 38840	The empty-coset of a class is the empty set. (Contributed by Peter Mazsa, 19-May-2019.)
⊢ [𝐴]∅ = ∅
Theorem	brcnvin 38841	Intersection with a converse, binary relation. (Contributed by Peter Mazsa, 24-Mar-2024.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴(𝑅 ∩ ◡𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ 𝐵𝑆𝐴)))
Theorem	ssdmral 38842*	Subclass of a domain. (Contributed by Peter Mazsa, 15-Sep-2018.)
⊢ (𝐴 ⊆ dom 𝑅 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 𝑥𝑅𝑦)
21.26.3  Range Cartesian product
Definition	df-xrn 38843	Define the range Cartesian product of two classes. Definition from [Holmes] p. 40. Membership in this class is characterized by xrnss3v 38844 and brxrn 38846. This is Scott Fenton's df-txp 36166 with a different symbol, see https://github.com/metamath/set.mm/issues/2469 36166. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ (𝐴 ⋉ 𝐵) = ((◡(1st ↾ (V × V)) ∘ 𝐴) ∩ (◡(2nd ↾ (V × V)) ∘ 𝐵))
Theorem	xrnss3v 38844	A range Cartesian product is a subset of the class of ordered triples. This is Scott Fenton's txpss3v 36190 with a different symbol, see https://github.com/metamath/set.mm/issues/2469 36190. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ (𝐴 ⋉ 𝐵) ⊆ (V × (V × V))
Theorem	xrnrel 38845	A range Cartesian product is a relation. This is Scott Fenton's txprel 36191 with a different symbol, see https://github.com/metamath/set.mm/issues/2469 36191. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ Rel (𝐴 ⋉ 𝐵)
Theorem	brxrn 38846	Characterize a ternary relation over a range Cartesian product. Together with xrnss3v 38844, this characterizes elementhood in a range cross. (Contributed by Peter Mazsa, 27-Jun-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴(𝑅 ⋉ 𝑆)⟨𝐵, 𝐶⟩ ↔ (𝐴𝑅𝐵 ∧ 𝐴𝑆𝐶)))
Theorem	brxrn2 38847*	A characterization of the range Cartesian product. (Contributed by Peter Mazsa, 14-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → (𝐴(𝑅 ⋉ 𝑆)𝐵 ↔ ∃𝑥∃𝑦(𝐵 = ⟨𝑥, 𝑦⟩ ∧ 𝐴𝑅𝑥 ∧ 𝐴𝑆𝑦)))
Theorem	dfxrn2 38848*	Alternate definition of the range Cartesian product. (Contributed by Peter Mazsa, 20-Feb-2022.)
⊢ (𝑅 ⋉ 𝑆) = ◡{⟨⟨𝑥, 𝑦⟩, 𝑢⟩ ∣ (𝑢𝑅𝑥 ∧ 𝑢𝑆𝑦)}
Theorem	brxrncnvep 38849	The range product with converse epsilon relation. (Contributed by Peter Mazsa, 22-Jun-2020.) (Revised by Peter Mazsa, 22-Nov-2025.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴(𝑅 ⋉ ◡ E )⟨𝐵, 𝐶⟩ ↔ (𝐶 ∈ 𝐴 ∧ 𝐴𝑅𝐵)))
Theorem	dmxrn 38850	Domain of the range product. (Contributed by Peter Mazsa, 19-Apr-2020.) (Revised by Peter Mazsa, 22-Nov-2025.)
⊢ dom (𝑅 ⋉ 𝑆) = (dom 𝑅 ∩ dom 𝑆)
Theorem	dmcnvep 38851	Domain of converse epsilon relation. (Contributed by Peter Mazsa, 30-Jan-2018.) (Revised by Peter Mazsa, 23-Nov-2025.)
⊢ dom ◡ E = (V ∖ {∅})
Theorem	dmxrncnvep 38852	Domain of the range product with converse epsilon relation. (Contributed by Peter Mazsa, 23-Nov-2025.)
⊢ dom (𝑅 ⋉ ◡ E ) = (dom 𝑅 ∖ {∅})
Theorem	dmcnvepres 38853	Domain of the restricted converse epsilon relation. (Contributed by Peter Mazsa, 28-Jan-2026.)
⊢ dom (◡ E ↾ 𝐴) = (𝐴 ∖ {∅})
Theorem	dmuncnvepres 38854	Domain of the union with the converse epsilon, restricted. (Contributed by Peter Mazsa, 28-Jan-2026.)
⊢ dom ((𝑅 ∪ ◡ E ) ↾ 𝐴) = (𝐴 ∩ (dom 𝑅 ∪ (V ∖ {∅})))
Theorem	dmxrnuncnvepres 38855	Domain of the combined relation of two special relations, see blockadjliftmap 38921. (Contributed by Peter Mazsa, 28-Jan-2026.)
⊢ dom (((𝑅 ⋉ ◡ E ) ∪ ◡ E ) ↾ 𝐴) = (𝐴 ∖ {∅})
Theorem	ecun 38856	The union coset of 𝐴. (Contributed by Peter Mazsa, 28-Jan-2026.)
⊢ (𝐴 ∈ 𝑉 → [𝐴](𝑅 ∪ 𝑆) = ([𝐴]𝑅 ∪ [𝐴]𝑆))
Theorem	ecunres 38857	The restricted union coset of 𝐵. (Contributed by Peter Mazsa, 28-Jan-2026.)
⊢ (𝐵 ∈ 𝑉 → [𝐵]((𝑅 ∪ 𝑆) ↾ 𝐴) = ([𝐵](𝑅 ↾ 𝐴) ∪ [𝐵](𝑆 ↾ 𝐴)))
Theorem	ecuncnvepres 38858	The restricted union with converse epsilon relation coset of 𝐵. (Contributed by Peter Mazsa, 28-Jan-2026.)
⊢ (𝐵 ∈ 𝐴 → [𝐵]((𝑅 ∪ ◡ E ) ↾ 𝐴) = (𝐵 ∪ [𝐵]𝑅))
Theorem	xrneq1 38859	Equality theorem for the range Cartesian product. (Contributed by Peter Mazsa, 16-Dec-2020.)
⊢ (𝐴 = 𝐵 → (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐶))
Theorem	xrneq1i 38860	Equality theorem for the range Cartesian product, inference form. (Contributed by Peter Mazsa, 16-Dec-2020.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐶)
Theorem	xrneq1d 38861	Equality theorem for the range Cartesian product, deduction form. (Contributed by Peter Mazsa, 7-Sep-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐶))
Theorem	xrneq2 38862	Equality theorem for the range Cartesian product. (Contributed by Peter Mazsa, 16-Dec-2020.)
⊢ (𝐴 = 𝐵 → (𝐶 ⋉ 𝐴) = (𝐶 ⋉ 𝐵))
Theorem	xrneq2i 38863	Equality theorem for the range Cartesian product, inference form. (Contributed by Peter Mazsa, 16-Dec-2020.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 ⋉ 𝐴) = (𝐶 ⋉ 𝐵)
Theorem	xrneq2d 38864	Equality theorem for the range Cartesian product, deduction form. (Contributed by Peter Mazsa, 7-Sep-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ⋉ 𝐴) = (𝐶 ⋉ 𝐵))
Theorem	xrneq12 38865	Equality theorem for the range Cartesian product. (Contributed by Peter Mazsa, 16-Dec-2020.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐷))
Theorem	xrneq12i 38866	Equality theorem for the range Cartesian product, inference form. (Contributed by Peter Mazsa, 16-Dec-2020.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐷)
Theorem	xrneq12d 38867	Equality theorem for the range Cartesian product, deduction form. (Contributed by Peter Mazsa, 18-Dec-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐷))
Theorem	elecxrn 38868*	Elementhood in the (𝑅 ⋉ 𝑆)-coset of 𝐴. (Contributed by Peter Mazsa, 18-Apr-2020.) (Revised by Peter Mazsa, 21-Sep-2021.)
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ [𝐴](𝑅 ⋉ 𝑆) ↔ ∃𝑥∃𝑦(𝐵 = ⟨𝑥, 𝑦⟩ ∧ 𝐴𝑅𝑥 ∧ 𝐴𝑆𝑦)))
Theorem	ecxrn 38869*	The (𝑅 ⋉ 𝑆)-coset of 𝐴. (Contributed by Peter Mazsa, 18-Apr-2020.) (Revised by Peter Mazsa, 21-Sep-2021.)
⊢ (𝐴 ∈ 𝑉 → [𝐴](𝑅 ⋉ 𝑆) = {⟨𝑦, 𝑧⟩ ∣ (𝐴𝑅𝑦 ∧ 𝐴𝑆𝑧)})
Theorem	relecxrn 38870	The (𝑅 ⋉ 𝑆)-coset of a set is a relation. (Contributed by Peter Mazsa, 15-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → Rel [𝐴](𝑅 ⋉ 𝑆))
Theorem	ecxrn2 38871	The (𝑅 ⋉ 𝑆)-coset of a set is the Cartesian product of its 𝑅-coset and 𝑆-coset. (Contributed by Peter Mazsa, 16-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → [𝐴](𝑅 ⋉ 𝑆) = ([𝐴]𝑅 × [𝐴]𝑆))
Theorem	ecxrncnvep 38872*	The (𝑅 ⋉ ◡ E )-coset of a set. (Contributed by Peter Mazsa, 22-May-2021.)
⊢ (𝐴 ∈ 𝑉 → [𝐴](𝑅 ⋉ ◡ E ) = {⟨𝑦, 𝑧⟩ ∣ (𝑧 ∈ 𝐴 ∧ 𝐴𝑅𝑦)})
Theorem	ecxrncnvep2 38873	The (𝑅 ⋉ ◡ E )-coset of a set is the Cartesian product of its 𝑅-coset and the set. (Contributed by Peter Mazsa, 25-Jan-2026.)
⊢ (𝐴 ∈ 𝑉 → [𝐴](𝑅 ⋉ ◡ E ) = ([𝐴]𝑅 × 𝐴))
Theorem	disjressuc2 38874*	Double restricted quantification over the union of a set and its singleton. (Contributed by Peter Mazsa, 22-Aug-2023.)
⊢ (𝐴 ∈ 𝑉 → (∀𝑢 ∈ (𝐴 ∪ {𝐴})∀𝑣 ∈ (𝐴 ∪ {𝐴})(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ↔ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)))
Theorem	disjecxrn 38875	Two ways of saying that (𝑅 ⋉ 𝑆)-cosets are disjoint. (Contributed by Peter Mazsa, 19-Jun-2020.) (Revised by Peter Mazsa, 21-Aug-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (([𝐴](𝑅 ⋉ 𝑆) ∩ [𝐵](𝑅 ⋉ 𝑆)) = ∅ ↔ (([𝐴]𝑅 ∩ [𝐵]𝑅) = ∅ ∨ ([𝐴]𝑆 ∩ [𝐵]𝑆) = ∅)))
Theorem	disjecxrncnvep 38876	Two ways of saying that cosets are disjoint, special case of disjecxrn 38875. (Contributed by Peter Mazsa, 12-Jul-2020.) (Revised by Peter Mazsa, 25-Aug-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (([𝐴](𝑅 ⋉ ◡ E ) ∩ [𝐵](𝑅 ⋉ ◡ E )) = ∅ ↔ ((𝐴 ∩ 𝐵) = ∅ ∨ ([𝐴]𝑅 ∩ [𝐵]𝑅) = ∅)))
Theorem	disjsuc2 38877*	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 38878*	Intersection of a range Cartesian product with a Cartesian product. (Contributed by Peter Mazsa, 7-Apr-2020.)
⊢ ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (𝐵 × 𝐶))) = ◡{⟨⟨𝑦, 𝑧⟩, 𝑢⟩ ∣ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑢(𝑅 ⋉ 𝑆)⟨𝑦, 𝑧⟩))}
Theorem	xrninxp2 38879*	Intersection of a range Cartesian product with a Cartesian product. (Contributed by Peter Mazsa, 8-Apr-2020.)
⊢ ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (𝐵 × 𝐶))) = {⟨𝑢, 𝑥⟩ ∣ (𝑥 ∈ (𝐵 × 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑢(𝑅 ⋉ 𝑆)𝑥))}
Theorem	xrninxpex 38880	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 38881	Two ways to express the intersection of a range Cartesian product with a Cartesian product. (Contributed by Peter Mazsa, 10-Apr-2020.)
⊢ ((𝑅 ∩ (𝐴 × 𝐵)) ⋉ (𝑆 ∩ (𝐴 × 𝐶))) = ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (𝐵 × 𝐶)))
Theorem	br1cnvxrn2 38882*	The converse of a binary relation over a range Cartesian product. (Contributed by Peter Mazsa, 11-Jul-2021.)
⊢ (𝐵 ∈ 𝑉 → (𝐴◡(𝑅 ⋉ 𝑆)𝐵 ↔ ∃𝑦∃𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝐵𝑅𝑦 ∧ 𝐵𝑆𝑧)))
Theorem	elec1cnvxrn2 38883*	Elementhood in the converse range Cartesian product coset of 𝐴. (Contributed by Peter Mazsa, 11-Jul-2021.)
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ [𝐴]◡(𝑅 ⋉ 𝑆) ↔ ∃𝑦∃𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝐵𝑅𝑦 ∧ 𝐵𝑆𝑧)))
Theorem	rnxrn 38884*	Range of the range Cartesian product of classes. (Contributed by Peter Mazsa, 1-Jun-2020.)
⊢ ran (𝑅 ⋉ 𝑆) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑢𝑅𝑥 ∧ 𝑢𝑆𝑦)}
Theorem	rnxrnres 38885*	Range of a range Cartesian product with a restricted relation. (Contributed by Peter Mazsa, 5-Dec-2021.)
⊢ ran (𝑅 ⋉ (𝑆 ↾ 𝐴)) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑢𝑅𝑥 ∧ 𝑢𝑆𝑦)}
Theorem	rnxrncnvepres 38886*	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 38887*	Range of a range Cartesian product with a restriction of the identity relation. (Contributed by Peter Mazsa, 6-Dec-2021.)
⊢ ran (𝑅 ⋉ ( I ↾ 𝐴)) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑢 = 𝑦 ∧ 𝑢𝑅𝑥)}
Theorem	xrnres 38888	Two ways to express restriction of range Cartesian product, see also xrnres2 38889, xrnres3 38890. (Contributed by Peter Mazsa, 5-Jun-2021.)
⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = ((𝑅 ↾ 𝐴) ⋉ 𝑆)
Theorem	xrnres2 38889	Two ways to express restriction of range Cartesian product, see also xrnres 38888, xrnres3 38890. (Contributed by Peter Mazsa, 6-Sep-2021.)
⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = (𝑅 ⋉ (𝑆 ↾ 𝐴))
Theorem	xrnres3 38890	Two ways to express restriction of range Cartesian product, see also xrnres 38888, xrnres2 38889. (Contributed by Peter Mazsa, 28-Mar-2020.)
⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = ((𝑅 ↾ 𝐴) ⋉ (𝑆 ↾ 𝐴))
Theorem	xrnres4 38891	Two ways to express restriction of range Cartesian product. (Contributed by Peter Mazsa, 29-Dec-2020.)
⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (ran (𝑅 ↾ 𝐴) × ran (𝑆 ↾ 𝐴))))
Theorem	xrnresex 38892	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 38893	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 38894	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 38895	Domain of the range product with restricted converse epsilon relation. (Contributed by Peter Mazsa, 23-Nov-2025.)
⊢ dom (𝑅 ⋉ (◡ E ↾ 𝐴)) = (dom (𝑅 ↾ 𝐴) ∖ {∅})
Theorem	dmxrncnvepres2 38896	Domain of the range product with restricted converse epsilon relation. (Contributed by Peter Mazsa, 29-Jan-2026.)
⊢ dom (𝑅 ⋉ (◡ E ↾ 𝐴)) = (𝐴 ∩ (dom 𝑅 ∖ {∅}))
Theorem	eldmxrncnvepres 38897	Element of the domain of the range product with restricted converse epsilon relation. (Contributed by Peter Mazsa, 23-Nov-2025.)
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ dom (𝑅 ⋉ (◡ E ↾ 𝐴)) ↔ (𝐵 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ∧ [𝐵]𝑅 ≠ ∅)))
Theorem	eldmxrncnvepres2 38898*	Element of the domain of the range product with restricted converse epsilon relation. This identifies the domain of the pet 39428 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 38899	An (𝑅 ⋉ (◡ E ↾ 𝐴))-coset in its domain quotient. (Contributed by Peter Mazsa, 23-Nov-2025.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑅 ∈ 𝑋) → ([𝐵](𝑅 ⋉ (◡ E ↾ 𝐴)) ∈ (dom (𝑅 ⋉ (◡ E ↾ 𝐴)) / (𝑅 ⋉ (◡ E ↾ 𝐴))) ↔ (𝐵 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ∧ [𝐵]𝑅 ≠ ∅)))
Theorem	eceldmqsxrncnvepres2 38900*	An (𝑅 ⋉ (◡ E ↾ 𝐴))-coset in its domain quotient. In the pet 39428 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 ↾ 𝐴))) ↔ (𝐵 ∈ 𝐴 ∧ ∃𝑥 𝑥 ∈ 𝐵 ∧ ∃𝑦 𝐵𝑅𝑦)))