Home | Metamath
Proof Explorer Theorem List (p. 340 of 426) | < 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: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | exmid2 33901 | An excluded middle law. (Contributed by Giovanni Mascellani, 23-May-2019.) |
⊢ ((𝜓 ∧ 𝜑) → 𝜒) & ⊢ ((¬ 𝜓 ∧ 𝜂) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜂) → 𝜒) | ||
Theorem | selconj 33902 | An inference for selecting one of a list of conjuncts. (Contributed by Giovanni Mascellani, 23-May-2019.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ ((𝜂 ∧ 𝜑) ↔ (𝜓 ∧ (𝜂 ∧ 𝜒))) | ||
Theorem | truconj 33903 | Add true as a conjunct. (Contributed by Giovanni Mascellani, 23-May-2019.) |
⊢ (𝜑 ↔ (⊤ ∧ 𝜑)) | ||
Theorem | orel 33904 | An inference for disjunction elimination. (Contributed by Giovanni Mascellani, 24-May-2019.) |
⊢ ((𝜓 ∧ 𝜂) → 𝜃) & ⊢ ((𝜒 ∧ 𝜌) → 𝜃) & ⊢ (𝜑 → (𝜓 ∨ 𝜒)) ⇒ ⊢ ((𝜑 ∧ (𝜂 ∧ 𝜌)) → 𝜃) | ||
Theorem | negel 33905 | An inference for negation elimination. (Contributed by Giovanni Mascellani, 24-May-2019.) |
⊢ (𝜓 → 𝜒) & ⊢ (𝜑 → ¬ 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → ⊥) | ||
Theorem | botel 33906 | An inference for bottom elimination. (Contributed by Giovanni Mascellani, 24-May-2019.) |
⊢ (𝜑 → ⊥) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | tradd 33907 | Add top ad a conjunct. (Contributed by Giovanni Mascellani, 24-May-2019.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (𝜑 ↔ (⊤ ∧ 𝜓)) | ||
Theorem | sbtru 33908 | Substitution does not change truth. (Contributed by Giovanni Mascellani, 24-May-2019.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ([𝐴 / 𝑥]⊤ ↔ ⊤) | ||
Theorem | sbfal 33909 | Substitution does not change falsity. (Contributed by Giovanni Mascellani, 24-May-2019.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ([𝐴 / 𝑥]⊥ ↔ ⊥) | ||
Theorem | sbcani 33910 | Distribution of class substitution over conjunction, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.) |
⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜒) & ⊢ ([𝐴 / 𝑥]𝜓 ↔ 𝜂) ⇒ ⊢ ([𝐴 / 𝑥](𝜑 ∧ 𝜓) ↔ (𝜒 ∧ 𝜂)) | ||
Theorem | sbcori 33911 | Distribution of class substitution over disjunction, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.) |
⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜒) & ⊢ ([𝐴 / 𝑥]𝜓 ↔ 𝜂) ⇒ ⊢ ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ↔ (𝜒 ∨ 𝜂)) | ||
Theorem | sbcimi 33912 | Distribution of class substitution over implication, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.) |
⊢ 𝐴 ∈ V & ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜒) & ⊢ ([𝐴 / 𝑥]𝜓 ↔ 𝜂) ⇒ ⊢ ([𝐴 / 𝑥](𝜑 → 𝜓) ↔ (𝜒 → 𝜂)) | ||
Theorem | sbceqi 33913 | Distribution of class substitution over equality, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.) |
⊢ 𝐴 ∈ V & ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐷 & ⊢ ⦋𝐴 / 𝑥⦌𝐶 = 𝐸 ⇒ ⊢ ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ 𝐷 = 𝐸) | ||
Theorem | sbcni 33914 | Move class substitution inside a negation, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.) |
⊢ 𝐴 ∈ V & ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜓) ⇒ ⊢ ([𝐴 / 𝑥] ¬ 𝜑 ↔ ¬ 𝜓) | ||
Theorem | sbali 33915 | 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 33916 | 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 33917* | Move universal quantifier in and out of class substitution, with an explicit non-free variable condition. (Contributed by Giovanni Mascellani, 29-May-2019.) |
⊢ Ⅎ𝑦𝐴 ⇒ ⊢ ([𝐴 / 𝑥]∀𝑦𝜑 ↔ ∀𝑦[𝐴 / 𝑥]𝜑) | ||
Theorem | sbcexf 33918* | Move existential quantifier in and out of class substitution, with an explicit non-free variable condition. (Contributed by Giovanni Mascellani, 29-May-2019.) |
⊢ Ⅎ𝑦𝐴 ⇒ ⊢ ([𝐴 / 𝑥]∃𝑦𝜑 ↔ ∃𝑦[𝐴 / 𝑥]𝜑) | ||
Theorem | sbcalfi 33919* | Move universal quantifier in and out of class substitution, with an explicit non-free variable condition and in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.) |
⊢ Ⅎ𝑦𝐴 & ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜓) ⇒ ⊢ ([𝐴 / 𝑥]∀𝑦𝜑 ↔ ∀𝑦𝜓) | ||
Theorem | sbcexfi 33920* | Move existential quantifier in and out of class substitution, with an explicit non-free variable condition and in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.) |
⊢ Ⅎ𝑦𝐴 & ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜓) ⇒ ⊢ ([𝐴 / 𝑥]∃𝑦𝜑 ↔ ∃𝑦𝜓) | ||
Theorem | csbvargi 33921 | The proper substitution of a class for a variable in that variable results in the class (if the class exists), in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ⦋𝐴 / 𝑥⦌𝑥 = 𝐴 | ||
Theorem | csbconstgi 33922* | The proper substitution of a class for a variable in another variable does not modify it, in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ⦋𝐴 / 𝑥⦌𝑦 = 𝑦 | ||
Theorem | spsbcdi 33923 | A lemma for eliminating a universal quantifier, in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.) |
⊢ 𝐴 ∈ V & ⊢ (𝜑 → ∀𝑥𝜒) & ⊢ ([𝐴 / 𝑥]𝜒 ↔ 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | alrimii 33924* | A lemma for introducing a universal quantifier, in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → 𝜓) & ⊢ ([𝑦 / 𝑥]𝜒 ↔ 𝜓) & ⊢ Ⅎ𝑦𝜒 ⇒ ⊢ (𝜑 → ∀𝑥𝜒) | ||
Theorem | spesbcdi 33925 | A lemma for introducing an existential quantifier, in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.) |
⊢ (𝜑 → 𝜓) & ⊢ ([𝐴 / 𝑥]𝜒 ↔ 𝜓) ⇒ ⊢ (𝜑 → ∃𝑥𝜒) | ||
Theorem | exlimddvf 33926 | A lemma for eliminating an existential quantifier. (Contributed by Giovanni Mascellani, 30-May-2019.) |
⊢ (𝜑 → ∃𝑥𝜃) & ⊢ Ⅎ𝑥𝜓 & ⊢ ((𝜃 ∧ 𝜓) → 𝜒) & ⊢ Ⅎ𝑥𝜒 ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
Theorem | exlimddvfi 33927 | A lemma for eliminating an existential quantifier, in inference form. (Contributed by Giovanni Mascellani, 31-May-2019.) |
⊢ (𝜑 → ∃𝑥𝜃) & ⊢ Ⅎ𝑦𝜃 & ⊢ Ⅎ𝑦𝜓 & ⊢ ([𝑦 / 𝑥]𝜃 ↔ 𝜂) & ⊢ ((𝜂 ∧ 𝜓) → 𝜒) & ⊢ Ⅎ𝑦𝜒 ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
Theorem | sbceq1ddi 33928 | A lemma for eliminating inequality, in inference form. (Contributed by Giovanni Mascellani, 31-May-2019.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜓 → 𝜃) & ⊢ ([𝐴 / 𝑥]𝜒 ↔ 𝜃) & ⊢ ([𝐵 / 𝑥]𝜒 ↔ 𝜂) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜂) | ||
Theorem | sbccom2lem 33929* | Lemma for sbccom2 33930. (Contributed by Giovanni Mascellani, 31-May-2019.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦][𝐴 / 𝑥]𝜑) | ||
Theorem | sbccom2 33930* | Commutative law for double class substitution. (Contributed by Giovanni Mascellani, 31-May-2019.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦][𝐴 / 𝑥]𝜑) | ||
Theorem | sbccom2f 33931* | Commutative law for double class substitution, with non free variable condition. (Contributed by Giovanni Mascellani, 31-May-2019.) |
⊢ 𝐴 ∈ V & ⊢ Ⅎ𝑦𝐴 ⇒ ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦][𝐴 / 𝑥]𝜑) | ||
Theorem | sbccom2fi 33932* | Commutative law for double class substitution, with non free variable condition and in inference form. (Contributed by Giovanni Mascellani, 1-Jun-2019.) |
⊢ 𝐴 ∈ V & ⊢ Ⅎ𝑦𝐴 & ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶 & ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜓) ⇒ ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [𝐶 / 𝑦]𝜓) | ||
Theorem | sbcgfi 33933 | Substitution for a variable not free in a wff does not affect it, in inference form. (Contributed by Giovanni Mascellani, 1-Jun-2019.) |
⊢ 𝐴 ∈ V & ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜑) | ||
Theorem | csbcom2fi 33934* | Commutative law for double class substitution in a class, with non free variable condition and in inference form. (Contributed by Giovanni Mascellani, 4-Jun-2019.) |
⊢ 𝐴 ∈ V & ⊢ Ⅎ𝑦𝐴 & ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶 & ⊢ ⦋𝐴 / 𝑥⦌𝐷 = 𝐸 ⇒ ⊢ ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐷 = ⦋𝐶 / 𝑦⦌𝐸 | ||
Theorem | csbgfi 33935 | Substitution for a variable not free in a class does not affect it, 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 33936 | Refutation of falsity, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
⊢ (𝜃 → ¬ ⊥) | ||
Theorem | tsim1 33937 | A Tseitin axiom for logical implication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
⊢ (𝜃 → ((¬ 𝜑 ∨ 𝜓) ∨ ¬ (𝜑 → 𝜓))) | ||
Theorem | tsim2 33938 | A Tseitin axiom for logical implication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
⊢ (𝜃 → (𝜑 ∨ (𝜑 → 𝜓))) | ||
Theorem | tsim3 33939 | A Tseitin axiom for logical implication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
⊢ (𝜃 → (¬ 𝜓 ∨ (𝜑 → 𝜓))) | ||
Theorem | tsbi1 33940 | A Tseitin axiom for logical biimplication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
⊢ (𝜃 → ((¬ 𝜑 ∨ ¬ 𝜓) ∨ (𝜑 ↔ 𝜓))) | ||
Theorem | tsbi2 33941 | A Tseitin axiom for logical biimplication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
⊢ (𝜃 → ((𝜑 ∨ 𝜓) ∨ (𝜑 ↔ 𝜓))) | ||
Theorem | tsbi3 33942 | A Tseitin axiom for logical biimplication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
⊢ (𝜃 → ((𝜑 ∨ ¬ 𝜓) ∨ ¬ (𝜑 ↔ 𝜓))) | ||
Theorem | tsbi4 33943 | A Tseitin axiom for logical biimplication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
⊢ (𝜃 → ((¬ 𝜑 ∨ 𝜓) ∨ ¬ (𝜑 ↔ 𝜓))) | ||
Theorem | tsxo1 33944 | A Tseitin axiom for logical exclusive disjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
⊢ (𝜃 → ((¬ 𝜑 ∨ ¬ 𝜓) ∨ ¬ (𝜑 ⊻ 𝜓))) | ||
Theorem | tsxo2 33945 | A Tseitin axiom for logical exclusive disjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
⊢ (𝜃 → ((𝜑 ∨ 𝜓) ∨ ¬ (𝜑 ⊻ 𝜓))) | ||
Theorem | tsxo3 33946 | A Tseitin axiom for logical exclusive disjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
⊢ (𝜃 → ((𝜑 ∨ ¬ 𝜓) ∨ (𝜑 ⊻ 𝜓))) | ||
Theorem | tsxo4 33947 | A Tseitin axiom for logical exclusive disjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
⊢ (𝜃 → ((¬ 𝜑 ∨ 𝜓) ∨ (𝜑 ⊻ 𝜓))) | ||
Theorem | tsan1 33948 | A Tseitin axiom for logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
⊢ (𝜃 → ((¬ 𝜑 ∨ ¬ 𝜓) ∨ (𝜑 ∧ 𝜓))) | ||
Theorem | tsan2 33949 | A Tseitin axiom for logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
⊢ (𝜃 → (𝜑 ∨ ¬ (𝜑 ∧ 𝜓))) | ||
Theorem | tsan3 33950 | A Tseitin axiom for logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
⊢ (𝜃 → (𝜓 ∨ ¬ (𝜑 ∧ 𝜓))) | ||
Theorem | tsna1 33951 | A Tseitin axiom for logical incompatibility, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
⊢ (𝜃 → ((¬ 𝜑 ∨ ¬ 𝜓) ∨ ¬ (𝜑 ⊼ 𝜓))) | ||
Theorem | tsna2 33952 | A Tseitin axiom for logical incompatibility, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
⊢ (𝜃 → (𝜑 ∨ (𝜑 ⊼ 𝜓))) | ||
Theorem | tsna3 33953 | A Tseitin axiom for logical incompatibility, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
⊢ (𝜃 → (𝜓 ∨ (𝜑 ⊼ 𝜓))) | ||
Theorem | tsor1 33954 | A Tseitin axiom for logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.) |
⊢ (𝜃 → ((𝜑 ∨ 𝜓) ∨ ¬ (𝜑 ∨ 𝜓))) | ||
Theorem | tsor2 33955 | A Tseitin axiom for logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.) |
⊢ (𝜃 → (¬ 𝜑 ∨ (𝜑 ∨ 𝜓))) | ||
Theorem | tsor3 33956 | A Tseitin axiom for logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.) |
⊢ (𝜃 → (¬ 𝜓 ∨ (𝜑 ∨ 𝜓))) | ||
Theorem | ts3an1 33957 | A Tseitin axiom for triple logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.) |
⊢ (𝜃 → ((¬ (𝜑 ∧ 𝜓) ∨ ¬ 𝜒) ∨ (𝜑 ∧ 𝜓 ∧ 𝜒))) | ||
Theorem | ts3an2 33958 | A Tseitin axiom for triple logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.) |
⊢ (𝜃 → ((𝜑 ∧ 𝜓) ∨ ¬ (𝜑 ∧ 𝜓 ∧ 𝜒))) | ||
Theorem | ts3an3 33959 | A Tseitin axiom for triple logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.) |
⊢ (𝜃 → (𝜒 ∨ ¬ (𝜑 ∧ 𝜓 ∧ 𝜒))) | ||
Theorem | ts3or1 33960 | A Tseitin axiom for triple logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.) |
⊢ (𝜃 → (((𝜑 ∨ 𝜓) ∨ 𝜒) ∨ ¬ (𝜑 ∨ 𝜓 ∨ 𝜒))) | ||
Theorem | ts3or2 33961 | A Tseitin axiom for triple logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.) |
⊢ (𝜃 → (¬ (𝜑 ∨ 𝜓) ∨ (𝜑 ∨ 𝜓 ∨ 𝜒))) | ||
Theorem | ts3or3 33962 | 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 biimplications) with other constructs. | ||
Theorem | iuneq2f 33963 | Equality deduction for indexed union. (Contributed by Giovanni Mascellani, 9-Apr-2018.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶) | ||
Theorem | abeq12 33964 | Equality deduction for class abstraction. (Contributed by Giovanni Mascellani, 10-Apr-2018.) |
⊢ (∀𝑥(𝜑 ↔ 𝜓) → {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓}) | ||
Theorem | rabeq12f 33965 | Equality deduction for restricted class abstraction. (Contributed by Giovanni Mascellani, 10-Apr-2018.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓)) → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜓}) | ||
Theorem | csbeq12 33966 | Equality deduction for substitution in class. (Contributed by Giovanni Mascellani, 10-Apr-2018.) |
⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 𝐶 = 𝐷) → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐷) | ||
Theorem | nfbii2 33967 | Equality deduction for not-freeness. (Contributed by Giovanni Mascellani, 10-Apr-2018.) |
⊢ (∀𝑥(𝜑 ↔ 𝜓) → (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓)) | ||
Theorem | sbeqi 33968 | Equality deduction for substitution. (Contributed by Giovanni Mascellani, 10-Apr-2018.) |
⊢ ((𝑥 = 𝑦 ∧ ∀𝑧(𝜑 ↔ 𝜓)) → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜓)) | ||
Theorem | ralbi12f 33969 | Equality deduction for restricted universal quantification. (Contributed by Giovanni Mascellani, 10-Apr-2018.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓)) → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | oprabbi 33970 | Equality deduction for class abstraction of nested ordered pairs. (Contributed by Giovanni Mascellani, 10-Apr-2018.) |
⊢ (∀𝑥∀𝑦∀𝑧(𝜑 ↔ 𝜓) → {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓}) | ||
Theorem | mpt2bi123f 33971* | Equality deduction for maps-to notations with two arguments. (Contributed by Giovanni Mascellani, 10-Apr-2018.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑦𝐶 & ⊢ Ⅎ𝑦𝐷 & ⊢ Ⅎ𝑥𝐶 & ⊢ Ⅎ𝑥𝐷 ⇒ ⊢ (((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝐸 = 𝐹) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐷 ↦ 𝐹)) | ||
Theorem | iuneq12f 33972 | Equality deduction for indexed unions. (Contributed by Giovanni Mascellani, 10-Apr-2018.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝐶 = 𝐷) → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷) | ||
Theorem | iineq12f 33973 | Equality deduction for indexed intersections. (Contributed by Giovanni Mascellani, 10-Apr-2018.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝐶 = 𝐷) → ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐷) | ||
Theorem | opabbi 33974 | Equality deduction for class abstraction of ordered pairs. (Contributed by Giovanni Mascellani, 10-Apr-2018.) |
⊢ (∀𝑥∀𝑦(𝜑 ↔ 𝜓) → {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑦〉 ∣ 𝜓}) | ||
Theorem | mptbi12f 33975 | 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 | scottexf 33976* | A version of scottex 8748 with non-free variables instead of distinct variables. (Contributed by Giovanni Mascellani, 19-Aug-2018.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} ∈ V | ||
Theorem | scott0f 33977* | A version of scott0 8749 with non-free variables instead of distinct variables. (Contributed by Giovanni Mascellani, 19-Aug-2018.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝐴 = ∅ ↔ {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} = ∅) | ||
Theorem | scottn0f 33978* | A version of scott0f 33977 with inequalities instead of equalities. (Contributed by Giovanni Mascellani, 19-Aug-2018.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝐴 ≠ ∅ ↔ {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} ≠ ∅) | ||
Theorem | ac6s3f 33979* | Generalization of the Axiom of Choice to classes, with bound-variable hypothesis. (Contributed by Giovanni Mascellani, 19-Aug-2018.) |
⊢ Ⅎ𝑦𝜓 & ⊢ 𝐴 ∈ V & ⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦𝜑 → ∃𝑓∀𝑥 ∈ 𝐴 𝜓) | ||
Theorem | ac6s6 33980* | 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 33981* | 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 33982 | Extend the definition of a class to include the range Cartesian product class. |
class (𝐴 ⋉ 𝐵) | ||
Theorem | elv 33983 | New way (elv 33983, el2v 33984 theorems and el3v 33987 theorems) to shorten some proofs. Inference forms (with 𝐴 ∈ V hypotheses) of the general theorems (proving 𝐴 ∈ 𝑉 →) may be superfluous. (Contributed by Peter Mazsa, 13-Oct-2018.) |
⊢ (𝑥 ∈ V → 𝜑) ⇒ ⊢ 𝜑 | ||
Theorem | el2v 33984 | New way (elv 33983, el2v 33984 theorems and el3v 33987 theorems) to shorten some proofs. Inference forms (with 𝐴 ∈ V and 𝐵 ∈ V hypotheses) of the general theorems (proving (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) →) may be superfluous. (Contributed by Peter Mazsa, 13-Oct-2018.) |
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → 𝜑) ⇒ ⊢ 𝜑 | ||
Theorem | el2v1 33985 | New way (elv 33983, el2v 33984 theorems and el3v 33987 theorems) to shorten some proofs. (Contributed by Peter Mazsa, 23-Oct-2018.) |
⊢ ((𝑥 ∈ V ∧ 𝜑) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | el2v2 33986 | New way (elv 33983, el2v 33984 theorems and el3v 33987 theorems) to shorten some proofs. (Contributed by Peter Mazsa, 23-Oct-2018.) |
⊢ ((𝜑 ∧ 𝑦 ∈ V) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | el3v 33987 | New way (elv 33983, el2v 33984 theorems and el3v 33987 theorems) to shorten some proofs. Inference forms (with 𝐴 ∈ V, 𝐵 ∈ V and 𝐶 ∈ V hypotheses) of the general theorems (proving (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) →) may be superfluous. (Contributed by Peter Mazsa, 13-Oct-2018.) |
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → 𝜑) ⇒ ⊢ 𝜑 | ||
Theorem | el3v1 33988 | New way (elv 33983, el2v 33984 theorems and el3v 33987 theorems) to shorten some proofs. (Contributed by Peter Mazsa, 16-Oct-2020.) |
⊢ ((𝑥 ∈ V ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜓 ∧ 𝜒) → 𝜃) | ||
Theorem | el3v2 33989 | New way (elv 33983, el2v 33984 theorems and el3v 33987 theorems) to shorten some proofs. (Contributed by Peter Mazsa, 16-Oct-2020.) |
⊢ ((𝜑 ∧ 𝑦 ∈ V ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜒) → 𝜃) | ||
Theorem | el3v3 33990 | New way (elv 33983, el2v 33984 theorems and el3v 33987 theorems) to shorten some proofs. (Contributed by Peter Mazsa, 16-Oct-2020.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝑧 ∈ V) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜃) | ||
Theorem | el3v12 33991 | New way (elv 33983, el2v 33984 theorems and el3v 33987 theorems) to shorten some proofs. (Contributed by Peter Mazsa, 11-Jul-2021.) |
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝜒) → 𝜃) ⇒ ⊢ (𝜒 → 𝜃) | ||
Theorem | el3v13 33992 | New way (elv 33983, el2v 33984 theorems and el3v 33987 theorems) to shorten some proofs. (Contributed by Peter Mazsa, 11-Jul-2021.) |
⊢ ((𝑥 ∈ V ∧ 𝜓 ∧ 𝑧 ∈ V) → 𝜃) ⇒ ⊢ (𝜓 → 𝜃) | ||
Theorem | el3v23 33993 | New way (elv 33983, el2v 33984 theorems and el3v 33987 theorems) to shorten some proofs. (Contributed by Peter Mazsa, 11-Jul-2021.) |
⊢ ((𝜑 ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → 𝜃) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | biancom 33994 | Commuting conjunction in a biconditional. (Contributed by Peter Mazsa, 17-Jun-2018.) |
⊢ (𝜑 ↔ (𝜒 ∧ 𝜓)) ⇒ ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) | ||
Theorem | biancomd 33995 | Commuting conjunction in a biconditional, deduction form. (Contributed by Peter Mazsa, 3-Oct-2018.) |
⊢ (𝜑 → (𝜓 ↔ (𝜃 ∧ 𝜒))) ⇒ ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃))) | ||
Theorem | anbi1ci 33996 | Introduce a left and the same right conjunct to the sides of a logical equivalence. (Contributed by Peter Mazsa, 7-Mar-2020.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ((𝜒 ∧ 𝜑) ↔ (𝜓 ∧ 𝜒)) | ||
Theorem | anbi1cd 33997 | Introduce a left and the same right conjunct to the sides of a logical equivalence, deduction form. (Contributed by Peter Mazsa, 22-May-2021.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ((𝜃 ∧ 𝜓) ↔ (𝜒 ∧ 𝜃))) | ||
Theorem | an2anr 33998 | Double commutation in conjunction. (Contributed by Peter Mazsa, 27-Jun-2019.) |
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜓 ∧ 𝜑) ∧ (𝜃 ∧ 𝜒))) | ||
Theorem | anan 33999 | Multiple commutations in conjunction. (Contributed by Peter Mazsa, 7-Mar-2020.) |
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ ((𝜑 ∧ 𝜃) ∧ 𝜏)) ↔ ((𝜓 ∧ 𝜃) ∧ (𝜑 ∧ (𝜒 ∧ 𝜏)))) | ||
Theorem | triantru3 34000 | A wff is equivalent to its conjunctions with truths. (Contributed by Peter Mazsa, 30-Nov-2018.) |
⊢ 𝜑 & ⊢ 𝜓 ⇒ ⊢ (𝜒 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |