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