P. 382 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 38101-38200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	selconj 38101	An inference for selecting one of a list of conjuncts. (Contributed by Giovanni Mascellani, 23-May-2019.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))    ⇒   ⊢ ((𝜂 ∧ 𝜑) ↔ (𝜓 ∧ (𝜂 ∧ 𝜒)))
Theorem	truconj 38102	Add true as a conjunct. (Contributed by Giovanni Mascellani, 23-May-2019.)
⊢ (𝜑 ↔ (⊤ ∧ 𝜑))
Theorem	orel 38103	An inference for disjunction elimination. (Contributed by Giovanni Mascellani, 24-May-2019.)
⊢ ((𝜓 ∧ 𝜂) → 𝜃)    &   ⊢ ((𝜒 ∧ 𝜌) → 𝜃)    &   ⊢ (𝜑 → (𝜓 ∨ 𝜒))    ⇒   ⊢ ((𝜑 ∧ (𝜂 ∧ 𝜌)) → 𝜃)
Theorem	negel 38104	An inference for negation elimination. (Contributed by Giovanni Mascellani, 24-May-2019.)
⊢ (𝜓 → 𝜒)    &   ⊢ (𝜑 → ¬ 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ⊥)
Theorem	botel 38105	An inference for bottom elimination. (Contributed by Giovanni Mascellani, 24-May-2019.)
⊢ (𝜑 → ⊥)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	tradd 38106	Add top ad a conjunct. (Contributed by Giovanni Mascellani, 24-May-2019.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (𝜑 ↔ (⊤ ∧ 𝜓))
Theorem	gm-sbtru 38107	Substitution does not change truth. (Contributed by Giovanni Mascellani, 24-May-2019.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ([𝐴 / 𝑥]⊤ ↔ ⊤)
Theorem	sbfal 38108	Substitution does not change falsity. (Contributed by Giovanni Mascellani, 24-May-2019.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ([𝐴 / 𝑥]⊥ ↔ ⊥)
Theorem	sbcani 38109	Distribution of class substitution over conjunction, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.)
⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜒)    &   ⊢ ([𝐴 / 𝑥]𝜓 ↔ 𝜂)    ⇒   ⊢ ([𝐴 / 𝑥](𝜑 ∧ 𝜓) ↔ (𝜒 ∧ 𝜂))
Theorem	sbcori 38110	Distribution of class substitution over disjunction, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.)
⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜒)    &   ⊢ ([𝐴 / 𝑥]𝜓 ↔ 𝜂)    ⇒   ⊢ ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ↔ (𝜒 ∨ 𝜂))
Theorem	sbcimi 38111	Distribution of class substitution over implication, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.)
⊢ 𝐴 ∈ V    &   ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜒)    &   ⊢ ([𝐴 / 𝑥]𝜓 ↔ 𝜂)    ⇒   ⊢ ([𝐴 / 𝑥](𝜑 → 𝜓) ↔ (𝜒 → 𝜂))
Theorem	sbcni 38112	Move class substitution inside a negation, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.)
⊢ 𝐴 ∈ V    &   ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜓)    ⇒   ⊢ ([𝐴 / 𝑥] ¬ 𝜑 ↔ ¬ 𝜓)
Theorem	sbali 38113	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 38114	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 38115*	Move universal quantifier in and out of class substitution, with an explicit nonfree variable condition. (Contributed by Giovanni Mascellani, 29-May-2019.)
⊢ Ⅎ𝑦𝐴    ⇒   ⊢ ([𝐴 / 𝑥]∀𝑦𝜑 ↔ ∀𝑦[𝐴 / 𝑥]𝜑)
Theorem	sbcexf 38116*	Move existential quantifier in and out of class substitution, with an explicit nonfree variable condition. (Contributed by Giovanni Mascellani, 29-May-2019.)
⊢ Ⅎ𝑦𝐴    ⇒   ⊢ ([𝐴 / 𝑥]∃𝑦𝜑 ↔ ∃𝑦[𝐴 / 𝑥]𝜑)
Theorem	sbcalfi 38117*	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 38118*	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 38119	A lemma for eliminating a universal quantifier, in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.)
⊢ 𝐴 ∈ V    &   ⊢ (𝜑 → ∀𝑥𝜒)    &   ⊢ ([𝐴 / 𝑥]𝜒 ↔ 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	alrimii 38120*	A lemma for introducing a universal quantifier, in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → 𝜓)    &   ⊢ ([𝑦 / 𝑥]𝜒 ↔ 𝜓)    &   ⊢ Ⅎ𝑦𝜒    ⇒   ⊢ (𝜑 → ∀𝑥𝜒)
Theorem	spesbcdi 38121	A lemma for introducing an existential quantifier, in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.)
⊢ (𝜑 → 𝜓)    &   ⊢ ([𝐴 / 𝑥]𝜒 ↔ 𝜓)    ⇒   ⊢ (𝜑 → ∃𝑥𝜒)
Theorem	exlimddvf 38122	A lemma for eliminating an existential quantifier. (Contributed by Giovanni Mascellani, 30-May-2019.)
⊢ (𝜑 → ∃𝑥𝜃)    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ ((𝜃 ∧ 𝜓) → 𝜒)    &   ⊢ Ⅎ𝑥𝜒    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	exlimddvfi 38123	A lemma for eliminating an existential quantifier, in inference form. (Contributed by Giovanni Mascellani, 31-May-2019.)
⊢ (𝜑 → ∃𝑥𝜃)    &   ⊢ Ⅎ𝑦𝜃    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ ([𝑦 / 𝑥]𝜃 ↔ 𝜂)    &   ⊢ ((𝜂 ∧ 𝜓) → 𝜒)    &   ⊢ Ⅎ𝑦𝜒    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	sbceq1ddi 38124	A lemma for eliminating inequality, in inference form. (Contributed by Giovanni Mascellani, 31-May-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜓 → 𝜃)    &   ⊢ ([𝐴 / 𝑥]𝜒 ↔ 𝜃)    &   ⊢ ([𝐵 / 𝑥]𝜒 ↔ 𝜂)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜂)
Theorem	sbccom2lem 38125*	Lemma for sbccom2 38126. (Contributed by Giovanni Mascellani, 31-May-2019.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦][𝐴 / 𝑥]𝜑)
Theorem	sbccom2 38126*	Commutative law for double class substitution. (Contributed by Giovanni Mascellani, 31-May-2019.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦][𝐴 / 𝑥]𝜑)
Theorem	sbccom2f 38127*	Commutative law for double class substitution, with nonfree variable condition. (Contributed by Giovanni Mascellani, 31-May-2019.)
⊢ 𝐴 ∈ V    &   ⊢ Ⅎ𝑦𝐴    ⇒   ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦][𝐴 / 𝑥]𝜑)
Theorem	sbccom2fi 38128*	Commutative law for double class substitution, with nonfree variable condition and in inference form. (Contributed by Giovanni Mascellani, 1-Jun-2019.)
⊢ 𝐴 ∈ V    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶    &   ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜓)    ⇒   ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [𝐶 / 𝑦]𝜓)
Theorem	csbcom2fi 38129*	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.25.2  Tseitin axioms A collection of Tseitin axioms used to convert a wff to Conjunctive Normal Form.
Theorem	fald 38130	Refutation of falsity, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ¬ ⊥)
Theorem	tsim1 38131	A Tseitin axiom for logical implication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((¬ 𝜑 ∨ 𝜓) ∨ ¬ (𝜑 → 𝜓)))
Theorem	tsim2 38132	A Tseitin axiom for logical implication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → (𝜑 ∨ (𝜑 → 𝜓)))
Theorem	tsim3 38133	A Tseitin axiom for logical implication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → (¬ 𝜓 ∨ (𝜑 → 𝜓)))
Theorem	tsbi1 38134	A Tseitin axiom for logical biconditional, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((¬ 𝜑 ∨ ¬ 𝜓) ∨ (𝜑 ↔ 𝜓)))
Theorem	tsbi2 38135	A Tseitin axiom for logical biconditional, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((𝜑 ∨ 𝜓) ∨ (𝜑 ↔ 𝜓)))
Theorem	tsbi3 38136	A Tseitin axiom for logical biconditional, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((𝜑 ∨ ¬ 𝜓) ∨ ¬ (𝜑 ↔ 𝜓)))
Theorem	tsbi4 38137	A Tseitin axiom for logical biconditional, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((¬ 𝜑 ∨ 𝜓) ∨ ¬ (𝜑 ↔ 𝜓)))
Theorem	tsxo1 38138	A Tseitin axiom for logical exclusive disjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((¬ 𝜑 ∨ ¬ 𝜓) ∨ ¬ (𝜑 ⊻ 𝜓)))
Theorem	tsxo2 38139	A Tseitin axiom for logical exclusive disjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((𝜑 ∨ 𝜓) ∨ ¬ (𝜑 ⊻ 𝜓)))
Theorem	tsxo3 38140	A Tseitin axiom for logical exclusive disjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((𝜑 ∨ ¬ 𝜓) ∨ (𝜑 ⊻ 𝜓)))
Theorem	tsxo4 38141	A Tseitin axiom for logical exclusive disjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((¬ 𝜑 ∨ 𝜓) ∨ (𝜑 ⊻ 𝜓)))
Theorem	tsan1 38142	A Tseitin axiom for logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((¬ 𝜑 ∨ ¬ 𝜓) ∨ (𝜑 ∧ 𝜓)))
Theorem	tsan2 38143	A Tseitin axiom for logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → (𝜑 ∨ ¬ (𝜑 ∧ 𝜓)))
Theorem	tsan3 38144	A Tseitin axiom for logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → (𝜓 ∨ ¬ (𝜑 ∧ 𝜓)))
Theorem	tsna1 38145	A Tseitin axiom for logical incompatibility, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((¬ 𝜑 ∨ ¬ 𝜓) ∨ ¬ (𝜑 ⊼ 𝜓)))
Theorem	tsna2 38146	A Tseitin axiom for logical incompatibility, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → (𝜑 ∨ (𝜑 ⊼ 𝜓)))
Theorem	tsna3 38147	A Tseitin axiom for logical incompatibility, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → (𝜓 ∨ (𝜑 ⊼ 𝜓)))
Theorem	tsor1 38148	A Tseitin axiom for logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → ((𝜑 ∨ 𝜓) ∨ ¬ (𝜑 ∨ 𝜓)))
Theorem	tsor2 38149	A Tseitin axiom for logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → (¬ 𝜑 ∨ (𝜑 ∨ 𝜓)))
Theorem	tsor3 38150	A Tseitin axiom for logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → (¬ 𝜓 ∨ (𝜑 ∨ 𝜓)))
Theorem	ts3an1 38151	A Tseitin axiom for triple logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → ((¬ (𝜑 ∧ 𝜓) ∨ ¬ 𝜒) ∨ (𝜑 ∧ 𝜓 ∧ 𝜒)))
Theorem	ts3an2 38152	A Tseitin axiom for triple logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → ((𝜑 ∧ 𝜓) ∨ ¬ (𝜑 ∧ 𝜓 ∧ 𝜒)))
Theorem	ts3an3 38153	A Tseitin axiom for triple logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → (𝜒 ∨ ¬ (𝜑 ∧ 𝜓 ∧ 𝜒)))
Theorem	ts3or1 38154	A Tseitin axiom for triple logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → (((𝜑 ∨ 𝜓) ∨ 𝜒) ∨ ¬ (𝜑 ∨ 𝜓 ∨ 𝜒)))
Theorem	ts3or2 38155	A Tseitin axiom for triple logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → (¬ (𝜑 ∨ 𝜓) ∨ (𝜑 ∨ 𝜓 ∨ 𝜒)))
Theorem	ts3or3 38156	A Tseitin axiom for triple logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
⊢ (𝜃 → (¬ 𝜒 ∨ (𝜑 ∨ 𝜓 ∨ 𝜒)))
21.25.3  Equality deductions A collection of theorems for commuting equalities (or biconditionals) with other constructs.
Theorem	iuneq2f 38157	Equality deduction for indexed union. (Contributed by Giovanni Mascellani, 9-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶)
Theorem	rabeq12f 38158	Equality deduction for restricted class abstraction. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓)) → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜓})
Theorem	csbeq12 38159	Equality deduction for substitution in class. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 𝐶 = 𝐷) → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐷)
Theorem	sbeqi 38160	Equality deduction for substitution. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ ((𝑥 = 𝑦 ∧ ∀𝑧(𝜑 ↔ 𝜓)) → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜓))
Theorem	ralbi12f 38161	Equality deduction for restricted universal quantification. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓)) → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓))
Theorem	oprabbi 38162	Equality deduction for class abstraction of nested ordered pairs. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ (∀𝑥∀𝑦∀𝑧(𝜑 ↔ 𝜓) → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓})
Theorem	mpobi123f 38163*	Equality deduction for maps-to notations with two arguments. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑦𝐶    &   ⊢ Ⅎ𝑦𝐷    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ Ⅎ𝑥𝐷    ⇒   ⊢ (((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝐸 = 𝐹) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐷 ↦ 𝐹))
Theorem	iuneq12f 38164	Equality deduction for indexed unions. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝐶 = 𝐷) → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷)
Theorem	iineq12f 38165	Equality deduction for indexed intersections. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝐶 = 𝐷) → ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐷)
Theorem	opabbi 38166	Equality deduction for class abstraction of ordered pairs. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ (∀𝑥∀𝑦(𝜑 ↔ 𝜓) → {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓})
Theorem	mptbi12f 38167	Equality deduction for maps-to notations. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝐷 = 𝐸) → (𝑥 ∈ 𝐴 ↦ 𝐷) = (𝑥 ∈ 𝐵 ↦ 𝐸))
21.25.4  Miscellanea Work in progress or things that do not belong anywhere else.
Theorem	orcomdd 38168	Commutativity of logic disjunction, in double deduction form. Should not be moved to main, see PR #3034 in Github. Use orcomd 871 instead. (Contributed by Giovanni Mascellani, 19-Mar-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝜑 → (𝜓 → (𝜒 ∨ 𝜃)))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜃 ∨ 𝜒)))
Theorem	scottexf 38169*	A version of scottex 9845 with nonfree variables instead of distinct variables. (Contributed by Giovanni Mascellani, 19-Aug-2018.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} ∈ V
Theorem	scott0f 38170*	A version of scott0 9846 with nonfree variables instead of distinct variables. (Contributed by Giovanni Mascellani, 19-Aug-2018.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 = ∅ ↔ {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} = ∅)
Theorem	scottn0f 38171*	A version of scott0f 38170 with inequalities instead of equalities. (Contributed by Giovanni Mascellani, 19-Aug-2018.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 ≠ ∅ ↔ {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} ≠ ∅)
Theorem	ac6s3f 38172*	Generalization of the Axiom of Choice to classes, with bound-variable hypothesis. (Contributed by Giovanni Mascellani, 19-Aug-2018.)
⊢ Ⅎ𝑦𝜓    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦𝜑 → ∃𝑓∀𝑥 ∈ 𝐴 𝜓)
Theorem	ac6s6 38173*	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 38174*	Generalization of the Axiom of Choice to classes, moving the existence condition in the consequent. (Contributed by Giovanni Mascellani, 20-Aug-2018.)
⊢ 𝐴 ∈ V    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓))    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ ∃𝑓∀𝑥 ∈ 𝐴 (∃𝑦𝜑 → 𝜓)
21.26  Mathbox for Peter Mazsa
21.26.1  Notations
Syntax	cxrn 38175	Extend the definition of a class to include the range Cartesian product class.
class (𝐴 ⋉ 𝐵)
Syntax	ccoss 38176	Extend the definition of a class to include the class of cosets by a class. (Read: the class of cosets by 𝑅.)
class ≀ 𝑅
Syntax	ccoels 38177	Extend the definition of a class to include the class of coelements on a class. (Read: the class of coelements on 𝐴.)
class ∼ 𝐴
Syntax	crels 38178	Extend the definition of a class to include the relation class.
class Rels
Syntax	cssr 38179	Extend the definition of a class to include the subset class.
class S
Syntax	crefs 38180	Extend the definition of a class to include the reflexivity class.
class Refs
Syntax	crefrels 38181	Extend the definition of a class to include the reflexive relations class.
class RefRels
Syntax	wrefrel 38182	Extend the definition of a wff to include the reflexive relation predicate. (Read: 𝑅 is a reflexive relation.)
wff RefRel 𝑅
Syntax	ccnvrefs 38183	Extend the definition of a class to include the converse reflexivity class.
class CnvRefs
Syntax	ccnvrefrels 38184	Extend the definition of a class to include the converse reflexive relations class.
class CnvRefRels
Syntax	wcnvrefrel 38185	Extend the definition of a wff to include the converse reflexive relation predicate. (Read: 𝑅 is a converse reflexive relation.)
wff CnvRefRel 𝑅
Syntax	csyms 38186	Extend the definition of a class to include the symmetry class.
class Syms
Syntax	csymrels 38187	Extend the definition of a class to include the symmetry relations class.
class SymRels
Syntax	wsymrel 38188	Extend the definition of a wff to include the symmetry relation predicate. (Read: 𝑅 is a symmetric relation.)
wff SymRel 𝑅
Syntax	ctrs 38189	Extend the definition of a class to include the transitivity class (but cf. the transitive class defined in df-tr 5218).
class Trs
Syntax	ctrrels 38190	Extend the definition of a class to include the transitive relations class.
class TrRels
Syntax	wtrrel 38191	Extend the definition of a wff to include the transitive relation predicate. (Read: 𝑅 is a transitive relation.)
wff TrRel 𝑅
Syntax	ceqvrels 38192	Extend the definition of a class to include the equivalence relations class.
class EqvRels
Syntax	weqvrel 38193	Extend the definition of a wff to include the equivalence relation predicate. (Read: 𝑅 is an equivalence relation.)
wff EqvRel 𝑅
Syntax	ccoeleqvrels 38194	Extend the definition of a class to include the coelement equivalence relations class.
class CoElEqvRels
Syntax	wcoeleqvrel 38195	Extend the definition of a wff to include the coelement equivalence relation predicate. (Read: the coelement equivalence relation on 𝐴.)
wff CoElEqvRel 𝐴
Syntax	credunds 38196	Extend the definition of a class to include the redundancy class.
class Redunds
Syntax	wredund 38197	Extend the definition of a wff to include the redundancy predicate. (Read: 𝐴 is redundant with respect to 𝐵 in 𝐶.)
wff 𝐴 Redund ⟨𝐵, 𝐶⟩
Syntax	wredundp 38198	Extend wff definition to include the redundancy operator for propositions.
wff redund (𝜑, 𝜓, 𝜒)
Syntax	cdmqss 38199	Extend the definition of a class to include the domain quotients class.
class DomainQss
Syntax	wdmqs 38200	Extend the definition of a wff to include the domain quotient predicate. (Read: the domain quotient of 𝑅 is 𝐴.)
wff 𝑅 DomainQs 𝐴