P. 378 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37701-37800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	contrd 37701	A proof by contradiction, in deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.)
⊢ (𝜑 → (¬ 𝜓 → 𝜒))    &   ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	an12i 37702	An inference from commuting operands in a chain of conjunctions. (Contributed by Giovanni Mascellani, 22-May-2019.)
⊢ (𝜑 ∧ (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜓 ∧ (𝜑 ∧ 𝜒))
Theorem	exmid2 37703	An excluded middle law. (Contributed by Giovanni Mascellani, 23-May-2019.)
⊢ ((𝜓 ∧ 𝜑) → 𝜒)    &   ⊢ ((¬ 𝜓 ∧ 𝜂) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜂) → 𝜒)
Theorem	selconj 37704	An inference for selecting one of a list of conjuncts. (Contributed by Giovanni Mascellani, 23-May-2019.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))    ⇒   ⊢ ((𝜂 ∧ 𝜑) ↔ (𝜓 ∧ (𝜂 ∧ 𝜒)))
Theorem	truconj 37705	Add true as a conjunct. (Contributed by Giovanni Mascellani, 23-May-2019.)
⊢ (𝜑 ↔ (⊤ ∧ 𝜑))
Theorem	orel 37706	An inference for disjunction elimination. (Contributed by Giovanni Mascellani, 24-May-2019.)
⊢ ((𝜓 ∧ 𝜂) → 𝜃)    &   ⊢ ((𝜒 ∧ 𝜌) → 𝜃)    &   ⊢ (𝜑 → (𝜓 ∨ 𝜒))    ⇒   ⊢ ((𝜑 ∧ (𝜂 ∧ 𝜌)) → 𝜃)
Theorem	negel 37707	An inference for negation elimination. (Contributed by Giovanni Mascellani, 24-May-2019.)
⊢ (𝜓 → 𝜒)    &   ⊢ (𝜑 → ¬ 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ⊥)
Theorem	botel 37708	An inference for bottom elimination. (Contributed by Giovanni Mascellani, 24-May-2019.)
⊢ (𝜑 → ⊥)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	tradd 37709	Add top ad a conjunct. (Contributed by Giovanni Mascellani, 24-May-2019.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (𝜑 ↔ (⊤ ∧ 𝜓))
Theorem	gm-sbtru 37710	Substitution does not change truth. (Contributed by Giovanni Mascellani, 24-May-2019.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ([𝐴 / 𝑥]⊤ ↔ ⊤)
Theorem	sbfal 37711	Substitution does not change falsity. (Contributed by Giovanni Mascellani, 24-May-2019.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ([𝐴 / 𝑥]⊥ ↔ ⊥)
Theorem	sbcani 37712	Distribution of class substitution over conjunction, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.)
⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜒)    &   ⊢ ([𝐴 / 𝑥]𝜓 ↔ 𝜂)    ⇒   ⊢ ([𝐴 / 𝑥](𝜑 ∧ 𝜓) ↔ (𝜒 ∧ 𝜂))
Theorem	sbcori 37713	Distribution of class substitution over disjunction, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.)
⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜒)    &   ⊢ ([𝐴 / 𝑥]𝜓 ↔ 𝜂)    ⇒   ⊢ ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ↔ (𝜒 ∨ 𝜂))
Theorem	sbcimi 37714	Distribution of class substitution over implication, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.)
⊢ 𝐴 ∈ V    &   ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜒)    &   ⊢ ([𝐴 / 𝑥]𝜓 ↔ 𝜂)    ⇒   ⊢ ([𝐴 / 𝑥](𝜑 → 𝜓) ↔ (𝜒 → 𝜂))
Theorem	sbcni 37715	Move class substitution inside a negation, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.)
⊢ 𝐴 ∈ V    &   ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜓)    ⇒   ⊢ ([𝐴 / 𝑥] ¬ 𝜑 ↔ ¬ 𝜓)
Theorem	sbali 37716	Discard class substitution in a universal quantification when substituting the quantified variable, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ([𝐴 / 𝑥]∀𝑥𝜑 ↔ ∀𝑥𝜑)
Theorem	sbexi 37717	Discard class substitution in an existential quantification when substituting the quantified variable, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ([𝐴 / 𝑥]∃𝑥𝜑 ↔ ∃𝑥𝜑)
Theorem	sbcalf 37718*	Move universal quantifier in and out of class substitution, with an explicit nonfree variable condition. (Contributed by Giovanni Mascellani, 29-May-2019.)
⊢ Ⅎ𝑦𝐴    ⇒   ⊢ ([𝐴 / 𝑥]∀𝑦𝜑 ↔ ∀𝑦[𝐴 / 𝑥]𝜑)
Theorem	sbcexf 37719*	Move existential quantifier in and out of class substitution, with an explicit nonfree variable condition. (Contributed by Giovanni Mascellani, 29-May-2019.)
⊢ Ⅎ𝑦𝐴    ⇒   ⊢ ([𝐴 / 𝑥]∃𝑦𝜑 ↔ ∃𝑦[𝐴 / 𝑥]𝜑)
Theorem	sbcalfi 37720*	Move universal quantifier in and out of class substitution, with an explicit nonfree variable condition and in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.)
⊢ Ⅎ𝑦𝐴    &   ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜓)    ⇒   ⊢ ([𝐴 / 𝑥]∀𝑦𝜑 ↔ ∀𝑦𝜓)
Theorem	sbcexfi 37721*	Move existential quantifier in and out of class substitution, with an explicit nonfree variable condition and in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.)
⊢ Ⅎ𝑦𝐴    &   ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜓)    ⇒   ⊢ ([𝐴 / 𝑥]∃𝑦𝜑 ↔ ∃𝑦𝜓)
Theorem	spsbcdi 37722	A lemma for eliminating a universal quantifier, in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.)
⊢ 𝐴 ∈ V    &   ⊢ (𝜑 → ∀𝑥𝜒)    &   ⊢ ([𝐴 / 𝑥]𝜒 ↔ 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	alrimii 37723*	A lemma for introducing a universal quantifier, in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → 𝜓)    &   ⊢ ([𝑦 / 𝑥]𝜒 ↔ 𝜓)    &   ⊢ Ⅎ𝑦𝜒    ⇒   ⊢ (𝜑 → ∀𝑥𝜒)
Theorem	spesbcdi 37724	A lemma for introducing an existential quantifier, in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.)
⊢ (𝜑 → 𝜓)    &   ⊢ ([𝐴 / 𝑥]𝜒 ↔ 𝜓)    ⇒   ⊢ (𝜑 → ∃𝑥𝜒)
Theorem	exlimddvf 37725	A lemma for eliminating an existential quantifier. (Contributed by Giovanni Mascellani, 30-May-2019.)
⊢ (𝜑 → ∃𝑥𝜃)    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ ((𝜃 ∧ 𝜓) → 𝜒)    &   ⊢ Ⅎ𝑥𝜒    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	exlimddvfi 37726	A lemma for eliminating an existential quantifier, in inference form. (Contributed by Giovanni Mascellani, 31-May-2019.)
⊢ (𝜑 → ∃𝑥𝜃)    &   ⊢ Ⅎ𝑦𝜃    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ ([𝑦 / 𝑥]𝜃 ↔ 𝜂)    &   ⊢ ((𝜂 ∧ 𝜓) → 𝜒)    &   ⊢ Ⅎ𝑦𝜒    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	sbceq1ddi 37727	A lemma for eliminating inequality, in inference form. (Contributed by Giovanni Mascellani, 31-May-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜓 → 𝜃)    &   ⊢ ([𝐴 / 𝑥]𝜒 ↔ 𝜃)    &   ⊢ ([𝐵 / 𝑥]𝜒 ↔ 𝜂)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜂)
Theorem	sbccom2lem 37728*	Lemma for sbccom2 37729. (Contributed by Giovanni Mascellani, 31-May-2019.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦][𝐴 / 𝑥]𝜑)
Theorem	sbccom2 37729*	Commutative law for double class substitution. (Contributed by Giovanni Mascellani, 31-May-2019.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦][𝐴 / 𝑥]𝜑)
Theorem	sbccom2f 37730*	Commutative law for double class substitution, with nonfree variable condition. (Contributed by Giovanni Mascellani, 31-May-2019.)
⊢ 𝐴 ∈ V    &   ⊢ Ⅎ𝑦𝐴    ⇒   ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦][𝐴 / 𝑥]𝜑)
Theorem	sbccom2fi 37731*	Commutative law for double class substitution, with nonfree variable condition and in inference form. (Contributed by Giovanni Mascellani, 1-Jun-2019.)
⊢ 𝐴 ∈ V    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶    &   ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜓)    ⇒   ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [𝐶 / 𝑦]𝜓)
Theorem	csbcom2fi 37732*	Commutative law for double class substitution in a class, with nonfree variable condition and in inference form. (Contributed by Giovanni Mascellani, 4-Jun-2019.)
⊢ 𝐴 ∈ V    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶    &   ⊢ ⦋𝐴 / 𝑥⦌𝐷 = 𝐸    ⇒   ⊢ ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐷 = ⦋𝐶 / 𝑦⦌𝐸
21.23.2  Tseitin axioms A collection of Tseitin axioms used to convert a wff to Conjunctive Normal Form.
Theorem	fald 37733	Refutation of falsity, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ¬ ⊥)
Theorem	tsim1 37734	A Tseitin axiom for logical implication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((¬ 𝜑 ∨ 𝜓) ∨ ¬ (𝜑 → 𝜓)))
Theorem	tsim2 37735	A Tseitin axiom for logical implication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → (𝜑 ∨ (𝜑 → 𝜓)))
Theorem	tsim3 37736	A Tseitin axiom for logical implication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → (¬ 𝜓 ∨ (𝜑 → 𝜓)))
Theorem	tsbi1 37737	A Tseitin axiom for logical biconditional, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((¬ 𝜑 ∨ ¬ 𝜓) ∨ (𝜑 ↔ 𝜓)))
Theorem	tsbi2 37738	A Tseitin axiom for logical biconditional, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((𝜑 ∨ 𝜓) ∨ (𝜑 ↔ 𝜓)))
Theorem	tsbi3 37739	A Tseitin axiom for logical biconditional, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((𝜑 ∨ ¬ 𝜓) ∨ ¬ (𝜑 ↔ 𝜓)))
Theorem	tsbi4 37740	A Tseitin axiom for logical biconditional, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((¬ 𝜑 ∨ 𝜓) ∨ ¬ (𝜑 ↔ 𝜓)))
Theorem	tsxo1 37741	A Tseitin axiom for logical exclusive disjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((¬ 𝜑 ∨ ¬ 𝜓) ∨ ¬ (𝜑 ⊻ 𝜓)))
Theorem	tsxo2 37742	A Tseitin axiom for logical exclusive disjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((𝜑 ∨ 𝜓) ∨ ¬ (𝜑 ⊻ 𝜓)))
Theorem	tsxo3 37743	A Tseitin axiom for logical exclusive disjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((𝜑 ∨ ¬ 𝜓) ∨ (𝜑 ⊻ 𝜓)))
Theorem	tsxo4 37744	A Tseitin axiom for logical exclusive disjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((¬ 𝜑 ∨ 𝜓) ∨ (𝜑 ⊻ 𝜓)))
Theorem	tsan1 37745	A Tseitin axiom for logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((¬ 𝜑 ∨ ¬ 𝜓) ∨ (𝜑 ∧ 𝜓)))
Theorem	tsan2 37746	A Tseitin axiom for logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → (𝜑 ∨ ¬ (𝜑 ∧ 𝜓)))
Theorem	tsan3 37747	A Tseitin axiom for logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → (𝜓 ∨ ¬ (𝜑 ∧ 𝜓)))
Theorem	tsna1 37748	A Tseitin axiom for logical incompatibility, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((¬ 𝜑 ∨ ¬ 𝜓) ∨ ¬ (𝜑 ⊼ 𝜓)))
Theorem	tsna2 37749	A Tseitin axiom for logical incompatibility, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → (𝜑 ∨ (𝜑 ⊼ 𝜓)))
Theorem	tsna3 37750	A Tseitin axiom for logical incompatibility, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → (𝜓 ∨ (𝜑 ⊼ 𝜓)))
Theorem	tsor1 37751	A Tseitin axiom for logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → ((𝜑 ∨ 𝜓) ∨ ¬ (𝜑 ∨ 𝜓)))
Theorem	tsor2 37752	A Tseitin axiom for logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → (¬ 𝜑 ∨ (𝜑 ∨ 𝜓)))
Theorem	tsor3 37753	A Tseitin axiom for logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → (¬ 𝜓 ∨ (𝜑 ∨ 𝜓)))
Theorem	ts3an1 37754	A Tseitin axiom for triple logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → ((¬ (𝜑 ∧ 𝜓) ∨ ¬ 𝜒) ∨ (𝜑 ∧ 𝜓 ∧ 𝜒)))
Theorem	ts3an2 37755	A Tseitin axiom for triple logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → ((𝜑 ∧ 𝜓) ∨ ¬ (𝜑 ∧ 𝜓 ∧ 𝜒)))
Theorem	ts3an3 37756	A Tseitin axiom for triple logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → (𝜒 ∨ ¬ (𝜑 ∧ 𝜓 ∧ 𝜒)))
Theorem	ts3or1 37757	A Tseitin axiom for triple logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → (((𝜑 ∨ 𝜓) ∨ 𝜒) ∨ ¬ (𝜑 ∨ 𝜓 ∨ 𝜒)))
Theorem	ts3or2 37758	A Tseitin axiom for triple logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → (¬ (𝜑 ∨ 𝜓) ∨ (𝜑 ∨ 𝜓 ∨ 𝜒)))
Theorem	ts3or3 37759	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 37760	Equality deduction for indexed union. (Contributed by Giovanni Mascellani, 9-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶)
Theorem	rabeq12f 37761	Equality deduction for restricted class abstraction. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓)) → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜓})
Theorem	csbeq12 37762	Equality deduction for substitution in class. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 𝐶 = 𝐷) → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐷)
Theorem	sbeqi 37763	Equality deduction for substitution. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ ((𝑥 = 𝑦 ∧ ∀𝑧(𝜑 ↔ 𝜓)) → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜓))
Theorem	ralbi12f 37764	Equality deduction for restricted universal quantification. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓)) → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓))
Theorem	oprabbi 37765	Equality deduction for class abstraction of nested ordered pairs. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ (∀𝑥∀𝑦∀𝑧(𝜑 ↔ 𝜓) → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓})
Theorem	mpobi123f 37766*	Equality deduction for maps-to notations with two arguments. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑦𝐶    &   ⊢ Ⅎ𝑦𝐷    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ Ⅎ𝑥𝐷    ⇒   ⊢ (((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝐸 = 𝐹) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐷 ↦ 𝐹))
Theorem	iuneq12f 37767	Equality deduction for indexed unions. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝐶 = 𝐷) → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷)
Theorem	iineq12f 37768	Equality deduction for indexed intersections. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝐶 = 𝐷) → ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐷)
Theorem	opabbi 37769	Equality deduction for class abstraction of ordered pairs. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ (∀𝑥∀𝑦(𝜑 ↔ 𝜓) → {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓})
Theorem	mptbi12f 37770	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 37771	Commutativity of logic disjunction, in double deduction form. Should not be moved to main, see PR #3034 in Github. Use orcomd 869 instead. (Contributed by Giovanni Mascellani, 19-Mar-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝜑 → (𝜓 → (𝜒 ∨ 𝜃)))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜃 ∨ 𝜒)))
Theorem	scottexf 37772*	A version of scottex 9910 with nonfree variables instead of distinct variables. (Contributed by Giovanni Mascellani, 19-Aug-2018.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} ∈ V
Theorem	scott0f 37773*	A version of scott0 9911 with nonfree variables instead of distinct variables. (Contributed by Giovanni Mascellani, 19-Aug-2018.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 = ∅ ↔ {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} = ∅)
Theorem	scottn0f 37774*	A version of scott0f 37773 with inequalities instead of equalities. (Contributed by Giovanni Mascellani, 19-Aug-2018.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 ≠ ∅ ↔ {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} ≠ ∅)
Theorem	ac6s3f 37775*	Generalization of the Axiom of Choice to classes, with bound-variable hypothesis. (Contributed by Giovanni Mascellani, 19-Aug-2018.)
⊢ Ⅎ𝑦𝜓    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦𝜑 → ∃𝑓∀𝑥 ∈ 𝐴 𝜓)
Theorem	ac6s6 37776*	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 37777*	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 37778	Extend the definition of a class to include the range Cartesian product class.
class (𝐴 ⋉ 𝐵)
Syntax	ccoss 37779	Extend the definition of a class to include the class of cosets by a class. (Read: the class of cosets by 𝑅.)
class ≀ 𝑅
Syntax	ccoels 37780	Extend the definition of a class to include the class of coelements on a class. (Read: the class of coelements on 𝐴.)
class ∼ 𝐴
Syntax	crels 37781	Extend the definition of a class to include the relation class.
class Rels
Syntax	cssr 37782	Extend the definition of a class to include the subset class.
class S
Syntax	crefs 37783	Extend the definition of a class to include the reflexivity class.
class Refs
Syntax	crefrels 37784	Extend the definition of a class to include the reflexive relations class.
class RefRels
Syntax	wrefrel 37785	Extend the definition of a wff to include the reflexive relation predicate. (Read: 𝑅 is a reflexive relation.)
wff RefRel 𝑅
Syntax	ccnvrefs 37786	Extend the definition of a class to include the converse reflexivity class.
class CnvRefs
Syntax	ccnvrefrels 37787	Extend the definition of a class to include the converse reflexive relations class.
class CnvRefRels
Syntax	wcnvrefrel 37788	Extend the definition of a wff to include the converse reflexive relation predicate. (Read: 𝑅 is a converse reflexive relation.)
wff CnvRefRel 𝑅
Syntax	csyms 37789	Extend the definition of a class to include the symmetry class.
class Syms
Syntax	csymrels 37790	Extend the definition of a class to include the symmetry relations class.
class SymRels
Syntax	wsymrel 37791	Extend the definition of a wff to include the symmetry relation predicate. (Read: 𝑅 is a symmetric relation.)
wff SymRel 𝑅
Syntax	ctrs 37792	Extend the definition of a class to include the transitivity class (but cf. the transitive class defined in df-tr 5267).
class Trs
Syntax	ctrrels 37793	Extend the definition of a class to include the transitive relations class.
class TrRels
Syntax	wtrrel 37794	Extend the definition of a wff to include the transitive relation predicate. (Read: 𝑅 is a transitive relation.)
wff TrRel 𝑅
Syntax	ceqvrels 37795	Extend the definition of a class to include the equivalence relations class.
class EqvRels
Syntax	weqvrel 37796	Extend the definition of a wff to include the equivalence relation predicate. (Read: 𝑅 is an equivalence relation.)
wff EqvRel 𝑅
Syntax	ccoeleqvrels 37797	Extend the definition of a class to include the coelement equivalence relations class.
class CoElEqvRels
Syntax	wcoeleqvrel 37798	Extend the definition of a wff to include the coelement equivalence relation predicate. (Read: the coelement equivalence relation on 𝐴.)
wff CoElEqvRel 𝐴
Syntax	credunds 37799	Extend the definition of a class to include the redundancy class.
class Redunds
Syntax	wredund 37800	Extend the definition of a wff to include the redundancy predicate. (Read: 𝐴 is redundant with respect to 𝐵 in 𝐶.)
wff 𝐴 Redund ⟨𝐵, 𝐶⟩