P. 376 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37501-37600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	tsan3 37501	A Tseitin axiom for logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → (𝜓 ∨ ¬ (𝜑 ∧ 𝜓)))
Theorem	tsna1 37502	A Tseitin axiom for logical incompatibility, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((¬ 𝜑 ∨ ¬ 𝜓) ∨ ¬ (𝜑 ⊼ 𝜓)))
Theorem	tsna2 37503	A Tseitin axiom for logical incompatibility, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → (𝜑 ∨ (𝜑 ⊼ 𝜓)))
Theorem	tsna3 37504	A Tseitin axiom for logical incompatibility, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → (𝜓 ∨ (𝜑 ⊼ 𝜓)))
Theorem	tsor1 37505	A Tseitin axiom for logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → ((𝜑 ∨ 𝜓) ∨ ¬ (𝜑 ∨ 𝜓)))
Theorem	tsor2 37506	A Tseitin axiom for logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → (¬ 𝜑 ∨ (𝜑 ∨ 𝜓)))
Theorem	tsor3 37507	A Tseitin axiom for logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → (¬ 𝜓 ∨ (𝜑 ∨ 𝜓)))
Theorem	ts3an1 37508	A Tseitin axiom for triple logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → ((¬ (𝜑 ∧ 𝜓) ∨ ¬ 𝜒) ∨ (𝜑 ∧ 𝜓 ∧ 𝜒)))
Theorem	ts3an2 37509	A Tseitin axiom for triple logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → ((𝜑 ∧ 𝜓) ∨ ¬ (𝜑 ∧ 𝜓 ∧ 𝜒)))
Theorem	ts3an3 37510	A Tseitin axiom for triple logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → (𝜒 ∨ ¬ (𝜑 ∧ 𝜓 ∧ 𝜒)))
Theorem	ts3or1 37511	A Tseitin axiom for triple logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → (((𝜑 ∨ 𝜓) ∨ 𝜒) ∨ ¬ (𝜑 ∨ 𝜓 ∨ 𝜒)))
Theorem	ts3or2 37512	A Tseitin axiom for triple logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → (¬ (𝜑 ∨ 𝜓) ∨ (𝜑 ∨ 𝜓 ∨ 𝜒)))
Theorem	ts3or3 37513	A Tseitin axiom for triple logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → (¬ 𝜒 ∨ (𝜑 ∨ 𝜓 ∨ 𝜒)))
21.23.3  Equality deductions A collection of theorems for commuting equalities (or biconditionals) with other constructs.
Theorem	iuneq2f 37514	Equality deduction for indexed union. (Contributed by Giovanni Mascellani, 9-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶)
Theorem	rabeq12f 37515	Equality deduction for restricted class abstraction. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓)) → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜓})
Theorem	csbeq12 37516	Equality deduction for substitution in class. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 𝐶 = 𝐷) → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐷)
Theorem	sbeqi 37517	Equality deduction for substitution. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ ((𝑥 = 𝑦 ∧ ∀𝑧(𝜑 ↔ 𝜓)) → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜓))
Theorem	ralbi12f 37518	Equality deduction for restricted universal quantification. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓)) → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓))
Theorem	oprabbi 37519	Equality deduction for class abstraction of nested ordered pairs. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ (∀𝑥∀𝑦∀𝑧(𝜑 ↔ 𝜓) → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓})
Theorem	mpobi123f 37520*	Equality deduction for maps-to notations with two arguments. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑦𝐶    &   ⊢ Ⅎ𝑦𝐷    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ Ⅎ𝑥𝐷    ⇒   ⊢ (((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝐸 = 𝐹) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐷 ↦ 𝐹))
Theorem	iuneq12f 37521	Equality deduction for indexed unions. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝐶 = 𝐷) → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷)
Theorem	iineq12f 37522	Equality deduction for indexed intersections. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝐶 = 𝐷) → ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐷)
Theorem	opabbi 37523	Equality deduction for class abstraction of ordered pairs. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ (∀𝑥∀𝑦(𝜑 ↔ 𝜓) → {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓})
Theorem	mptbi12f 37524	Equality deduction for maps-to notations. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝐷 = 𝐸) → (𝑥 ∈ 𝐴 ↦ 𝐷) = (𝑥 ∈ 𝐵 ↦ 𝐸))
21.23.4  Miscellanea Work in progress or things that do not belong anywhere else.
Theorem	orcomdd 37525	Commutativity of logic disjunction, in double deduction form. Should not be moved to main, see PR #3034 in Github. Use orcomd 868 instead. (Contributed by Giovanni Mascellani, 19-Mar-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝜑 → (𝜓 → (𝜒 ∨ 𝜃)))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜃 ∨ 𝜒)))
Theorem	scottexf 37526*	A version of scottex 9876 with nonfree variables instead of distinct variables. (Contributed by Giovanni Mascellani, 19-Aug-2018.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} ∈ V
Theorem	scott0f 37527*	A version of scott0 9877 with nonfree variables instead of distinct variables. (Contributed by Giovanni Mascellani, 19-Aug-2018.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 = ∅ ↔ {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} = ∅)
Theorem	scottn0f 37528*	A version of scott0f 37527 with inequalities instead of equalities. (Contributed by Giovanni Mascellani, 19-Aug-2018.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 ≠ ∅ ↔ {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} ≠ ∅)
Theorem	ac6s3f 37529*	Generalization of the Axiom of Choice to classes, with bound-variable hypothesis. (Contributed by Giovanni Mascellani, 19-Aug-2018.)
⊢ Ⅎ𝑦𝜓    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦𝜑 → ∃𝑓∀𝑥 ∈ 𝐴 𝜓)
Theorem	ac6s6 37530*	Generalization of the Axiom of Choice to classes, moving the existence condition in the consequent. (Contributed by Giovanni Mascellani, 19-Aug-2018.)
⊢ Ⅎ𝑦𝜓    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ∃𝑓∀𝑥 ∈ 𝐴 (∃𝑦𝜑 → 𝜓)
Theorem	ac6s6f 37531*	Generalization of the Axiom of Choice to classes, moving the existence condition in the consequent. (Contributed by Giovanni Mascellani, 20-Aug-2018.)
⊢ 𝐴 ∈ V    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓))    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ ∃𝑓∀𝑥 ∈ 𝐴 (∃𝑦𝜑 → 𝜓)
21.24  Mathbox for Peter Mazsa
21.24.1  Notations
Syntax	cxrn 37532	Extend the definition of a class to include the range Cartesian product class.
class (𝐴 ⋉ 𝐵)
Syntax	ccoss 37533	Extend the definition of a class to include the class of cosets by a class. (Read: the class of cosets by 𝑅.)
class ≀ 𝑅
Syntax	ccoels 37534	Extend the definition of a class to include the class of coelements on a class. (Read: the class of coelements on 𝐴.)
class ∼ 𝐴
Syntax	crels 37535	Extend the definition of a class to include the relation class.
class Rels
Syntax	cssr 37536	Extend the definition of a class to include the subset class.
class S
Syntax	crefs 37537	Extend the definition of a class to include the reflexivity class.
class Refs
Syntax	crefrels 37538	Extend the definition of a class to include the reflexive relations class.
class RefRels
Syntax	wrefrel 37539	Extend the definition of a wff to include the reflexive relation predicate. (Read: 𝑅 is a reflexive relation.)
wff RefRel 𝑅
Syntax	ccnvrefs 37540	Extend the definition of a class to include the converse reflexivity class.
class CnvRefs
Syntax	ccnvrefrels 37541	Extend the definition of a class to include the converse reflexive relations class.
class CnvRefRels
Syntax	wcnvrefrel 37542	Extend the definition of a wff to include the converse reflexive relation predicate. (Read: 𝑅 is a converse reflexive relation.)
wff CnvRefRel 𝑅
Syntax	csyms 37543	Extend the definition of a class to include the symmetry class.
class Syms
Syntax	csymrels 37544	Extend the definition of a class to include the symmetry relations class.
class SymRels
Syntax	wsymrel 37545	Extend the definition of a wff to include the symmetry relation predicate. (Read: 𝑅 is a symmetric relation.)
wff SymRel 𝑅
Syntax	ctrs 37546	Extend the definition of a class to include the transitivity class (but cf. the transitive class defined in df-tr 5256).
class Trs
Syntax	ctrrels 37547	Extend the definition of a class to include the transitive relations class.
class TrRels
Syntax	wtrrel 37548	Extend the definition of a wff to include the transitive relation predicate. (Read: 𝑅 is a transitive relation.)
wff TrRel 𝑅
Syntax	ceqvrels 37549	Extend the definition of a class to include the equivalence relations class.
class EqvRels
Syntax	weqvrel 37550	Extend the definition of a wff to include the equivalence relation predicate. (Read: 𝑅 is an equivalence relation.)
wff EqvRel 𝑅
Syntax	ccoeleqvrels 37551	Extend the definition of a class to include the coelement equivalence relations class.
class CoElEqvRels
Syntax	wcoeleqvrel 37552	Extend the definition of a wff to include the coelement equivalence relation predicate. (Read: the coelement equivalence relation on 𝐴.)
wff CoElEqvRel 𝐴
Syntax	credunds 37553	Extend the definition of a class to include the redundancy class.
class Redunds
Syntax	wredund 37554	Extend the definition of a wff to include the redundancy predicate. (Read: 𝐴 is redundant with respect to 𝐵 in 𝐶.)
wff 𝐴 Redund ⟨𝐵, 𝐶⟩
Syntax	wredundp 37555	Extend wff definition to include the redundancy operator for propositions.
wff redund (𝜑, 𝜓, 𝜒)
Syntax	cdmqss 37556	Extend the definition of a class to include the domain quotients class.
class DomainQss
Syntax	wdmqs 37557	Extend the definition of a wff to include the domain quotient predicate. (Read: the domain quotient of 𝑅 is 𝐴.)
wff 𝑅 DomainQs 𝐴
Syntax	cers 37558	Extend the definition of a class to include the equivalence relations on their domain quotients class.
class Ers
Syntax	werALTV 37559	Extend the definition of a wff to include the equivalence relation on its domain quotient predicate. (Read: 𝑅 is an equivalence relation on its domain quotient 𝐴.)
wff 𝑅 ErALTV 𝐴
Syntax	ccomembers 37560	Extend the definition of a class to include the comember equivalence relations class.
class CoMembErs
Syntax	wcomember 37561	Extend the definition of a wff to include the comember equivalence relation predicate. (Read: the comember equivalence relation on 𝐴, or, the restricted coelement equivalence relation on its domain quotient 𝐴.)
wff CoMembEr 𝐴
Syntax	cfunss 37562	Extend the definition of a class to include the function set class.
class Funss
Syntax	cfunsALTV 37563	Extend the definition of a class to include the functions class, i.e., the function relations class.
class FunsALTV
Syntax	wfunALTV 37564	Extend the definition of a wff to include the function predicate, i.e., the function relation predicate. (Read: 𝐹 is a function.)
wff FunALTV 𝐹
Syntax	cdisjss 37565	Extend the definition of a class to include the disjoint set class.
class Disjss
Syntax	cdisjs 37566	Extend the definition of a class to include the disjoints class, i.e., the disjoint relations class.
class Disjs
Syntax	wdisjALTV 37567	Extend the definition of a wff to include the disjoint predicate, i.e., the disjoint relation predicate. (Read: 𝑅 is a disjoint.)
wff Disj 𝑅
Syntax	celdisjs 37568	Extend the definition of a class to include the disjoint elements class, i.e., the disjoint element relations class.
class ElDisjs
Syntax	weldisj 37569	Extend the definition of a wff to include the disjoint element predicate, i.e., the disjoint element relation predicate. (Read: the elements of 𝐴 are disjoint.)
wff ElDisj 𝐴
Syntax	wantisymrel 37570	Extend the definition of a wff to include the antisymmetry relation predicate. (Read: 𝑅 is an antisymmetric relation.)
wff AntisymRel 𝑅
Syntax	cparts 37571	Extend the definition of a class to include the partitions class, i.e., the partition relations class.
class Parts
Syntax	wpart 37572	Extend the definition of a wff to include the partition predicate, i.e., the partition relation predicate. (Read: 𝐴 is a partition by 𝑅.)
wff 𝑅 Part 𝐴
Syntax	cmembparts 37573	Extend the definition of a class to include the member partitions class, i.e., the member partition relations class.
class MembParts
Syntax	wmembpart 37574	Extend the definition of a wff to include the member partition predicate, i.e., the member partition relation predicate. (Read: 𝐴 is a member partition.)
wff MembPart 𝐴
21.24.2  Preparatory theorems
Theorem	el2v1 37575	New way (elv 3472, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 23-Oct-2018.)
⊢ ((𝑥 ∈ V ∧ 𝜑) → 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	el3v 37576	New way (elv 3472, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. Inference forms (with ⊢ 𝐴 ∈ V, ⊢ 𝐵 ∈ V and ⊢ 𝐶 ∈ V hypotheses) of the general theorems (proving ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → assertions) may be superfluous. (Contributed by Peter Mazsa, 13-Oct-2018.)
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → 𝜑)    ⇒   ⊢ 𝜑
Theorem	el3v1 37577	New way (elv 3472, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 16-Oct-2020.)
⊢ ((𝑥 ∈ V ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
Theorem	el3v2 37578	New way (elv 3472, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 16-Oct-2020.)
⊢ ((𝜑 ∧ 𝑦 ∈ V ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
Theorem	el3v3 37579	New way (elv 3472, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 16-Oct-2020.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝑧 ∈ V) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
Theorem	el3v12 37580	New way (elv 3472, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 11-Jul-2021.)
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜒 → 𝜃)
Theorem	el3v13 37581	New way (elv 3472, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 11-Jul-2021.)
⊢ ((𝑥 ∈ V ∧ 𝜓 ∧ 𝑧 ∈ V) → 𝜃)    ⇒   ⊢ (𝜓 → 𝜃)
Theorem	el3v23 37582	New way (elv 3472, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 11-Jul-2021.)
⊢ ((𝜑 ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	anan 37583	Multiple commutations in conjunction. (Contributed by Peter Mazsa, 7-Mar-2020.)
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ ((𝜑 ∧ 𝜃) ∧ 𝜏)) ↔ ((𝜓 ∧ 𝜃) ∧ (𝜑 ∧ (𝜒 ∧ 𝜏))))
Theorem	triantru3 37584	A wff is equivalent to its conjunctions with truths. (Contributed by Peter Mazsa, 30-Nov-2018.)
⊢ 𝜑    &   ⊢ 𝜓    ⇒   ⊢ (𝜒 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒))
Theorem	bianbi 37585	Exchanging conjunction in a biconditional. (Contributed by Peter Mazsa, 31-Jul-2023.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))    &   ⊢ (𝜓 ↔ 𝜃)    ⇒   ⊢ (𝜑 ↔ (𝜃 ∧ 𝜒))
Theorem	bianim 37586	Exchanging conjunction in a biconditional. (Contributed by Peter Mazsa, 31-Jul-2023.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))    &   ⊢ (𝜒 → (𝜓 ↔ 𝜃))    ⇒   ⊢ (𝜑 ↔ (𝜃 ∧ 𝜒))
Theorem	biorfd 37587	A wff is equivalent to its disjunction with falsehood, deduction form. (Contributed by Peter Mazsa, 22-Aug-2023.)
⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → (𝜒 ↔ (𝜓 ∨ 𝜒)))
Theorem	eqbrtr 37588	Substitution of equal classes in binary relation. (Contributed by Peter Mazsa, 14-Jun-2024.)
⊢ ((𝐴 = 𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶)
Theorem	eqbrb 37589	Substitution of equal classes in a binary relation. (Contributed by Peter Mazsa, 14-Jun-2024.)
⊢ ((𝐴 = 𝐵 ∧ 𝐴𝑅𝐶) ↔ (𝐴 = 𝐵 ∧ 𝐵𝑅𝐶))
Theorem	eqeltr 37590	Substitution of equal classes into element relation. (Contributed by Peter Mazsa, 22-Jul-2017.)
⊢ ((𝐴 = 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)
Theorem	eqelb 37591	Substitution of equal classes into element relation. (Contributed by Peter Mazsa, 17-Jul-2019.)
⊢ ((𝐴 = 𝐵 ∧ 𝐴 ∈ 𝐶) ↔ (𝐴 = 𝐵 ∧ 𝐵 ∈ 𝐶))
Theorem	eqeqan2d 37592	Implication of introducing a new equality. (Contributed by Peter Mazsa, 17-Apr-2019.)
⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ ((𝐴 = 𝐵 ∧ 𝜑) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))
Theorem	suceqsneq 37593	One-to-one relationship between the successor operation and the singleton. (Contributed by Peter Mazsa, 31-Dec-2024.)
⊢ (𝐴 ∈ 𝑉 → (suc 𝐴 = suc 𝐵 ↔ {𝐴} = {𝐵}))
Theorem	sucdifsn2 37594	Absorption of union with a singleton by difference. (Contributed by Peter Mazsa, 24-Jul-2024.)
⊢ ((𝐴 ∪ {𝐴}) ∖ {𝐴}) = 𝐴
Theorem	sucdifsn 37595	The difference between the successor and the singleton of a class is the class. (Contributed by Peter Mazsa, 20-Sep-2024.)
⊢ (suc 𝐴 ∖ {𝐴}) = 𝐴
Theorem	disjresin 37596	The restriction to a disjoint is the empty class. (Contributed by Peter Mazsa, 24-Jul-2024.)
⊢ ((𝐴 ∩ 𝐵) = ∅ → (𝑅 ↾ (𝐴 ∩ 𝐵)) = ∅)
Theorem	disjresdisj 37597	The intersection of restrictions to disjoint is the empty class. (Contributed by Peter Mazsa, 24-Jul-2024.)
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝑅 ↾ 𝐴) ∩ (𝑅 ↾ 𝐵)) = ∅)
Theorem	disjresdif 37598	The difference between restrictions to disjoint is the first restriction. (Contributed by Peter Mazsa, 24-Jul-2024.)
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝑅 ↾ 𝐴) ∖ (𝑅 ↾ 𝐵)) = (𝑅 ↾ 𝐴))
Theorem	disjresundif 37599	Lemma for ressucdifsn2 37600. (Contributed by Peter Mazsa, 24-Jul-2024.)
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝑅 ↾ (𝐴 ∪ 𝐵)) ∖ (𝑅 ↾ 𝐵)) = (𝑅 ↾ 𝐴))
Theorem	ressucdifsn2 37600	The difference between restrictions to the successor and the singleton of a class is the restriction to the class, see ressucdifsn 37601. (Contributed by Peter Mazsa, 24-Jul-2024.)
⊢ ((𝑅 ↾ (𝐴 ∪ {𝐴})) ∖ (𝑅 ↾ {𝐴})) = (𝑅 ↾ 𝐴)