P. 387 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 38601-38700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	brvdif 38601	Binary relation with universal complement is the negation of the relation. (Contributed by Peter Mazsa, 1-Jul-2018.)
⊢ (𝐴(V ∖ 𝑅)𝐵 ↔ ¬ 𝐴𝑅𝐵)
Theorem	brvdif2 38602	Binary relation with universal complement. (Contributed by Peter Mazsa, 14-Jul-2018.)
⊢ (𝐴(V ∖ 𝑅)𝐵 ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
Theorem	brvvdif 38603	Binary relation with the complement under the universal class of ordered pairs. (Contributed by Peter Mazsa, 9-Nov-2018.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴((V × V) ∖ 𝑅)𝐵 ↔ ¬ 𝐴𝑅𝐵))
Theorem	brvbrvvdif 38604	Binary relation with the complement under the universal class of ordered pairs is the same as with universal complement. (Contributed by Peter Mazsa, 28-Nov-2018.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴((V × V) ∖ 𝑅)𝐵 ↔ 𝐴(V ∖ 𝑅)𝐵))
Theorem	brcnvep 38605	The converse of the binary epsilon relation. (Contributed by Peter Mazsa, 30-Jan-2018.)
⊢ (𝐴 ∈ 𝑉 → (𝐴◡ E 𝐵 ↔ 𝐵 ∈ 𝐴))
Theorem	elecALTV 38606	Elementhood in the 𝑅-coset of 𝐴. Theorem 72 of [Suppes] p. 82. (I think we should replace elecg 8681 with this original form of Suppes. Peter Mazsa). (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐵 ∈ [𝐴]𝑅 ↔ 𝐴𝑅𝐵))
Theorem	brcnvepres 38607	Restricted converse epsilon binary relation. (Contributed by Peter Mazsa, 10-Feb-2018.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵(◡ E ↾ 𝐴)𝐶 ↔ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵)))
Theorem	brres2 38608	Binary relation on a restriction. (Contributed by Peter Mazsa, 2-Jan-2019.) (Revised by Peter Mazsa, 16-Dec-2021.)
⊢ (𝐵(𝑅 ↾ 𝐴)𝐶 ↔ 𝐵(𝑅 ∩ (𝐴 × ran (𝑅 ↾ 𝐴)))𝐶)
Theorem	br1cnvres 38609	Binary relation on the converse of a restriction. (Contributed by Peter Mazsa, 27-Jul-2019.)
⊢ (𝐵 ∈ 𝑉 → (𝐵◡(𝑅 ↾ 𝐴)𝐶 ↔ (𝐶 ∈ 𝐴 ∧ 𝐶𝑅𝐵)))
Theorem	elec1cnvres 38610	Elementhood in the converse restricted coset of 𝐵. (Contributed by Peter Mazsa, 21-Sep-2018.)
⊢ (𝐵 ∈ 𝑉 → (𝐶 ∈ [𝐵]◡(𝑅 ↾ 𝐴) ↔ (𝐶 ∈ 𝐴 ∧ 𝐶𝑅𝐵)))
Theorem	ec1cnvres 38611*	Converse restricted coset of 𝐵. (Contributed by Peter Mazsa, 22-Mar-2019.) (Revised by Peter Mazsa, 21-Oct-2021.)
⊢ (𝐵 ∈ 𝑉 → [𝐵]◡(𝑅 ↾ 𝐴) = {𝑥 ∈ 𝐴 ∣ 𝑥𝑅𝐵})
Theorem	eldmres 38612*	Elementhood in the domain of a restriction. (Contributed by Peter Mazsa, 9-Jan-2019.)
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ dom (𝑅 ↾ 𝐴) ↔ (𝐵 ∈ 𝐴 ∧ ∃𝑦 𝐵𝑅𝑦)))
Theorem	elrnres 38613*	Element of the range of a restriction. (Contributed by Peter Mazsa, 26-Dec-2018.)
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ ran (𝑅 ↾ 𝐴) ↔ ∃𝑥 ∈ 𝐴 𝑥𝑅𝐵))
Theorem	eldmressnALTV 38614	Element of the domain of a restriction to a singleton. (Contributed by Peter Mazsa, 12-Jun-2024.)
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ dom (𝑅 ↾ {𝐴}) ↔ (𝐵 = 𝐴 ∧ 𝐴 ∈ dom 𝑅)))
Theorem	elrnressn 38615	Element of the range of a restriction to a singleton. (Contributed by Peter Mazsa, 12-Jun-2024.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐵 ∈ ran (𝑅 ↾ {𝐴}) ↔ 𝐴𝑅𝐵))
Theorem	eldm4 38616*	Elementhood in a domain. (Contributed by Peter Mazsa, 24-Oct-2018.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom 𝑅 ↔ ∃𝑦 𝑦 ∈ [𝐴]𝑅))
Theorem	eldmres2 38617*	Elementhood in the domain of a restriction. (Contributed by Peter Mazsa, 21-Aug-2020.)
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ dom (𝑅 ↾ 𝐴) ↔ (𝐵 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ [𝐵]𝑅)))
Theorem	eldmres3 38618	Elementhood in the domain of a restriction. (Contributed by Peter Mazsa, 23-Nov-2025.)
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ dom (𝑅 ↾ 𝐴) ↔ (𝐵 ∈ 𝐴 ∧ [𝐵]𝑅 ≠ ∅)))
Theorem	eceq1i 38619	Equality theorem for 𝐶-coset of 𝐴 and 𝐶-coset of 𝐵, inference version. (Contributed by Peter Mazsa, 11-May-2021.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ [𝐴]𝐶 = [𝐵]𝐶
Theorem	ecres 38620*	Restricted coset of 𝐵. (Contributed by Peter Mazsa, 9-Dec-2018.)
⊢ [𝐵](𝑅 ↾ 𝐴) = {𝑥 ∣ (𝐵 ∈ 𝐴 ∧ 𝐵𝑅𝑥)}
Theorem	eccnvepres 38621*	Restricted converse epsilon coset of 𝐵. (Contributed by Peter Mazsa, 11-Feb-2018.) (Revised by Peter Mazsa, 21-Oct-2021.)
⊢ (𝐵 ∈ 𝑉 → [𝐵](◡ E ↾ 𝐴) = {𝑥 ∈ 𝐵 ∣ 𝐵 ∈ 𝐴})
Theorem	eleccnvep 38622	Elementhood in the converse epsilon coset of 𝐴 is elementhood in 𝐴. (Contributed by Peter Mazsa, 27-Jan-2019.)
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ [𝐴]◡ E ↔ 𝐵 ∈ 𝐴))
Theorem	eccnvep 38623	The converse epsilon coset of a set is the set. (Contributed by Peter Mazsa, 27-Jan-2019.)
⊢ (𝐴 ∈ 𝑉 → [𝐴]◡ E = 𝐴)
Theorem	extep 38624	Property of epsilon relation, see also extid 38651, extssr 38924 and the comment of df-ssr 38913. (Contributed by Peter Mazsa, 10-Jul-2019.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ([𝐴]◡ E = [𝐵]◡ E ↔ 𝐴 = 𝐵))
Theorem	disjeccnvep 38625	Property of the epsilon relation. (Contributed by Peter Mazsa, 27-Apr-2020.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (([𝐴]◡ E ∩ [𝐵]◡ E ) = ∅ ↔ (𝐴 ∩ 𝐵) = ∅))
Theorem	eccnvepres2 38626	The restricted converse epsilon coset of an element of the restriction is the element itself. (Contributed by Peter Mazsa, 16-Jul-2019.)
⊢ (𝐵 ∈ 𝐴 → [𝐵](◡ E ↾ 𝐴) = 𝐵)
Theorem	eccnvepres3 38627	Condition for a restricted converse epsilon coset of a set to be the set itself. (Contributed by Peter Mazsa, 11-May-2021.)
⊢ (𝐵 ∈ dom (◡ E ↾ 𝐴) → [𝐵](◡ E ↾ 𝐴) = 𝐵)
Theorem	eldmqsres 38628*	Elementhood in a restricted domain quotient set. (Contributed by Peter Mazsa, 21-Aug-2020.)
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ (dom (𝑅 ↾ 𝐴) / (𝑅 ↾ 𝐴)) ↔ ∃𝑢 ∈ 𝐴 (∃𝑥 𝑥 ∈ [𝑢]𝑅 ∧ 𝐵 = [𝑢]𝑅)))
Theorem	eldmqsres2 38629*	Elementhood in a restricted domain quotient set. (Contributed by Peter Mazsa, 22-Aug-2020.)
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ (dom (𝑅 ↾ 𝐴) / (𝑅 ↾ 𝐴)) ↔ ∃𝑢 ∈ 𝐴 ∃𝑥 ∈ [ 𝑢]𝑅𝐵 = [𝑢]𝑅))
Theorem	qsss1 38630	Subclass theorem for quotient sets. (Contributed by Peter Mazsa, 12-Sep-2020.)
⊢ (𝐴 ⊆ 𝐵 → (𝐴 / 𝐶) ⊆ (𝐵 / 𝐶))
Theorem	qseq1i 38631	Equality theorem for quotient set, inference form. (Contributed by Peter Mazsa, 3-Jun-2021.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 / 𝐶) = (𝐵 / 𝐶)
Theorem	brinxprnres 38632	Binary relation on a restriction. (Contributed by Peter Mazsa, 2-Jan-2019.)
⊢ (𝐶 ∈ 𝑉 → (𝐵(𝑅 ∩ (𝐴 × ran (𝑅 ↾ 𝐴)))𝐶 ↔ (𝐵 ∈ 𝐴 ∧ 𝐵𝑅𝐶)))
Theorem	inxprnres 38633*	Restriction of a class as a class of ordered pairs. (Contributed by Peter Mazsa, 2-Jan-2019.)
⊢ (𝑅 ∩ (𝐴 × ran (𝑅 ↾ 𝐴))) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑥𝑅𝑦)}
Theorem	dfres4 38634	Alternate definition of the restriction of a class. (Contributed by Peter Mazsa, 2-Jan-2019.)
⊢ (𝑅 ↾ 𝐴) = (𝑅 ∩ (𝐴 × ran (𝑅 ↾ 𝐴)))
Theorem	exan3 38635*	Equivalent expressions with existential quantification. (Contributed by Peter Mazsa, 10-Sep-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑢(𝐴 ∈ [𝑢]𝑅 ∧ 𝐵 ∈ [𝑢]𝑅) ↔ ∃𝑢(𝑢𝑅𝐴 ∧ 𝑢𝑅𝐵)))
Theorem	exanres 38636*	Equivalent expressions with existential quantification. (Contributed by Peter Mazsa, 2-May-2021.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (∃𝑢(𝑢(𝑅 ↾ 𝐴)𝐵 ∧ 𝑢(𝑆 ↾ 𝐴)𝐶) ↔ ∃𝑢 ∈ 𝐴 (𝑢𝑅𝐵 ∧ 𝑢𝑆𝐶)))
Theorem	exanres3 38637*	Equivalent expressions with restricted existential quantification. (Contributed by Peter Mazsa, 10-Sep-2021.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (∃𝑢 ∈ 𝐴 (𝐵 ∈ [𝑢]𝑅 ∧ 𝐶 ∈ [𝑢]𝑆) ↔ ∃𝑢 ∈ 𝐴 (𝑢𝑅𝐵 ∧ 𝑢𝑆𝐶)))
Theorem	exanres2 38638*	Equivalent expressions with existential quantification. (Contributed by Peter Mazsa, 10-Sep-2021.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (∃𝑢(𝑢(𝑅 ↾ 𝐴)𝐵 ∧ 𝑢(𝑆 ↾ 𝐴)𝐶) ↔ ∃𝑢 ∈ 𝐴 (𝐵 ∈ [𝑢]𝑅 ∧ 𝐶 ∈ [𝑢]𝑆)))
Theorem	cnvepres 38639*	Restricted converse epsilon relation as a class of ordered pairs. (Contributed by Peter Mazsa, 10-Feb-2018.)
⊢ (◡ E ↾ 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥)}
Theorem	eqrel2 38640*	Equality of relations. (Contributed by Peter Mazsa, 8-Mar-2019.)
⊢ ((Rel 𝐴 ∧ Rel 𝐵) → (𝐴 = 𝐵 ↔ ∀𝑥∀𝑦(𝑥𝐴𝑦 ↔ 𝑥𝐵𝑦)))
Theorem	rncnv 38641	Range of converse is the domain. (Contributed by Peter Mazsa, 12-Feb-2018.)
⊢ ran ◡𝐴 = dom 𝐴
Theorem	dfdm6 38642*	Alternate definition of domain. (Contributed by Peter Mazsa, 2-Mar-2018.)
⊢ dom 𝑅 = {𝑥 ∣ [𝑥]𝑅 ≠ ∅}
Theorem	dfrn6 38643*	Alternate definition of range. (Contributed by Peter Mazsa, 1-Aug-2018.)
⊢ ran 𝑅 = {𝑥 ∣ [𝑥]◡𝑅 ≠ ∅}
Theorem	rncnvepres 38644	The range of the restricted converse epsilon is the union of the restriction. (Contributed by Peter Mazsa, 11-Feb-2018.) (Revised by Peter Mazsa, 26-Sep-2021.)
⊢ ran (◡ E ↾ 𝐴) = ∪ 𝐴
Theorem	dmecd 38645	Equality of the coset of 𝐵 and the coset of 𝐶 implies equivalence of domain elementhood (equivalence is not necessary as opposed to ereldm 8690). (Contributed by Peter Mazsa, 9-Oct-2018.)
⊢ (𝜑 → dom 𝑅 = 𝐴)    &   ⊢ (𝜑 → [𝐵]𝑅 = [𝐶]𝑅)    ⇒   ⊢ (𝜑 → (𝐵 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴))
Theorem	dmec2d 38646	Equality of the coset of 𝐵 and the coset of 𝐶 implies equivalence of domain elementhood (equivalence is not necessary as opposed to ereldm 8690). (Contributed by Peter Mazsa, 12-Oct-2018.)
⊢ (𝜑 → [𝐵]𝑅 = [𝐶]𝑅)    ⇒   ⊢ (𝜑 → (𝐵 ∈ dom 𝑅 ↔ 𝐶 ∈ dom 𝑅))
Theorem	brid 38647	Property of the identity binary relation. (Contributed by Peter Mazsa, 18-Dec-2021.)
⊢ (𝐴 I 𝐵 ↔ 𝐵 I 𝐴)
Theorem	ideq2 38648	For sets, the identity binary relation is the same as equality. (Contributed by Peter Mazsa, 24-Jun-2020.) (Revised by Peter Mazsa, 18-Dec-2021.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 I 𝐵 ↔ 𝐴 = 𝐵))
Theorem	idresssidinxp 38649	Condition for the identity restriction to be a subclass of identity intersection with a Cartesian product. (Contributed by Peter Mazsa, 19-Jul-2018.)
⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴) ⊆ ( I ∩ (𝐴 × 𝐵)))
Theorem	idreseqidinxp 38650	Condition for the identity restriction to be equal to the identity intersection with a Cartesian product. (Contributed by Peter Mazsa, 19-Jul-2018.)
⊢ (𝐴 ⊆ 𝐵 → ( I ∩ (𝐴 × 𝐵)) = ( I ↾ 𝐴))
Theorem	extid 38651	Property of identity relation, see also extep 38624, extssr 38924 and the comment of df-ssr 38913. (Contributed by Peter Mazsa, 5-Jul-2019.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴]◡ I = [𝐵]◡ I ↔ 𝐴 = 𝐵))
Theorem	inxpss 38652*	Two ways to say that an intersection with a Cartesian product is a subclass. (Contributed by Peter Mazsa, 16-Jul-2019.)
⊢ ((𝑅 ∩ (𝐴 × 𝐵)) ⊆ 𝑆 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 → 𝑥𝑆𝑦))
Theorem	idinxpss 38653*	Two ways to say that an intersection of the identity relation with a Cartesian product is a subclass. (Contributed by Peter Mazsa, 16-Jul-2019.)
⊢ (( I ∩ (𝐴 × 𝐵)) ⊆ 𝑅 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 = 𝑦 → 𝑥𝑅𝑦))
Theorem	ref5 38654*	Two ways to say that an intersection of the identity relation with a Cartesian product is a subclass. (Contributed by Peter Mazsa, 12-Dec-2023.)
⊢ (( I ∩ (𝐴 × 𝐵)) ⊆ 𝑅 ↔ ∀𝑥 ∈ (𝐴 ∩ 𝐵)𝑥𝑅𝑥)
Theorem	inxpss3 38655*	Two ways to say that an intersection with a Cartesian product is a subclass (see also inxpss 38652). (Contributed by Peter Mazsa, 8-Mar-2019.)
⊢ (∀𝑥∀𝑦(𝑥(𝑅 ∩ (𝐴 × 𝐵))𝑦 → 𝑥(𝑆 ∩ (𝐴 × 𝐵))𝑦) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 → 𝑥𝑆𝑦))
Theorem	inxpss2 38656*	Two ways to say that intersections with Cartesian products are in a subclass relation. (Contributed by Peter Mazsa, 8-Mar-2019.)
⊢ ((𝑅 ∩ (𝐴 × 𝐵)) ⊆ (𝑆 ∩ (𝐴 × 𝐵)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 → 𝑥𝑆𝑦))
Theorem	inxpssidinxp 38657*	Two ways to say that intersections with Cartesian products are in a subclass relation, special case of inxpss2 38656. (Contributed by Peter Mazsa, 4-Jul-2019.)
⊢ ((𝑅 ∩ (𝐴 × 𝐵)) ⊆ ( I ∩ (𝐴 × 𝐵)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 → 𝑥 = 𝑦))
Theorem	idinxpssinxp 38658*	Two ways to say that intersections with Cartesian products are in a subclass relation, special case of inxpss2 38656. (Contributed by Peter Mazsa, 6-Mar-2019.)
⊢ (( I ∩ (𝐴 × 𝐵)) ⊆ (𝑅 ∩ (𝐴 × 𝐵)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 = 𝑦 → 𝑥𝑅𝑦))
Theorem	idinxpssinxp2 38659*	Identity intersection with a square Cartesian product in subclass relation with an intersection with the same Cartesian product. (Contributed by Peter Mazsa, 4-Mar-2019.) (Proof modification is discouraged.)
⊢ (( I ∩ (𝐴 × 𝐴)) ⊆ (𝑅 ∩ (𝐴 × 𝐴)) ↔ ∀𝑥 ∈ 𝐴 𝑥𝑅𝑥)
Theorem	idinxpssinxp3 38660	Identity intersection with a square Cartesian product in subclass relation with an intersection with the same Cartesian product. (Contributed by Peter Mazsa, 16-Mar-2019.) (Proof modification is discouraged.)
⊢ (( I ∩ (𝐴 × 𝐴)) ⊆ (𝑅 ∩ (𝐴 × 𝐴)) ↔ ( I ↾ 𝐴) ⊆ 𝑅)
Theorem	idinxpssinxp4 38661*	Identity intersection with a square Cartesian product in subclass relation with an intersection with the same Cartesian product (see also idinxpssinxp2 38659). (Contributed by Peter Mazsa, 8-Mar-2019.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 = 𝑦 → 𝑥𝑅𝑦) ↔ ∀𝑥 ∈ 𝐴 𝑥𝑅𝑥)
Theorem	relcnveq3 38662*	Two ways of saying a relation is symmetric. (Contributed by FL, 31-Aug-2009.)
⊢ (Rel 𝑅 → (𝑅 = ◡𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥)))
Theorem	relcnveq 38663	Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 23-Aug-2018.)
⊢ (Rel 𝑅 → (◡𝑅 ⊆ 𝑅 ↔ ◡𝑅 = 𝑅))
Theorem	relcnveq2 38664*	Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 28-Apr-2019.)
⊢ (Rel 𝑅 → (◡𝑅 = 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥)))
Theorem	relcnveq4 38665*	Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 28-Apr-2019.)
⊢ (Rel 𝑅 → (◡𝑅 ⊆ 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥)))
Theorem	qsresid 38666	Simplification of a special quotient set. (Contributed by Peter Mazsa, 2-Sep-2020.)
⊢ (𝐴 / (𝑅 ↾ 𝐴)) = (𝐴 / 𝑅)
Theorem	n0elqs 38667	Two ways of expressing that the empty set is not an element of a quotient set. (Contributed by Peter Mazsa, 5-Dec-2019.)
⊢ (¬ ∅ ∈ (𝐴 / 𝑅) ↔ 𝐴 ⊆ dom 𝑅)
Theorem	n0elqs2 38668	Two ways of expressing that the empty set is not an element of a quotient set. (Contributed by Peter Mazsa, 25-Jul-2021.)
⊢ (¬ ∅ ∈ (𝐴 / 𝑅) ↔ dom (𝑅 ↾ 𝐴) = 𝐴)
Theorem	rnresequniqs 38669	The range of a restriction is equal to the union of the quotient set. (Contributed by Peter Mazsa, 19-May-2018.)
⊢ ((𝑅 ↾ 𝐴) ∈ 𝑉 → ran (𝑅 ↾ 𝐴) = ∪ (𝐴 / 𝑅))
Theorem	n0el2 38670	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 38671	Sethood condition for the restricted converse epsilon relation. (Contributed by Peter Mazsa, 24-Sep-2018.)
⊢ (𝐴 ∈ 𝑉 → (◡ E ↾ 𝐴) ∈ V)
Theorem	cnvepima 38672	The image of converse epsilon. (Contributed by Peter Mazsa, 22-Mar-2023.)
⊢ (𝐴 ∈ 𝑉 → (◡ E “ 𝐴) = ∪ 𝐴)
Theorem	inex3 38673	Sufficient condition for the intersection relation to be a set. (Contributed by Peter Mazsa, 24-Nov-2019.)
⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → (𝐴 ∩ 𝐵) ∈ V)
Theorem	inxpex 38674	Sufficient condition for an intersection with a Cartesian product to be a set. (Contributed by Peter Mazsa, 10-May-2019.)
⊢ ((𝑅 ∈ 𝑊 ∨ (𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉)) → (𝑅 ∩ (𝐴 × 𝐵)) ∈ V)
Theorem	eqres 38675	Converting a class constant definition by restriction (like df-ers 39083 or df-parts 39203) into a binary relation. (Contributed by Peter Mazsa, 1-Oct-2018.)
⊢ 𝑅 = (𝑆 ↾ 𝐶)    ⇒   ⊢ (𝐵 ∈ 𝑉 → (𝐴𝑅𝐵 ↔ (𝐴 ∈ 𝐶 ∧ 𝐴𝑆𝐵)))
Theorem	brrabga 38676*	The law of concretion for operation class abstraction. (Contributed by Peter Mazsa, 24-Oct-2022.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓))    &   ⊢ 𝑅 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (⟨𝐴, 𝐵⟩𝑅𝐶 ↔ 𝜓))
Theorem	brcnvrabga 38677*	The law of concretion for the converse of operation class abstraction. (Contributed by Peter Mazsa, 25-Oct-2022.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓))    &   ⊢ 𝑅 = ◡{⟨⟨𝑦, 𝑧⟩, 𝑥⟩ ∣ 𝜑}    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴𝑅⟨𝐵, 𝐶⟩ ↔ 𝜓))
Theorem	opideq 38678	Equality conditions for ordered pairs ⟨𝐴, 𝐴⟩ and ⟨𝐵, 𝐵⟩. (Contributed by Peter Mazsa, 22-Jul-2019.) (Revised by Thierry Arnoux, 16-Feb-2022.)
⊢ (𝐴 ∈ 𝑉 → (⟨𝐴, 𝐴⟩ = ⟨𝐵, 𝐵⟩ ↔ 𝐴 = 𝐵))
Theorem	iss2 38679	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 38680*	Elementhood in a domain of a converse. (Contributed by Peter Mazsa, 25-May-2018.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom ◡𝑅 ↔ ∃𝑢 𝑢𝑅𝐴))
Theorem	dfrel5 38681	Alternate definition of the relation predicate. (Contributed by Peter Mazsa, 6-Nov-2018.)
⊢ (Rel 𝑅 ↔ (𝑅 ↾ dom 𝑅) = 𝑅)
Theorem	dfrel6 38682	Alternate definition of the relation predicate. (Contributed by Peter Mazsa, 14-Mar-2019.)
⊢ (Rel 𝑅 ↔ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) = 𝑅)
Theorem	cnvresrn 38683	Converse restricted to range is converse. (Contributed by Peter Mazsa, 3-Sep-2021.)
⊢ (◡𝑅 ↾ ran 𝑅) = ◡𝑅
Theorem	relssinxpdmrn 38684	Subset of restriction, special case. (Contributed by Peter Mazsa, 10-Apr-2023.)
⊢ (Rel 𝑅 → (𝑅 ⊆ (𝑆 ∩ (dom 𝑅 × ran 𝑅)) ↔ 𝑅 ⊆ 𝑆))
Theorem	cnvref4 38685	Two ways to say that a relation is a subclass. (Contributed by Peter Mazsa, 11-Apr-2023.)
⊢ (Rel 𝑅 → ((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ (𝑆 ∩ (dom 𝑅 × ran 𝑅)) ↔ 𝑅 ⊆ 𝑆))
Theorem	cnvref5 38686*	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 38687*	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 38688*	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 38689*	Equivalence of restricted universal quantifications. (Contributed by Peter Mazsa, 29-May-2018.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 = 𝑦 ∨ (𝐶 ∩ 𝐷) = ∅) ↔ ∀𝑥 ∈ 𝐴 ∀𝑧∀𝑦 ∈ 𝐵 ((𝑧 ∈ 𝐶 ∧ 𝑧 ∈ 𝐷) → 𝑥 = 𝑦))
Theorem	inecmo 38690*	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 38691*	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 38692*	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 38693	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 38694*	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 38695*	"At most one" can be restricted to the range. (Contributed by Peter Mazsa, 2-Feb-2026.)
⊢ (∀𝑥∃*𝑢 𝑢𝑅𝑥 ↔ ∀𝑥 ∈ ran 𝑅∃*𝑢 𝑢𝑅𝑥)
Theorem	ralrnmo 38696*	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 38697	Sethood of the domain quotient under sethood of 𝑅. (Contributed by Peter Mazsa, 2-Nov-2018.)
⊢ (𝑅 ∈ 𝑉 → (dom 𝑅 / 𝑅) ∈ V)
Theorem	raldmqsmo 38698*	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 38699*	Pull a restricted universal quantifier into the body (for ∃*). (Contributed by Peter Mazsa, 9-May-2019.)
⊢ (∀𝑦 ∈ 𝐵 ∃*𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦∃*𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 ∧ 𝜑))
Theorem	raldmqseu 38700*	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 𝑅 𝑢 = [𝑡]𝑅))