P. 364 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36301-36400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	el3v3 36301	New way (elv 3428, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 16-Oct-2020.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝑧 ∈ V) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
Theorem	el3v12 36302	New way (elv 3428, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 11-Jul-2021.)
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜒 → 𝜃)
Theorem	el3v13 36303	New way (elv 3428, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 11-Jul-2021.)
⊢ ((𝑥 ∈ V ∧ 𝜓 ∧ 𝑧 ∈ V) → 𝜃)    ⇒   ⊢ (𝜓 → 𝜃)
Theorem	el3v23 36304	New way (elv 3428, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 11-Jul-2021.)
⊢ ((𝜑 ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	an2anr 36305	Double commutation in conjunction. (Contributed by Peter Mazsa, 27-Jun-2019.)
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜓 ∧ 𝜑) ∧ (𝜃 ∧ 𝜒)))
Theorem	anan 36306	Multiple commutations in conjunction. (Contributed by Peter Mazsa, 7-Mar-2020.)
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ ((𝜑 ∧ 𝜃) ∧ 𝜏)) ↔ ((𝜓 ∧ 𝜃) ∧ (𝜑 ∧ (𝜒 ∧ 𝜏))))
Theorem	triantru3 36307	A wff is equivalent to its conjunctions with truths. (Contributed by Peter Mazsa, 30-Nov-2018.)
⊢ 𝜑    &   ⊢ 𝜓    ⇒   ⊢ (𝜒 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒))
Theorem	eqeltr 36308	Substitution of equal classes into elementhood relation. (Contributed by Peter Mazsa, 22-Jul-2017.)
⊢ ((𝐴 = 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)
Theorem	eqelb 36309	Substitution of equal classes into elementhood relation. (Contributed by Peter Mazsa, 17-Jul-2019.)
⊢ ((𝐴 = 𝐵 ∧ 𝐴 ∈ 𝐶) ↔ (𝐴 = 𝐵 ∧ 𝐵 ∈ 𝐶))
Theorem	eqeqan2d 36310	Implication of introducing a new equality. (Contributed by Peter Mazsa, 17-Apr-2019.)
⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ ((𝐴 = 𝐵 ∧ 𝜑) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))
Theorem	inres2 36311	Two ways of expressing the restriction of an intersection. (Contributed by Peter Mazsa, 5-Jun-2021.)
⊢ ((𝑅 ↾ 𝐴) ∩ 𝑆) = ((𝑅 ∩ 𝑆) ↾ 𝐴)
Theorem	coideq 36312	Equality theorem for composition of two classes. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐴) = (𝐵 ∘ 𝐵))
Theorem	nexmo1 36313	If there is no case where wff is true, it is true for at most one case. (Contributed by Peter Mazsa, 27-Sep-2021.)
⊢ (¬ ∃𝑥𝜑 → ∃*𝑥𝜑)
Theorem	3albii 36314	Inference adding three universal quantifiers to both sides of an equivalence. (Contributed by Peter Mazsa, 10-Aug-2018.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∀𝑥∀𝑦∀𝑧𝜑 ↔ ∀𝑥∀𝑦∀𝑧𝜓)
Theorem	3ralbii 36315	Inference adding three restricted universal quantifiers to both sides of an equivalence. (Contributed by Peter Mazsa, 25-Jul-2019.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓)
Theorem	ssrabi 36316	Inference of restricted abstraction subclass from implication. (Contributed by Peter Mazsa, 26-Oct-2022.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓}
Theorem	rabbieq 36317	Equivalent wff's correspond to restricted class abstractions which are equal with the same class. (Contributed by Peter Mazsa, 8-Jul-2019.)
⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜑}    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜓}
Theorem	rabimbieq 36318	Restricted equivalent wff's correspond to restricted class abstractions which are equal with the same class. (Contributed by Peter Mazsa, 22-Jul-2021.)
⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜑}    &   ⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜓}
Theorem	abeqin 36319*	Intersection with class abstraction. (Contributed by Peter Mazsa, 21-Jul-2021.)
⊢ 𝐴 = (𝐵 ∩ 𝐶)    &   ⊢ 𝐵 = {𝑥 ∣ 𝜑}    ⇒   ⊢ 𝐴 = {𝑥 ∈ 𝐶 ∣ 𝜑}
Theorem	abeqinbi 36320*	Intersection with class abstraction and equivalent wff's. (Contributed by Peter Mazsa, 21-Jul-2021.)
⊢ 𝐴 = (𝐵 ∩ 𝐶)    &   ⊢ 𝐵 = {𝑥 ∣ 𝜑}    &   ⊢ (𝑥 ∈ 𝐶 → (𝜑 ↔ 𝜓))    ⇒   ⊢ 𝐴 = {𝑥 ∈ 𝐶 ∣ 𝜓}
Theorem	rabeqel 36321*	Class element of a restricted class abstraction. (Contributed by Peter Mazsa, 24-Jul-2021.)
⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜑}    &   ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐶 ∈ 𝐵 ↔ (𝜓 ∧ 𝐶 ∈ 𝐴))
Theorem	eqrelf 36322*	The equality connective between relations. (Contributed by Peter Mazsa, 25-Jun-2019.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    ⇒   ⊢ ((Rel 𝐴 ∧ Rel 𝐵) → (𝐴 = 𝐵 ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐵)))
Theorem	releleccnv 36323	Elementhood in a converse 𝑅-coset when 𝑅 is a relation. (Contributed by Peter Mazsa, 9-Dec-2018.)
⊢ (Rel 𝑅 → (𝐴 ∈ [𝐵]◡𝑅 ↔ 𝐴𝑅𝐵))
Theorem	releccnveq 36324*	Equality of converse 𝑅-coset and converse 𝑆-coset when 𝑅 and 𝑆 are relations. (Contributed by Peter Mazsa, 27-Jul-2019.)
⊢ ((Rel 𝑅 ∧ Rel 𝑆) → ([𝐴]◡𝑅 = [𝐵]◡𝑆 ↔ ∀𝑥(𝑥𝑅𝐴 ↔ 𝑥𝑆𝐵)))
Theorem	opelvvdif 36325	Negated elementhood of ordered pair. (Contributed by Peter Mazsa, 14-Jan-2019.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ ∈ ((V × V) ∖ 𝑅) ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ 𝑅))
Theorem	vvdifopab 36326*	Ordered-pair class abstraction defined by a negation. (Contributed by Peter Mazsa, 25-Jun-2019.)
⊢ ((V × V) ∖ {⟨𝑥, 𝑦⟩ ∣ 𝜑}) = {⟨𝑥, 𝑦⟩ ∣ ¬ 𝜑}
Theorem	brvdif 36327	Binary relation with universal complement is the negation of the relation. (Contributed by Peter Mazsa, 1-Jul-2018.)
⊢ (𝐴(V ∖ 𝑅)𝐵 ↔ ¬ 𝐴𝑅𝐵)
Theorem	brvdif2 36328	Binary relation with universal complement. (Contributed by Peter Mazsa, 14-Jul-2018.)
⊢ (𝐴(V ∖ 𝑅)𝐵 ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
Theorem	brvvdif 36329	Binary relation with the complement under the universal class of ordered pairs. (Contributed by Peter Mazsa, 9-Nov-2018.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴((V × V) ∖ 𝑅)𝐵 ↔ ¬ 𝐴𝑅𝐵))
Theorem	brvbrvvdif 36330	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 36331	The converse of the binary epsilon relation. (Contributed by Peter Mazsa, 30-Jan-2018.)
⊢ (𝐴 ∈ 𝑉 → (𝐴◡ E 𝐵 ↔ 𝐵 ∈ 𝐴))
Theorem	elecALTV 36332	Elementhood in the 𝑅-coset of 𝐴. Theorem 72 of [Suppes] p. 82. (I think we should replace elecg 8499 with this original form of Suppes. Peter Mazsa). (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐵 ∈ [𝐴]𝑅 ↔ 𝐴𝑅𝐵))
Theorem	brcnvepres 36333	Restricted converse epsilon binary relation. (Contributed by Peter Mazsa, 10-Feb-2018.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵(◡ E ↾ 𝐴)𝐶 ↔ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵)))
Theorem	brres2 36334	Binary relation on a restriction. (Contributed by Peter Mazsa, 2-Jan-2019.) (Revised by Peter Mazsa, 16-Dec-2021.)
⊢ (𝐵(𝑅 ↾ 𝐴)𝐶 ↔ 𝐵(𝑅 ∩ (𝐴 × ran (𝑅 ↾ 𝐴)))𝐶)
Theorem	eldmres 36335*	Elementhood in the domain of a restriction. (Contributed by Peter Mazsa, 9-Jan-2019.)
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ dom (𝑅 ↾ 𝐴) ↔ (𝐵 ∈ 𝐴 ∧ ∃𝑦 𝐵𝑅𝑦)))
Theorem	eldm4 36336*	Elementhood in a domain. (Contributed by Peter Mazsa, 24-Oct-2018.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom 𝑅 ↔ ∃𝑦 𝑦 ∈ [𝐴]𝑅))
Theorem	eldmres2 36337*	Elementhood in the domain of a restriction. (Contributed by Peter Mazsa, 21-Aug-2020.)
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ dom (𝑅 ↾ 𝐴) ↔ (𝐵 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ [𝐵]𝑅)))
Theorem	eceq1i 36338	Equality theorem for 𝐶-coset of 𝐴 and 𝐶-coset of 𝐵, inference version. (Contributed by Peter Mazsa, 11-May-2021.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ [𝐴]𝐶 = [𝐵]𝐶
Theorem	elecres 36339	Elementhood in the restricted coset of 𝐵. (Contributed by Peter Mazsa, 21-Sep-2018.)
⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ [𝐵](𝑅 ↾ 𝐴) ↔ (𝐵 ∈ 𝐴 ∧ 𝐵𝑅𝐶)))
Theorem	ecres 36340*	Restricted coset of 𝐵. (Contributed by Peter Mazsa, 9-Dec-2018.)
⊢ [𝐵](𝑅 ↾ 𝐴) = {𝑥 ∣ (𝐵 ∈ 𝐴 ∧ 𝐵𝑅𝑥)}
Theorem	ecres2 36341	The restricted coset of 𝐵 when 𝐵 is an element of the restriction. (Contributed by Peter Mazsa, 16-Oct-2018.)
⊢ (𝐵 ∈ 𝐴 → [𝐵](𝑅 ↾ 𝐴) = [𝐵]𝑅)
Theorem	eccnvepres 36342*	Restricted converse epsilon coset of 𝐵. (Contributed by Peter Mazsa, 11-Feb-2018.) (Revised by Peter Mazsa, 21-Oct-2021.)
⊢ (𝐵 ∈ 𝑉 → [𝐵](◡ E ↾ 𝐴) = {𝑥 ∈ 𝐵 ∣ 𝐵 ∈ 𝐴})
Theorem	eleccnvep 36343	Elementhood in the converse epsilon coset of 𝐴 is elementhood in 𝐴. (Contributed by Peter Mazsa, 27-Jan-2019.)
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ [𝐴]◡ E ↔ 𝐵 ∈ 𝐴))
Theorem	eccnvep 36344	The converse epsilon coset of a set is the set. (Contributed by Peter Mazsa, 27-Jan-2019.)
⊢ (𝐴 ∈ 𝑉 → [𝐴]◡ E = 𝐴)
Theorem	extep 36345	Property of epsilon relation, see also extid 36373, extssr 36554 and the comment of df-ssr 36543. (Contributed by Peter Mazsa, 10-Jul-2019.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ([𝐴]◡ E = [𝐵]◡ E ↔ 𝐴 = 𝐵))
Theorem	eccnvepres2 36346	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 36347	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 36348*	Elementhood in a restricted domain quotient set. (Contributed by Peter Mazsa, 21-Aug-2020.)
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ (dom (𝑅 ↾ 𝐴) / (𝑅 ↾ 𝐴)) ↔ ∃𝑢 ∈ 𝐴 (∃𝑥 𝑥 ∈ [𝑢]𝑅 ∧ 𝐵 = [𝑢]𝑅)))
Theorem	eldmqsres2 36349*	Elementhood in a restricted domain quotient set. (Contributed by Peter Mazsa, 22-Aug-2020.)
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ (dom (𝑅 ↾ 𝐴) / (𝑅 ↾ 𝐴)) ↔ ∃𝑢 ∈ 𝐴 ∃𝑥 ∈ [ 𝑢]𝑅𝐵 = [𝑢]𝑅))
Theorem	qsss1 36350	Subclass theorem for quotient sets. (Contributed by Peter Mazsa, 12-Sep-2020.)
⊢ (𝐴 ⊆ 𝐵 → (𝐴 / 𝐶) ⊆ (𝐵 / 𝐶))
Theorem	qseq1i 36351	Equality theorem for quotient set, inference form. (Contributed by Peter Mazsa, 3-Jun-2021.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 / 𝐶) = (𝐵 / 𝐶)
Theorem	qseq1d 36352	Equality theorem for quotient set, deduction form. (Contributed by Peter Mazsa, 27-May-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐶) = (𝐵 / 𝐶))
Theorem	brinxprnres 36353	Binary relation on a restriction. (Contributed by Peter Mazsa, 2-Jan-2019.)
⊢ (𝐶 ∈ 𝑉 → (𝐵(𝑅 ∩ (𝐴 × ran (𝑅 ↾ 𝐴)))𝐶 ↔ (𝐵 ∈ 𝐴 ∧ 𝐵𝑅𝐶)))
Theorem	inxprnres 36354*	Restriction of a class as a class of ordered pairs. (Contributed by Peter Mazsa, 2-Jan-2019.)
⊢ (𝑅 ∩ (𝐴 × ran (𝑅 ↾ 𝐴))) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑥𝑅𝑦)}
Theorem	dfres4 36355	Alternate definition of the restriction of a class. (Contributed by Peter Mazsa, 2-Jan-2019.)
⊢ (𝑅 ↾ 𝐴) = (𝑅 ∩ (𝐴 × ran (𝑅 ↾ 𝐴)))
Theorem	exan3 36356*	Equivalent expressions with existential quantification. (Contributed by Peter Mazsa, 10-Sep-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑢(𝐴 ∈ [𝑢]𝑅 ∧ 𝐵 ∈ [𝑢]𝑅) ↔ ∃𝑢(𝑢𝑅𝐴 ∧ 𝑢𝑅𝐵)))
Theorem	exanres 36357*	Equivalent expressions with existential quantification. (Contributed by Peter Mazsa, 2-May-2021.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (∃𝑢(𝑢(𝑅 ↾ 𝐴)𝐵 ∧ 𝑢(𝑆 ↾ 𝐴)𝐶) ↔ ∃𝑢 ∈ 𝐴 (𝑢𝑅𝐵 ∧ 𝑢𝑆𝐶)))
Theorem	exanres3 36358*	Equivalent expressions with restricted existential quantification. (Contributed by Peter Mazsa, 10-Sep-2021.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (∃𝑢 ∈ 𝐴 (𝐵 ∈ [𝑢]𝑅 ∧ 𝐶 ∈ [𝑢]𝑆) ↔ ∃𝑢 ∈ 𝐴 (𝑢𝑅𝐵 ∧ 𝑢𝑆𝐶)))
Theorem	exanres2 36359*	Equivalent expressions with existential quantification. (Contributed by Peter Mazsa, 10-Sep-2021.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (∃𝑢(𝑢(𝑅 ↾ 𝐴)𝐵 ∧ 𝑢(𝑆 ↾ 𝐴)𝐶) ↔ ∃𝑢 ∈ 𝐴 (𝐵 ∈ [𝑢]𝑅 ∧ 𝐶 ∈ [𝑢]𝑆)))
Theorem	cnvepres 36360*	Restricted converse epsilon relation as a class of ordered pairs. (Contributed by Peter Mazsa, 10-Feb-2018.)
⊢ (◡ E ↾ 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥)}
Theorem	ssrel3 36361*	Subclass relation in another form when the subclass is a relation. (Contributed by Peter Mazsa, 16-Feb-2019.)
⊢ (Rel 𝐴 → (𝐴 ⊆ 𝐵 ↔ ∀𝑥∀𝑦(𝑥𝐴𝑦 → 𝑥𝐵𝑦)))
Theorem	eqrel2 36362*	Equality of relations. (Contributed by Peter Mazsa, 8-Mar-2019.)
⊢ ((Rel 𝐴 ∧ Rel 𝐵) → (𝐴 = 𝐵 ↔ ∀𝑥∀𝑦(𝑥𝐴𝑦 ↔ 𝑥𝐵𝑦)))
Theorem	rncnv 36363	Range of converse is the domain. (Contributed by Peter Mazsa, 12-Feb-2018.)
⊢ ran ◡𝐴 = dom 𝐴
Theorem	dfdm6 36364*	Alternate definition of domain. (Contributed by Peter Mazsa, 2-Mar-2018.)
⊢ dom 𝑅 = {𝑥 ∣ [𝑥]𝑅 ≠ ∅}
Theorem	dfrn6 36365*	Alternate definition of range. (Contributed by Peter Mazsa, 1-Aug-2018.)
⊢ ran 𝑅 = {𝑥 ∣ [𝑥]◡𝑅 ≠ ∅}
Theorem	rncnvepres 36366	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 36367	Equality of the coset of 𝐵 and the coset of 𝐶 implies equivalence of domain elementhood (equivalence is not necessary as opposed to ereldm 8504). (Contributed by Peter Mazsa, 9-Oct-2018.)
⊢ (𝜑 → dom 𝑅 = 𝐴)    &   ⊢ (𝜑 → [𝐵]𝑅 = [𝐶]𝑅)    ⇒   ⊢ (𝜑 → (𝐵 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴))
Theorem	dmec2d 36368	Equality of the coset of 𝐵 and the coset of 𝐶 implies equivalence of domain elementhood (equivalence is not necessary as opposed to ereldm 8504). (Contributed by Peter Mazsa, 12-Oct-2018.)
⊢ (𝜑 → [𝐵]𝑅 = [𝐶]𝑅)    ⇒   ⊢ (𝜑 → (𝐵 ∈ dom 𝑅 ↔ 𝐶 ∈ dom 𝑅))
Theorem	brid 36369	Property of the identity binary relation. (Contributed by Peter Mazsa, 18-Dec-2021.)
⊢ (𝐴 I 𝐵 ↔ 𝐵 I 𝐴)
Theorem	ideq2 36370	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 36371	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 36372	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 36373	Property of identity relation, see also extep 36345, extssr 36554 and the comment of df-ssr 36543. (Contributed by Peter Mazsa, 5-Jul-2019.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴]◡ I = [𝐵]◡ I ↔ 𝐴 = 𝐵))
Theorem	inxpss 36374*	Two ways to say that an intersection with a Cartesian product is a subclass. (Contributed by Peter Mazsa, 16-Jul-2019.)
⊢ ((𝑅 ∩ (𝐴 × 𝐵)) ⊆ 𝑆 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 → 𝑥𝑆𝑦))
Theorem	idinxpss 36375*	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	inxpss3 36376*	Two ways to say that an intersection with a Cartesian product is a subclass (see also inxpss 36374). (Contributed by Peter Mazsa, 8-Mar-2019.)
⊢ (∀𝑥∀𝑦(𝑥(𝑅 ∩ (𝐴 × 𝐵))𝑦 → 𝑥(𝑆 ∩ (𝐴 × 𝐵))𝑦) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 → 𝑥𝑆𝑦))
Theorem	inxpss2 36377*	Two ways to say that intersections with Cartesian products are in a subclass relation. (Contributed by Peter Mazsa, 8-Mar-2019.)
⊢ ((𝑅 ∩ (𝐴 × 𝐵)) ⊆ (𝑆 ∩ (𝐴 × 𝐵)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 → 𝑥𝑆𝑦))
Theorem	inxpssidinxp 36378*	Two ways to say that intersections with Cartesian products are in a subclass relation, special case of inxpss2 36377. (Contributed by Peter Mazsa, 4-Jul-2019.)
⊢ ((𝑅 ∩ (𝐴 × 𝐵)) ⊆ ( I ∩ (𝐴 × 𝐵)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 → 𝑥 = 𝑦))
Theorem	idinxpssinxp 36379*	Two ways to say that intersections with Cartesian products are in a subclass relation, special case of inxpss2 36377. (Contributed by Peter Mazsa, 6-Mar-2019.)
⊢ (( I ∩ (𝐴 × 𝐵)) ⊆ (𝑅 ∩ (𝐴 × 𝐵)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 = 𝑦 → 𝑥𝑅𝑦))
Theorem	idinxpssinxp2 36380*	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 36381	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 36382*	Identity intersection with a square Cartesian product in subclass relation with an intersection with the same Cartesian product (see also idinxpssinxp2 36380). (Contributed by Peter Mazsa, 8-Mar-2019.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 = 𝑦 → 𝑥𝑅𝑦) ↔ ∀𝑥 ∈ 𝐴 𝑥𝑅𝑥)
Theorem	relcnveq3 36383*	Two ways of saying a relation is symmetric. (Contributed by FL, 31-Aug-2009.)
⊢ (Rel 𝑅 → (𝑅 = ◡𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥)))
Theorem	relcnveq 36384	Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 23-Aug-2018.)
⊢ (Rel 𝑅 → (◡𝑅 ⊆ 𝑅 ↔ ◡𝑅 = 𝑅))
Theorem	relcnveq2 36385*	Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 28-Apr-2019.)
⊢ (Rel 𝑅 → (◡𝑅 = 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥)))
Theorem	relcnveq4 36386*	Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 28-Apr-2019.)
⊢ (Rel 𝑅 → (◡𝑅 ⊆ 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥)))
Theorem	qsresid 36387	Simplification of a special quotient set. (Contributed by Peter Mazsa, 2-Sep-2020.)
⊢ (𝐴 / (𝑅 ↾ 𝐴)) = (𝐴 / 𝑅)
Theorem	n0elqs 36388	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 36389	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	ecex2 36390	Condition for a coset to be a set. (Contributed by Peter Mazsa, 4-May-2019.)
⊢ ((𝑅 ↾ 𝐴) ∈ 𝑉 → (𝐵 ∈ 𝐴 → [𝐵]𝑅 ∈ V))
Theorem	uniqsALTV 36391	The union of a quotient set, like uniqs 8524 but with a weaker antecedent: only the restricion of 𝑅 by 𝐴 needs to be a set, not 𝑅 itself, see e.g. cnvepima 36399. (Contributed by Peter Mazsa, 20-Jun-2019.)
⊢ ((𝑅 ↾ 𝐴) ∈ 𝑉 → ∪ (𝐴 / 𝑅) = (𝑅 “ 𝐴))
Theorem	imaexALTV 36392	Existence of an image of a class. Theorem 3.17 of [Monk1] p. 39. (cf. imaexg 7736) with weakened antecedent: only the restricion of 𝐴 by a set needs to be a set, not 𝐴 itself, see e.g. cnvepimaex 36398. (Contributed by Peter Mazsa, 22-Feb-2023.) (Proof modification is discouraged.)
⊢ ((𝐴 ∈ 𝑉 ∨ ((𝐴 ↾ 𝐵) ∈ 𝑊 ∧ 𝐵 ∈ 𝑋)) → (𝐴 “ 𝐵) ∈ V)
Theorem	ecexALTV 36393	Existence of a coset, like ecexg 8460 but with a weaker antecedent: only the restricion of 𝑅 by the singleton of 𝐴 needs to be a set, not 𝑅 itself, see e.g. eccnvepex 36397. (Contributed by Peter Mazsa, 22-Feb-2023.)
⊢ ((𝑅 ↾ {𝐴}) ∈ 𝑉 → [𝐴]𝑅 ∈ V)
Theorem	rnresequniqs 36394	The range of a restriction is equal to the union of the quotient set. (Contributed by Peter Mazsa, 19-May-2018.)
⊢ ((𝑅 ↾ 𝐴) ∈ 𝑉 → ran (𝑅 ↾ 𝐴) = ∪ (𝐴 / 𝑅))
Theorem	n0el2 36395	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 36396	Sethood condition for the restricted converse epsilon relation. (Contributed by Peter Mazsa, 24-Sep-2018.)
⊢ (𝐴 ∈ 𝑉 → (◡ E ↾ 𝐴) ∈ V)
Theorem	eccnvepex 36397	The converse epsilon coset exists. (Contributed by Peter Mazsa, 22-Mar-2023.)
⊢ [𝐴]◡ E ∈ V
Theorem	cnvepimaex 36398	The image of converse epsilon exists, proof via imaexALTV 36392 (see also cnvepima 36399 and uniexg 7571 for alternate way). (Contributed by Peter Mazsa, 22-Mar-2023.)
⊢ (𝐴 ∈ 𝑉 → (◡ E “ 𝐴) ∈ V)
Theorem	cnvepima 36399	The image of converse epsilon. (Contributed by Peter Mazsa, 22-Mar-2023.)
⊢ (𝐴 ∈ 𝑉 → (◡ E “ 𝐴) = ∪ 𝐴)
Theorem	inex3 36400	Sufficient condition for the intersection relation to be a set. (Contributed by Peter Mazsa, 24-Nov-2019.)
⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → (𝐴 ∩ 𝐵) ∈ V)