Home | Metamath
Proof Explorer Theorem List (p. 361 of 462) | < 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-28971) |
Hilbert Space Explorer
(28972-30494) |
Users' Mathboxes
(30495-46134) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | tsor3 36001 | A Tseitin axiom for logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.) |
⊢ (𝜃 → (¬ 𝜓 ∨ (𝜑 ∨ 𝜓))) | ||
Theorem | ts3an1 36002 | A Tseitin axiom for triple logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.) |
⊢ (𝜃 → ((¬ (𝜑 ∧ 𝜓) ∨ ¬ 𝜒) ∨ (𝜑 ∧ 𝜓 ∧ 𝜒))) | ||
Theorem | ts3an2 36003 | A Tseitin axiom for triple logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.) |
⊢ (𝜃 → ((𝜑 ∧ 𝜓) ∨ ¬ (𝜑 ∧ 𝜓 ∧ 𝜒))) | ||
Theorem | ts3an3 36004 | A Tseitin axiom for triple logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.) |
⊢ (𝜃 → (𝜒 ∨ ¬ (𝜑 ∧ 𝜓 ∧ 𝜒))) | ||
Theorem | ts3or1 36005 | A Tseitin axiom for triple logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.) |
⊢ (𝜃 → (((𝜑 ∨ 𝜓) ∨ 𝜒) ∨ ¬ (𝜑 ∨ 𝜓 ∨ 𝜒))) | ||
Theorem | ts3or2 36006 | A Tseitin axiom for triple logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.) |
⊢ (𝜃 → (¬ (𝜑 ∨ 𝜓) ∨ (𝜑 ∨ 𝜓 ∨ 𝜒))) | ||
Theorem | ts3or3 36007 | 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 36008 | Equality deduction for indexed union. (Contributed by Giovanni Mascellani, 9-Apr-2018.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶) | ||
Theorem | rabeq12f 36009 | Equality deduction for restricted class abstraction. (Contributed by Giovanni Mascellani, 10-Apr-2018.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓)) → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜓}) | ||
Theorem | csbeq12 36010 | Equality deduction for substitution in class. (Contributed by Giovanni Mascellani, 10-Apr-2018.) |
⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 𝐶 = 𝐷) → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐷) | ||
Theorem | sbeqi 36011 | Equality deduction for substitution. (Contributed by Giovanni Mascellani, 10-Apr-2018.) |
⊢ ((𝑥 = 𝑦 ∧ ∀𝑧(𝜑 ↔ 𝜓)) → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜓)) | ||
Theorem | ralbi12f 36012 | Equality deduction for restricted universal quantification. (Contributed by Giovanni Mascellani, 10-Apr-2018.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓)) → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | oprabbi 36013 | Equality deduction for class abstraction of nested ordered pairs. (Contributed by Giovanni Mascellani, 10-Apr-2018.) |
⊢ (∀𝑥∀𝑦∀𝑧(𝜑 ↔ 𝜓) → {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓}) | ||
Theorem | mpobi123f 36014* | Equality deduction for maps-to notations with two arguments. (Contributed by Giovanni Mascellani, 10-Apr-2018.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑦𝐶 & ⊢ Ⅎ𝑦𝐷 & ⊢ Ⅎ𝑥𝐶 & ⊢ Ⅎ𝑥𝐷 ⇒ ⊢ (((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝐸 = 𝐹) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐷 ↦ 𝐹)) | ||
Theorem | iuneq12f 36015 | Equality deduction for indexed unions. (Contributed by Giovanni Mascellani, 10-Apr-2018.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝐶 = 𝐷) → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷) | ||
Theorem | iineq12f 36016 | Equality deduction for indexed intersections. (Contributed by Giovanni Mascellani, 10-Apr-2018.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝐶 = 𝐷) → ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐷) | ||
Theorem | opabbi 36017 | Equality deduction for class abstraction of ordered pairs. (Contributed by Giovanni Mascellani, 10-Apr-2018.) |
⊢ (∀𝑥∀𝑦(𝜑 ↔ 𝜓) → {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑦〉 ∣ 𝜓}) | ||
Theorem | mptbi12f 36018 | 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 36019 | 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 36020* | A version of scottex 9484 with nonfree variables instead of distinct variables. (Contributed by Giovanni Mascellani, 19-Aug-2018.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} ∈ V | ||
Theorem | scott0f 36021* | A version of scott0 9485 with nonfree variables instead of distinct variables. (Contributed by Giovanni Mascellani, 19-Aug-2018.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝐴 = ∅ ↔ {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} = ∅) | ||
Theorem | scottn0f 36022* | A version of scott0f 36021 with inequalities instead of equalities. (Contributed by Giovanni Mascellani, 19-Aug-2018.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝐴 ≠ ∅ ↔ {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} ≠ ∅) | ||
Theorem | ac6s3f 36023* | Generalization of the Axiom of Choice to classes, with bound-variable hypothesis. (Contributed by Giovanni Mascellani, 19-Aug-2018.) |
⊢ Ⅎ𝑦𝜓 & ⊢ 𝐴 ∈ V & ⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦𝜑 → ∃𝑓∀𝑥 ∈ 𝐴 𝜓) | ||
Theorem | ac6s6 36024* | 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 36025* | 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 36026 | Extend the definition of a class to include the range Cartesian product class. |
class (𝐴 ⋉ 𝐵) | ||
Syntax | ccoss 36027 | Extend the definition of a class to include the class of cosets by a class. (Read: the class of cosets by 𝑅.) |
class ≀ 𝑅 | ||
Syntax | ccoels 36028 | Extend the definition of a class to include the class of coelements on a class. (Read: the class of coelements on 𝐴.) |
class ∼ 𝐴 | ||
Syntax | crels 36029 | Extend the definition of a class to include the relation class. |
class Rels | ||
Syntax | cssr 36030 | Extend the definition of a class to include the subset class. |
class S | ||
Syntax | crefs 36031 | Extend the definition of a class to include the reflexivity class. |
class Refs | ||
Syntax | crefrels 36032 | Extend the definition of a class to include the reflexive relations class. |
class RefRels | ||
Syntax | wrefrel 36033 | Extend the definition of a wff to include the reflexive relation predicate. (Read: 𝑅 is a reflexive relation.) |
wff RefRel 𝑅 | ||
Syntax | ccnvrefs 36034 | Extend the definition of a class to include the converse reflexivity class. |
class CnvRefs | ||
Syntax | ccnvrefrels 36035 | Extend the definition of a class to include the converse reflexive relations class. |
class CnvRefRels | ||
Syntax | wcnvrefrel 36036 | Extend the definition of a wff to include the converse reflexive relation predicate. (Read: 𝑅 is a converse reflexive relation.) |
wff CnvRefRel 𝑅 | ||
Syntax | csyms 36037 | Extend the definition of a class to include the symmetry class. |
class Syms | ||
Syntax | csymrels 36038 | Extend the definition of a class to include the symmetry relations class. |
class SymRels | ||
Syntax | wsymrel 36039 | Extend the definition of a wff to include the symmetry relation predicate. (Read: 𝑅 is a symmetric relation.) |
wff SymRel 𝑅 | ||
Syntax | ctrs 36040 | Extend the definition of a class to include the transitivity class (but cf. the transitive class defined in df-tr 5151). |
class Trs | ||
Syntax | ctrrels 36041 | Extend the definition of a class to include the transitive relations class. |
class TrRels | ||
Syntax | wtrrel 36042 | Extend the definition of a wff to include the transitive relation predicate. (Read: 𝑅 is a transitive relation.) |
wff TrRel 𝑅 | ||
Syntax | ceqvrels 36043 | Extend the definition of a class to include the equivalence relations class. |
class EqvRels | ||
Syntax | weqvrel 36044 | Extend the definition of a wff to include the equivalence relation predicate. (Read: 𝑅 is an equivalence relation.) |
wff EqvRel 𝑅 | ||
Syntax | ccoeleqvrels 36045 | Extend the definition of a class to include the coelement equivalence relations class. |
class CoElEqvRels | ||
Syntax | wcoeleqvrel 36046 | Extend the definition of a wff to include the coelement equivalence relation predicate. (Read: the coelement equivalence relation on 𝐴.) |
wff CoElEqvRel 𝐴 | ||
Syntax | credunds 36047 | Extend the definition of a class to include the redundancy class. |
class Redunds | ||
Syntax | wredund 36048 | Extend the definition of a wff to include the redundancy predicate. (Read: 𝐴 is redundant with respect to 𝐵 in 𝐶.) |
wff 𝐴 Redund 〈𝐵, 𝐶〉 | ||
Syntax | wredundp 36049 | Extend wff definition to include the redundancy operator for propositions. |
wff redund (𝜑, 𝜓, 𝜒) | ||
Syntax | cdmqss 36050 | Extend the definition of a class to include the domain quotients class. |
class DomainQss | ||
Syntax | wdmqs 36051 | Extend the definition of a wff to include the domain quotient predicate. (Read: the domain quotient of 𝑅 is 𝐴.) |
wff 𝑅 DomainQs 𝐴 | ||
Syntax | cers 36052 | Extend the definition of a class to include the equivalence relations on their domain quotients class. |
class Ers | ||
Syntax | werALTV 36053 | 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 36054 | Extend the definition of a class to include the membership equivalence relations class. |
class MembErs | ||
Syntax | wmember 36055 | 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 36056 | Extend the definition of a class to include the function set class. |
class Funss | ||
Syntax | cfunsALTV 36057 | Extend the definition of a class to include the functions class, i.e., the function relations class. |
class FunsALTV | ||
Syntax | wfunALTV 36058 | 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 36059 | Extend the definition of a class to include the disjoint set class. |
class Disjss | ||
Syntax | cdisjs 36060 | Extend the definition of a class to include the disjoints class, i.e., the disjoint relations class. |
class Disjs | ||
Syntax | wdisjALTV 36061 | 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 36062 | Extend the definition of a class to include the disjoint elements class, i.e., the disjoint elementhood relations class. |
class ElDisjs | ||
Syntax | weldisj 36063 | 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 𝐴 | ||
Theorem | el2v1 36064 | New way (elv 3407, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 23-Oct-2018.) |
⊢ ((𝑥 ∈ V ∧ 𝜑) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | el3v 36065 | New way (elv 3407, 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 36066 | New way (elv 3407, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 16-Oct-2020.) |
⊢ ((𝑥 ∈ V ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜓 ∧ 𝜒) → 𝜃) | ||
Theorem | el3v2 36067 | New way (elv 3407, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 16-Oct-2020.) |
⊢ ((𝜑 ∧ 𝑦 ∈ V ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜒) → 𝜃) | ||
Theorem | el3v3 36068 | New way (elv 3407, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 16-Oct-2020.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝑧 ∈ V) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜃) | ||
Theorem | el3v12 36069 | New way (elv 3407, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 11-Jul-2021.) |
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝜒) → 𝜃) ⇒ ⊢ (𝜒 → 𝜃) | ||
Theorem | el3v13 36070 | New way (elv 3407, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 11-Jul-2021.) |
⊢ ((𝑥 ∈ V ∧ 𝜓 ∧ 𝑧 ∈ V) → 𝜃) ⇒ ⊢ (𝜓 → 𝜃) | ||
Theorem | el3v23 36071 | New way (elv 3407, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 11-Jul-2021.) |
⊢ ((𝜑 ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → 𝜃) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | an2anr 36072 | Double commutation in conjunction. (Contributed by Peter Mazsa, 27-Jun-2019.) |
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜓 ∧ 𝜑) ∧ (𝜃 ∧ 𝜒))) | ||
Theorem | anan 36073 | Multiple commutations in conjunction. (Contributed by Peter Mazsa, 7-Mar-2020.) |
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ ((𝜑 ∧ 𝜃) ∧ 𝜏)) ↔ ((𝜓 ∧ 𝜃) ∧ (𝜑 ∧ (𝜒 ∧ 𝜏)))) | ||
Theorem | triantru3 36074 | A wff is equivalent to its conjunctions with truths. (Contributed by Peter Mazsa, 30-Nov-2018.) |
⊢ 𝜑 & ⊢ 𝜓 ⇒ ⊢ (𝜒 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒)) | ||
Theorem | eqeltr 36075 | Substitution of equal classes into elementhood relation. (Contributed by Peter Mazsa, 22-Jul-2017.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶) | ||
Theorem | eqelb 36076 | Substitution of equal classes into elementhood relation. (Contributed by Peter Mazsa, 17-Jul-2019.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐴 ∈ 𝐶) ↔ (𝐴 = 𝐵 ∧ 𝐵 ∈ 𝐶)) | ||
Theorem | eqeqan2d 36077 | Implication of introducing a new equality. (Contributed by Peter Mazsa, 17-Apr-2019.) |
⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ ((𝐴 = 𝐵 ∧ 𝜑) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)) | ||
Theorem | inres2 36078 | Two ways of expressing the restriction of an intersection. (Contributed by Peter Mazsa, 5-Jun-2021.) |
⊢ ((𝑅 ↾ 𝐴) ∩ 𝑆) = ((𝑅 ∩ 𝑆) ↾ 𝐴) | ||
Theorem | coideq 36079 | Equality theorem for composition of two classes. (Contributed by Peter Mazsa, 23-Sep-2021.) |
⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐴) = (𝐵 ∘ 𝐵)) | ||
Theorem | nexmo1 36080 | 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 | 3albii 36081 | Inference adding three universal quantifiers to both sides of an equivalence. (Contributed by Peter Mazsa, 10-Aug-2018.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∀𝑥∀𝑦∀𝑧𝜑 ↔ ∀𝑥∀𝑦∀𝑧𝜓) | ||
Theorem | 3ralbii 36082 | Inference adding three restricted universal quantifiers to both sides of an equivalence. (Contributed by Peter Mazsa, 25-Jul-2019.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓) | ||
Theorem | ssrabi 36083 | Inference of restricted abstraction subclass from implication. (Contributed by Peter Mazsa, 26-Oct-2022.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓} | ||
Theorem | rabbieq 36084 | Equivalent wff's correspond to restricted class abstractions which are equal with the same class. (Contributed by Peter Mazsa, 8-Jul-2019.) |
⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜑} & ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜓} | ||
Theorem | rabimbieq 36085 | 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 36086* | Intersection with class abstraction. (Contributed by Peter Mazsa, 21-Jul-2021.) |
⊢ 𝐴 = (𝐵 ∩ 𝐶) & ⊢ 𝐵 = {𝑥 ∣ 𝜑} ⇒ ⊢ 𝐴 = {𝑥 ∈ 𝐶 ∣ 𝜑} | ||
Theorem | abeqinbi 36087* | Intersection with class abstraction and equivalent wff's. (Contributed by Peter Mazsa, 21-Jul-2021.) |
⊢ 𝐴 = (𝐵 ∩ 𝐶) & ⊢ 𝐵 = {𝑥 ∣ 𝜑} & ⊢ (𝑥 ∈ 𝐶 → (𝜑 ↔ 𝜓)) ⇒ ⊢ 𝐴 = {𝑥 ∈ 𝐶 ∣ 𝜓} | ||
Theorem | rabeqel 36088* | Class element of a restricted class abstraction. (Contributed by Peter Mazsa, 24-Jul-2021.) |
⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜑} & ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐶 ∈ 𝐵 ↔ (𝜓 ∧ 𝐶 ∈ 𝐴)) | ||
Theorem | eqrelf 36089* | The equality connective between relations. (Contributed by Peter Mazsa, 25-Jun-2019.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝐵 ⇒ ⊢ ((Rel 𝐴 ∧ Rel 𝐵) → (𝐴 = 𝐵 ↔ ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 ↔ 〈𝑥, 𝑦〉 ∈ 𝐵))) | ||
Theorem | releleccnv 36090 | Elementhood in a converse 𝑅-coset when 𝑅 is a relation. (Contributed by Peter Mazsa, 9-Dec-2018.) |
⊢ (Rel 𝑅 → (𝐴 ∈ [𝐵]◡𝑅 ↔ 𝐴𝑅𝐵)) | ||
Theorem | releccnveq 36091* | Equality of converse 𝑅-coset and converse 𝑆-coset when 𝑅 and 𝑆 are relations. (Contributed by Peter Mazsa, 27-Jul-2019.) |
⊢ ((Rel 𝑅 ∧ Rel 𝑆) → ([𝐴]◡𝑅 = [𝐵]◡𝑆 ↔ ∀𝑥(𝑥𝑅𝐴 ↔ 𝑥𝑆𝐵))) | ||
Theorem | opelvvdif 36092 | Negated elementhood of ordered pair. (Contributed by Peter Mazsa, 14-Jan-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (〈𝐴, 𝐵〉 ∈ ((V × V) ∖ 𝑅) ↔ ¬ 〈𝐴, 𝐵〉 ∈ 𝑅)) | ||
Theorem | vvdifopab 36093* | Ordered-pair class abstraction defined by a negation. (Contributed by Peter Mazsa, 25-Jun-2019.) |
⊢ ((V × V) ∖ {〈𝑥, 𝑦〉 ∣ 𝜑}) = {〈𝑥, 𝑦〉 ∣ ¬ 𝜑} | ||
Theorem | brvdif 36094 | Binary relation with universal complement is the negation of the relation. (Contributed by Peter Mazsa, 1-Jul-2018.) |
⊢ (𝐴(V ∖ 𝑅)𝐵 ↔ ¬ 𝐴𝑅𝐵) | ||
Theorem | brvdif2 36095 | Binary relation with universal complement. (Contributed by Peter Mazsa, 14-Jul-2018.) |
⊢ (𝐴(V ∖ 𝑅)𝐵 ↔ ¬ 〈𝐴, 𝐵〉 ∈ 𝑅) | ||
Theorem | brvvdif 36096 | Binary relation with the complement under the universal class of ordered pairs. (Contributed by Peter Mazsa, 9-Nov-2018.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴((V × V) ∖ 𝑅)𝐵 ↔ ¬ 𝐴𝑅𝐵)) | ||
Theorem | brvbrvvdif 36097 | Binary relation with the complement under the universal class of ordered pairs is the same as with universal complement. (Contributed by Peter Mazsa, 28-Nov-2018.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴((V × V) ∖ 𝑅)𝐵 ↔ 𝐴(V ∖ 𝑅)𝐵)) | ||
Theorem | brcnvep 36098 | The converse of the binary epsilon relation. (Contributed by Peter Mazsa, 30-Jan-2018.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴◡ E 𝐵 ↔ 𝐵 ∈ 𝐴)) | ||
Theorem | elecALTV 36099 | Elementhood in the 𝑅-coset of 𝐴. Theorem 72 of [Suppes] p. 82. (I think we should replace elecg 8423 with this original form of Suppes. Peter Mazsa). (Contributed by Mario Carneiro, 9-Jul-2014.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐵 ∈ [𝐴]𝑅 ↔ 𝐴𝑅𝐵)) | ||
Theorem | brcnvepres 36100 | Restricted converse epsilon binary relation. (Contributed by Peter Mazsa, 10-Feb-2018.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵(◡ E ↾ 𝐴)𝐶 ↔ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |