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	tsbi2 36301	A Tseitin axiom for logical biconditional, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((𝜑 ∨ 𝜓) ∨ (𝜑 ↔ 𝜓)))
Theorem	tsbi3 36302	A Tseitin axiom for logical biconditional, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((𝜑 ∨ ¬ 𝜓) ∨ ¬ (𝜑 ↔ 𝜓)))
Theorem	tsbi4 36303	A Tseitin axiom for logical biconditional, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((¬ 𝜑 ∨ 𝜓) ∨ ¬ (𝜑 ↔ 𝜓)))
Theorem	tsxo1 36304	A Tseitin axiom for logical exclusive disjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((¬ 𝜑 ∨ ¬ 𝜓) ∨ ¬ (𝜑 ⊻ 𝜓)))
Theorem	tsxo2 36305	A Tseitin axiom for logical exclusive disjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((𝜑 ∨ 𝜓) ∨ ¬ (𝜑 ⊻ 𝜓)))
Theorem	tsxo3 36306	A Tseitin axiom for logical exclusive disjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((𝜑 ∨ ¬ 𝜓) ∨ (𝜑 ⊻ 𝜓)))
Theorem	tsxo4 36307	A Tseitin axiom for logical exclusive disjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((¬ 𝜑 ∨ 𝜓) ∨ (𝜑 ⊻ 𝜓)))
Theorem	tsan1 36308	A Tseitin axiom for logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((¬ 𝜑 ∨ ¬ 𝜓) ∨ (𝜑 ∧ 𝜓)))
Theorem	tsan2 36309	A Tseitin axiom for logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → (𝜑 ∨ ¬ (𝜑 ∧ 𝜓)))
Theorem	tsan3 36310	A Tseitin axiom for logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → (𝜓 ∨ ¬ (𝜑 ∧ 𝜓)))
Theorem	tsna1 36311	A Tseitin axiom for logical incompatibility, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((¬ 𝜑 ∨ ¬ 𝜓) ∨ ¬ (𝜑 ⊼ 𝜓)))
Theorem	tsna2 36312	A Tseitin axiom for logical incompatibility, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → (𝜑 ∨ (𝜑 ⊼ 𝜓)))
Theorem	tsna3 36313	A Tseitin axiom for logical incompatibility, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → (𝜓 ∨ (𝜑 ⊼ 𝜓)))
Theorem	tsor1 36314	A Tseitin axiom for logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → ((𝜑 ∨ 𝜓) ∨ ¬ (𝜑 ∨ 𝜓)))
Theorem	tsor2 36315	A Tseitin axiom for logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → (¬ 𝜑 ∨ (𝜑 ∨ 𝜓)))
Theorem	tsor3 36316	A Tseitin axiom for logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → (¬ 𝜓 ∨ (𝜑 ∨ 𝜓)))
Theorem	ts3an1 36317	A Tseitin axiom for triple logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → ((¬ (𝜑 ∧ 𝜓) ∨ ¬ 𝜒) ∨ (𝜑 ∧ 𝜓 ∧ 𝜒)))
Theorem	ts3an2 36318	A Tseitin axiom for triple logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → ((𝜑 ∧ 𝜓) ∨ ¬ (𝜑 ∧ 𝜓 ∧ 𝜒)))
Theorem	ts3an3 36319	A Tseitin axiom for triple logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → (𝜒 ∨ ¬ (𝜑 ∧ 𝜓 ∧ 𝜒)))
Theorem	ts3or1 36320	A Tseitin axiom for triple logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → (((𝜑 ∨ 𝜓) ∨ 𝜒) ∨ ¬ (𝜑 ∨ 𝜓 ∨ 𝜒)))
Theorem	ts3or2 36321	A Tseitin axiom for triple logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → (¬ (𝜑 ∨ 𝜓) ∨ (𝜑 ∨ 𝜓 ∨ 𝜒)))
Theorem	ts3or3 36322	A Tseitin axiom for triple logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → (¬ 𝜒 ∨ (𝜑 ∨ 𝜓 ∨ 𝜒)))
20.21.3  Equality deductions A collection of theorems for commuting equalities (or biconditionals) with other constructs.
Theorem	iuneq2f 36323	Equality deduction for indexed union. (Contributed by Giovanni Mascellani, 9-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶)
Theorem	rabeq12f 36324	Equality deduction for restricted class abstraction. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓)) → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜓})
Theorem	csbeq12 36325	Equality deduction for substitution in class. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 𝐶 = 𝐷) → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐷)
Theorem	sbeqi 36326	Equality deduction for substitution. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ ((𝑥 = 𝑦 ∧ ∀𝑧(𝜑 ↔ 𝜓)) → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜓))
Theorem	ralbi12f 36327	Equality deduction for restricted universal quantification. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓)) → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓))
Theorem	oprabbi 36328	Equality deduction for class abstraction of nested ordered pairs. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ (∀𝑥∀𝑦∀𝑧(𝜑 ↔ 𝜓) → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓})
Theorem	mpobi123f 36329*	Equality deduction for maps-to notations with two arguments. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑦𝐶    &   ⊢ Ⅎ𝑦𝐷    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ Ⅎ𝑥𝐷    ⇒   ⊢ (((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝐸 = 𝐹) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐷 ↦ 𝐹))
Theorem	iuneq12f 36330	Equality deduction for indexed unions. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝐶 = 𝐷) → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷)
Theorem	iineq12f 36331	Equality deduction for indexed intersections. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝐶 = 𝐷) → ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐷)
Theorem	opabbi 36332	Equality deduction for class abstraction of ordered pairs. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ (∀𝑥∀𝑦(𝜑 ↔ 𝜓) → {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓})
Theorem	mptbi12f 36333	Equality deduction for maps-to notations. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝐷 = 𝐸) → (𝑥 ∈ 𝐴 ↦ 𝐷) = (𝑥 ∈ 𝐵 ↦ 𝐸))
20.21.4  Miscellanea Work in progress or things that do not belong anywhere else.
Theorem	orcomdd 36334	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 36335*	A version of scottex 9652 with nonfree variables instead of distinct variables. (Contributed by Giovanni Mascellani, 19-Aug-2018.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} ∈ V
Theorem	scott0f 36336*	A version of scott0 9653 with nonfree variables instead of distinct variables. (Contributed by Giovanni Mascellani, 19-Aug-2018.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 = ∅ ↔ {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} = ∅)
Theorem	scottn0f 36337*	A version of scott0f 36336 with inequalities instead of equalities. (Contributed by Giovanni Mascellani, 19-Aug-2018.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 ≠ ∅ ↔ {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} ≠ ∅)
Theorem	ac6s3f 36338*	Generalization of the Axiom of Choice to classes, with bound-variable hypothesis. (Contributed by Giovanni Mascellani, 19-Aug-2018.)
⊢ Ⅎ𝑦𝜓    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦𝜑 → ∃𝑓∀𝑥 ∈ 𝐴 𝜓)
Theorem	ac6s6 36339*	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 36340*	Generalization of the Axiom of Choice to classes, moving the existence condition in the consequent. (Contributed by Giovanni Mascellani, 20-Aug-2018.)
⊢ 𝐴 ∈ V    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓))    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ ∃𝑓∀𝑥 ∈ 𝐴 (∃𝑦𝜑 → 𝜓)
20.22  Mathbox for Peter Mazsa
20.22.1  Notations
Syntax	cxrn 36341	Extend the definition of a class to include the range Cartesian product class.
class (𝐴 ⋉ 𝐵)
Syntax	ccoss 36342	Extend the definition of a class to include the class of cosets by a class. (Read: the class of cosets by 𝑅.)
class ≀ 𝑅
Syntax	ccoels 36343	Extend the definition of a class to include the class of coelements on a class. (Read: the class of coelements on 𝐴.)
class ∼ 𝐴
Syntax	crels 36344	Extend the definition of a class to include the relation class.
class Rels
Syntax	cssr 36345	Extend the definition of a class to include the subset class.
class S
Syntax	crefs 36346	Extend the definition of a class to include the reflexivity class.
class Refs
Syntax	crefrels 36347	Extend the definition of a class to include the reflexive relations class.
class RefRels
Syntax	wrefrel 36348	Extend the definition of a wff to include the reflexive relation predicate. (Read: 𝑅 is a reflexive relation.)
wff RefRel 𝑅
Syntax	ccnvrefs 36349	Extend the definition of a class to include the converse reflexivity class.
class CnvRefs
Syntax	ccnvrefrels 36350	Extend the definition of a class to include the converse reflexive relations class.
class CnvRefRels
Syntax	wcnvrefrel 36351	Extend the definition of a wff to include the converse reflexive relation predicate. (Read: 𝑅 is a converse reflexive relation.)
wff CnvRefRel 𝑅
Syntax	csyms 36352	Extend the definition of a class to include the symmetry class.
class Syms
Syntax	csymrels 36353	Extend the definition of a class to include the symmetry relations class.
class SymRels
Syntax	wsymrel 36354	Extend the definition of a wff to include the symmetry relation predicate. (Read: 𝑅 is a symmetric relation.)
wff SymRel 𝑅
Syntax	ctrs 36355	Extend the definition of a class to include the transitivity class (but cf. the transitive class defined in df-tr 5193).
class Trs
Syntax	ctrrels 36356	Extend the definition of a class to include the transitive relations class.
class TrRels
Syntax	wtrrel 36357	Extend the definition of a wff to include the transitive relation predicate. (Read: 𝑅 is a transitive relation.)
wff TrRel 𝑅
Syntax	ceqvrels 36358	Extend the definition of a class to include the equivalence relations class.
class EqvRels
Syntax	weqvrel 36359	Extend the definition of a wff to include the equivalence relation predicate. (Read: 𝑅 is an equivalence relation.)
wff EqvRel 𝑅
Syntax	ccoeleqvrels 36360	Extend the definition of a class to include the coelement equivalence relations class.
class CoElEqvRels
Syntax	wcoeleqvrel 36361	Extend the definition of a wff to include the coelement equivalence relation predicate. (Read: the coelement equivalence relation on 𝐴.)
wff CoElEqvRel 𝐴
Syntax	credunds 36362	Extend the definition of a class to include the redundancy class.
class Redunds
Syntax	wredund 36363	Extend the definition of a wff to include the redundancy predicate. (Read: 𝐴 is redundant with respect to 𝐵 in 𝐶.)
wff 𝐴 Redund ⟨𝐵, 𝐶⟩
Syntax	wredundp 36364	Extend wff definition to include the redundancy operator for propositions.
wff redund (𝜑, 𝜓, 𝜒)
Syntax	cdmqss 36365	Extend the definition of a class to include the domain quotients class.
class DomainQss
Syntax	wdmqs 36366	Extend the definition of a wff to include the domain quotient predicate. (Read: the domain quotient of 𝑅 is 𝐴.)
wff 𝑅 DomainQs 𝐴
Syntax	cers 36367	Extend the definition of a class to include the equivalence relations on their domain quotients class.
class Ers
Syntax	werALTV 36368	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	cmembers 36369	Extend the definition of a class to include the membership equivalence relations class.
class MembErs
Syntax	wmember 36370	Extend the definition of a wff to include the membership equivalence relation predicate. (Read: the membership equivalence relation on 𝐴, or, the restricted elementhood equivalence relation on its domain quotient 𝐴.)
wff MembEr 𝐴
Syntax	cfunss 36371	Extend the definition of a class to include the function set class.
class Funss
Syntax	cfunsALTV 36372	Extend the definition of a class to include the functions class, i.e., the function relations class.
class FunsALTV
Syntax	wfunALTV 36373	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 36374	Extend the definition of a class to include the disjoint set class.
class Disjss
Syntax	cdisjs 36375	Extend the definition of a class to include the disjoints class, i.e., the disjoint relations class.
class Disjs
Syntax	wdisjALTV 36376	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 36377	Extend the definition of a class to include the disjoint elements class, i.e., the disjoint elementhood relations class.
class ElDisjs
Syntax	weldisj 36378	Extend the definition of a wff to include the disjoint elementhood predicate, i.e., the disjoint elementhood relation predicate. (Read: the elements of 𝐴 are disjoint.)
wff ElDisj 𝐴
20.22.2  Preparatory theorems
Theorem	el2v1 36379	New way (elv 3439, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 23-Oct-2018.)
⊢ ((𝑥 ∈ V ∧ 𝜑) → 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	el3v 36380	New way (elv 3439, 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 36381	New way (elv 3439, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 16-Oct-2020.)
⊢ ((𝑥 ∈ V ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
Theorem	el3v2 36382	New way (elv 3439, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 16-Oct-2020.)
⊢ ((𝜑 ∧ 𝑦 ∈ V ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
Theorem	el3v3 36383	New way (elv 3439, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 16-Oct-2020.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝑧 ∈ V) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
Theorem	el3v12 36384	New way (elv 3439, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 11-Jul-2021.)
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜒 → 𝜃)
Theorem	el3v13 36385	New way (elv 3439, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 11-Jul-2021.)
⊢ ((𝑥 ∈ V ∧ 𝜓 ∧ 𝑧 ∈ V) → 𝜃)    ⇒   ⊢ (𝜓 → 𝜃)
Theorem	el3v23 36386	New way (elv 3439, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 11-Jul-2021.)
⊢ ((𝜑 ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	an2anr 36387	Double commutation in conjunction. (Contributed by Peter Mazsa, 27-Jun-2019.)
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜓 ∧ 𝜑) ∧ (𝜃 ∧ 𝜒)))
Theorem	anan 36388	Multiple commutations in conjunction. (Contributed by Peter Mazsa, 7-Mar-2020.)
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ ((𝜑 ∧ 𝜃) ∧ 𝜏)) ↔ ((𝜓 ∧ 𝜃) ∧ (𝜑 ∧ (𝜒 ∧ 𝜏))))
Theorem	triantru3 36389	A wff is equivalent to its conjunctions with truths. (Contributed by Peter Mazsa, 30-Nov-2018.)
⊢ 𝜑    &   ⊢ 𝜓    ⇒   ⊢ (𝜒 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒))
Theorem	eqeltr 36390	Substitution of equal classes into elementhood relation. (Contributed by Peter Mazsa, 22-Jul-2017.)
⊢ ((𝐴 = 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)
Theorem	eqelb 36391	Substitution of equal classes into elementhood relation. (Contributed by Peter Mazsa, 17-Jul-2019.)
⊢ ((𝐴 = 𝐵 ∧ 𝐴 ∈ 𝐶) ↔ (𝐴 = 𝐵 ∧ 𝐵 ∈ 𝐶))
Theorem	eqeqan2d 36392	Implication of introducing a new equality. (Contributed by Peter Mazsa, 17-Apr-2019.)
⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ ((𝐴 = 𝐵 ∧ 𝜑) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))
Theorem	inres2 36393	Two ways of expressing the restriction of an intersection. (Contributed by Peter Mazsa, 5-Jun-2021.)
⊢ ((𝑅 ↾ 𝐴) ∩ 𝑆) = ((𝑅 ∩ 𝑆) ↾ 𝐴)
Theorem	coideq 36394	Equality theorem for composition of two classes. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐴) = (𝐵 ∘ 𝐵))
Theorem	nexmo1 36395	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	3ralbii 36396	Inference adding three restricted universal quantifiers to both sides of an equivalence. (Contributed by Peter Mazsa, 25-Jul-2019.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓)
Theorem	ssrabi 36397	Inference of restricted abstraction subclass from implication. (Contributed by Peter Mazsa, 26-Oct-2022.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓}
Theorem	rabbieq 36398	Equivalent wff's correspond to restricted class abstractions which are equal with the same class. (Contributed by Peter Mazsa, 8-Jul-2019.)
⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜑}    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜓}
Theorem	rabimbieq 36399	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 36400*	Intersection with class abstraction. (Contributed by Peter Mazsa, 21-Jul-2021.)
⊢ 𝐴 = (𝐵 ∩ 𝐶)    &   ⊢ 𝐵 = {𝑥 ∣ 𝜑}    ⇒   ⊢ 𝐴 = {𝑥 ∈ 𝐶 ∣ 𝜑}