![]() |
Metamath
Proof Explorer Theorem List (p. 371 of 479) | < 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | tsbi1 37001 | A Tseitin axiom for logical biconditional, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
β’ (π β ((Β¬ π β¨ Β¬ π) β¨ (π β π))) | ||
Theorem | tsbi2 37002 | A Tseitin axiom for logical biconditional, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
β’ (π β ((π β¨ π) β¨ (π β π))) | ||
Theorem | tsbi3 37003 | A Tseitin axiom for logical biconditional, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
β’ (π β ((π β¨ Β¬ π) β¨ Β¬ (π β π))) | ||
Theorem | tsbi4 37004 | A Tseitin axiom for logical biconditional, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
β’ (π β ((Β¬ π β¨ π) β¨ Β¬ (π β π))) | ||
Theorem | tsxo1 37005 | A Tseitin axiom for logical exclusive disjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
β’ (π β ((Β¬ π β¨ Β¬ π) β¨ Β¬ (π β» π))) | ||
Theorem | tsxo2 37006 | A Tseitin axiom for logical exclusive disjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
β’ (π β ((π β¨ π) β¨ Β¬ (π β» π))) | ||
Theorem | tsxo3 37007 | A Tseitin axiom for logical exclusive disjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
β’ (π β ((π β¨ Β¬ π) β¨ (π β» π))) | ||
Theorem | tsxo4 37008 | A Tseitin axiom for logical exclusive disjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
β’ (π β ((Β¬ π β¨ π) β¨ (π β» π))) | ||
Theorem | tsan1 37009 | A Tseitin axiom for logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
β’ (π β ((Β¬ π β¨ Β¬ π) β¨ (π β§ π))) | ||
Theorem | tsan2 37010 | A Tseitin axiom for logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
β’ (π β (π β¨ Β¬ (π β§ π))) | ||
Theorem | tsan3 37011 | A Tseitin axiom for logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
β’ (π β (π β¨ Β¬ (π β§ π))) | ||
Theorem | tsna1 37012 | A Tseitin axiom for logical incompatibility, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
β’ (π β ((Β¬ π β¨ Β¬ π) β¨ Β¬ (π βΌ π))) | ||
Theorem | tsna2 37013 | A Tseitin axiom for logical incompatibility, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
β’ (π β (π β¨ (π βΌ π))) | ||
Theorem | tsna3 37014 | A Tseitin axiom for logical incompatibility, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
β’ (π β (π β¨ (π βΌ π))) | ||
Theorem | tsor1 37015 | A Tseitin axiom for logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.) |
β’ (π β ((π β¨ π) β¨ Β¬ (π β¨ π))) | ||
Theorem | tsor2 37016 | A Tseitin axiom for logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.) |
β’ (π β (Β¬ π β¨ (π β¨ π))) | ||
Theorem | tsor3 37017 | A Tseitin axiom for logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.) |
β’ (π β (Β¬ π β¨ (π β¨ π))) | ||
Theorem | ts3an1 37018 | A Tseitin axiom for triple logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.) |
β’ (π β ((Β¬ (π β§ π) β¨ Β¬ π) β¨ (π β§ π β§ π))) | ||
Theorem | ts3an2 37019 | A Tseitin axiom for triple logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.) |
β’ (π β ((π β§ π) β¨ Β¬ (π β§ π β§ π))) | ||
Theorem | ts3an3 37020 | A Tseitin axiom for triple logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.) |
β’ (π β (π β¨ Β¬ (π β§ π β§ π))) | ||
Theorem | ts3or1 37021 | A Tseitin axiom for triple logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.) |
β’ (π β (((π β¨ π) β¨ π) β¨ Β¬ (π β¨ π β¨ π))) | ||
Theorem | ts3or2 37022 | A Tseitin axiom for triple logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.) |
β’ (π β (Β¬ (π β¨ π) β¨ (π β¨ π β¨ π))) | ||
Theorem | ts3or3 37023 | 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 37024 | Equality deduction for indexed union. (Contributed by Giovanni Mascellani, 9-Apr-2018.) |
β’ β²π₯π΄ & β’ β²π₯π΅ β β’ (π΄ = π΅ β βͺ π₯ β π΄ πΆ = βͺ π₯ β π΅ πΆ) | ||
Theorem | rabeq12f 37025 | Equality deduction for restricted class abstraction. (Contributed by Giovanni Mascellani, 10-Apr-2018.) |
β’ β²π₯π΄ & β’ β²π₯π΅ β β’ ((π΄ = π΅ β§ βπ₯ β π΄ (π β π)) β {π₯ β π΄ β£ π} = {π₯ β π΅ β£ π}) | ||
Theorem | csbeq12 37026 | Equality deduction for substitution in class. (Contributed by Giovanni Mascellani, 10-Apr-2018.) |
β’ ((π΄ = π΅ β§ βπ₯ πΆ = π·) β β¦π΄ / π₯β¦πΆ = β¦π΅ / π₯β¦π·) | ||
Theorem | sbeqi 37027 | Equality deduction for substitution. (Contributed by Giovanni Mascellani, 10-Apr-2018.) |
β’ ((π₯ = π¦ β§ βπ§(π β π)) β ([π₯ / π§]π β [π¦ / π§]π)) | ||
Theorem | ralbi12f 37028 | Equality deduction for restricted universal quantification. (Contributed by Giovanni Mascellani, 10-Apr-2018.) |
β’ β²π₯π΄ & β’ β²π₯π΅ β β’ ((π΄ = π΅ β§ βπ₯ β π΄ (π β π)) β (βπ₯ β π΄ π β βπ₯ β π΅ π)) | ||
Theorem | oprabbi 37029 | Equality deduction for class abstraction of nested ordered pairs. (Contributed by Giovanni Mascellani, 10-Apr-2018.) |
β’ (βπ₯βπ¦βπ§(π β π) β {β¨β¨π₯, π¦β©, π§β© β£ π} = {β¨β¨π₯, π¦β©, π§β© β£ π}) | ||
Theorem | mpobi123f 37030* | Equality deduction for maps-to notations with two arguments. (Contributed by Giovanni Mascellani, 10-Apr-2018.) |
β’ β²π₯π΄ & β’ β²π₯π΅ & β’ β²π¦π΄ & β’ β²π¦π΅ & β’ β²π¦πΆ & β’ β²π¦π· & β’ β²π₯πΆ & β’ β²π₯π· β β’ (((π΄ = π΅ β§ πΆ = π·) β§ βπ₯ β π΄ βπ¦ β πΆ πΈ = πΉ) β (π₯ β π΄, π¦ β πΆ β¦ πΈ) = (π₯ β π΅, π¦ β π· β¦ πΉ)) | ||
Theorem | iuneq12f 37031 | Equality deduction for indexed unions. (Contributed by Giovanni Mascellani, 10-Apr-2018.) |
β’ β²π₯π΄ & β’ β²π₯π΅ β β’ ((π΄ = π΅ β§ βπ₯ β π΄ πΆ = π·) β βͺ π₯ β π΄ πΆ = βͺ π₯ β π΅ π·) | ||
Theorem | iineq12f 37032 | Equality deduction for indexed intersections. (Contributed by Giovanni Mascellani, 10-Apr-2018.) |
β’ β²π₯π΄ & β’ β²π₯π΅ β β’ ((π΄ = π΅ β§ βπ₯ β π΄ πΆ = π·) β β© π₯ β π΄ πΆ = β© π₯ β π΅ π·) | ||
Theorem | opabbi 37033 | Equality deduction for class abstraction of ordered pairs. (Contributed by Giovanni Mascellani, 10-Apr-2018.) |
β’ (βπ₯βπ¦(π β π) β {β¨π₯, π¦β© β£ π} = {β¨π₯, π¦β© β£ π}) | ||
Theorem | mptbi12f 37034 | 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 37035 | Commutativity of logic disjunction, in double deduction form. Should not be moved to main, see PR #3034 in Github. Use orcomd 870 instead. (Contributed by Giovanni Mascellani, 19-Mar-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ (π β (π β (π β¨ π))) β β’ (π β (π β (π β¨ π))) | ||
Theorem | scottexf 37036* | A version of scottex 9880 with nonfree variables instead of distinct variables. (Contributed by Giovanni Mascellani, 19-Aug-2018.) |
β’ β²π¦π΄ & β’ β²π₯π΄ β β’ {π₯ β π΄ β£ βπ¦ β π΄ (rankβπ₯) β (rankβπ¦)} β V | ||
Theorem | scott0f 37037* | A version of scott0 9881 with nonfree variables instead of distinct variables. (Contributed by Giovanni Mascellani, 19-Aug-2018.) |
β’ β²π¦π΄ & β’ β²π₯π΄ β β’ (π΄ = β β {π₯ β π΄ β£ βπ¦ β π΄ (rankβπ₯) β (rankβπ¦)} = β ) | ||
Theorem | scottn0f 37038* | A version of scott0f 37037 with inequalities instead of equalities. (Contributed by Giovanni Mascellani, 19-Aug-2018.) |
β’ β²π¦π΄ & β’ β²π₯π΄ β β’ (π΄ β β β {π₯ β π΄ β£ βπ¦ β π΄ (rankβπ₯) β (rankβπ¦)} β β ) | ||
Theorem | ac6s3f 37039* | Generalization of the Axiom of Choice to classes, with bound-variable hypothesis. (Contributed by Giovanni Mascellani, 19-Aug-2018.) |
β’ β²π¦π & β’ π΄ β V & β’ (π¦ = (πβπ₯) β (π β π)) β β’ (βπ₯ β π΄ βπ¦π β βπβπ₯ β π΄ π) | ||
Theorem | ac6s6 37040* | 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 37041* | 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 37042 | Extend the definition of a class to include the range Cartesian product class. |
class (π΄ β π΅) | ||
Syntax | ccoss 37043 | Extend the definition of a class to include the class of cosets by a class. (Read: the class of cosets by π .) |
class β π | ||
Syntax | ccoels 37044 | Extend the definition of a class to include the class of coelements on a class. (Read: the class of coelements on π΄.) |
class βΌ π΄ | ||
Syntax | crels 37045 | Extend the definition of a class to include the relation class. |
class Rels | ||
Syntax | cssr 37046 | Extend the definition of a class to include the subset class. |
class S | ||
Syntax | crefs 37047 | Extend the definition of a class to include the reflexivity class. |
class Refs | ||
Syntax | crefrels 37048 | Extend the definition of a class to include the reflexive relations class. |
class RefRels | ||
Syntax | wrefrel 37049 | Extend the definition of a wff to include the reflexive relation predicate. (Read: π is a reflexive relation.) |
wff RefRel π | ||
Syntax | ccnvrefs 37050 | Extend the definition of a class to include the converse reflexivity class. |
class CnvRefs | ||
Syntax | ccnvrefrels 37051 | Extend the definition of a class to include the converse reflexive relations class. |
class CnvRefRels | ||
Syntax | wcnvrefrel 37052 | Extend the definition of a wff to include the converse reflexive relation predicate. (Read: π is a converse reflexive relation.) |
wff CnvRefRel π | ||
Syntax | csyms 37053 | Extend the definition of a class to include the symmetry class. |
class Syms | ||
Syntax | csymrels 37054 | Extend the definition of a class to include the symmetry relations class. |
class SymRels | ||
Syntax | wsymrel 37055 | Extend the definition of a wff to include the symmetry relation predicate. (Read: π is a symmetric relation.) |
wff SymRel π | ||
Syntax | ctrs 37056 | 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 37057 | Extend the definition of a class to include the transitive relations class. |
class TrRels | ||
Syntax | wtrrel 37058 | Extend the definition of a wff to include the transitive relation predicate. (Read: π is a transitive relation.) |
wff TrRel π | ||
Syntax | ceqvrels 37059 | Extend the definition of a class to include the equivalence relations class. |
class EqvRels | ||
Syntax | weqvrel 37060 | Extend the definition of a wff to include the equivalence relation predicate. (Read: π is an equivalence relation.) |
wff EqvRel π | ||
Syntax | ccoeleqvrels 37061 | Extend the definition of a class to include the coelement equivalence relations class. |
class CoElEqvRels | ||
Syntax | wcoeleqvrel 37062 | Extend the definition of a wff to include the coelement equivalence relation predicate. (Read: the coelement equivalence relation on π΄.) |
wff CoElEqvRel π΄ | ||
Syntax | credunds 37063 | Extend the definition of a class to include the redundancy class. |
class Redunds | ||
Syntax | wredund 37064 | Extend the definition of a wff to include the redundancy predicate. (Read: π΄ is redundant with respect to π΅ in πΆ.) |
wff π΄ Redund β¨π΅, πΆβ© | ||
Syntax | wredundp 37065 | Extend wff definition to include the redundancy operator for propositions. |
wff redund (π, π, π) | ||
Syntax | cdmqss 37066 | Extend the definition of a class to include the domain quotients class. |
class DomainQss | ||
Syntax | wdmqs 37067 | Extend the definition of a wff to include the domain quotient predicate. (Read: the domain quotient of π is π΄.) |
wff π DomainQs π΄ | ||
Syntax | cers 37068 | Extend the definition of a class to include the equivalence relations on their domain quotients class. |
class Ers | ||
Syntax | werALTV 37069 | 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 | ccomembers 37070 | Extend the definition of a class to include the comember equivalence relations class. |
class CoMembErs | ||
Syntax | wcomember 37071 | Extend the definition of a wff to include the comember equivalence relation predicate. (Read: the comember equivalence relation on π΄, or, the restricted coelement equivalence relation on its domain quotient π΄.) |
wff CoMembEr π΄ | ||
Syntax | cfunss 37072 | Extend the definition of a class to include the function set class. |
class Funss | ||
Syntax | cfunsALTV 37073 | Extend the definition of a class to include the functions class, i.e., the function relations class. |
class FunsALTV | ||
Syntax | wfunALTV 37074 | 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 37075 | Extend the definition of a class to include the disjoint set class. |
class Disjss | ||
Syntax | cdisjs 37076 | Extend the definition of a class to include the disjoints class, i.e., the disjoint relations class. |
class Disjs | ||
Syntax | wdisjALTV 37077 | 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 37078 | Extend the definition of a class to include the disjoint elements class, i.e., the disjoint element relations class. |
class ElDisjs | ||
Syntax | weldisj 37079 | Extend the definition of a wff to include the disjoint element predicate, i.e., the disjoint element relation predicate. (Read: the elements of π΄ are disjoint.) |
wff ElDisj π΄ | ||
Syntax | wantisymrel 37080 | Extend the definition of a wff to include the antisymmetry relation predicate. (Read: π is an antisymmetric relation.) |
wff AntisymRel π | ||
Syntax | cparts 37081 | Extend the definition of a class to include the partitions class, i.e., the partition relations class. |
class Parts | ||
Syntax | wpart 37082 | Extend the definition of a wff to include the partition predicate, i.e., the partition relation predicate. (Read: π΄ is a partition by π .) |
wff π Part π΄ | ||
Syntax | cmembparts 37083 | Extend the definition of a class to include the member partitions class, i.e., the member partition relations class. |
class MembParts | ||
Syntax | wmembpart 37084 | Extend the definition of a wff to include the member partition predicate, i.e., the member partition relation predicate. (Read: π΄ is a member partition.) |
wff MembPart π΄ | ||
Theorem | el2v1 37085 | New way (elv 3481, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 23-Oct-2018.) |
β’ ((π₯ β V β§ π) β π) β β’ (π β π) | ||
Theorem | el3v 37086 | New way (elv 3481, 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 37087 | New way (elv 3481, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 16-Oct-2020.) |
β’ ((π₯ β V β§ π β§ π) β π) β β’ ((π β§ π) β π) | ||
Theorem | el3v2 37088 | New way (elv 3481, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 16-Oct-2020.) |
β’ ((π β§ π¦ β V β§ π) β π) β β’ ((π β§ π) β π) | ||
Theorem | el3v3 37089 | New way (elv 3481, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 16-Oct-2020.) |
β’ ((π β§ π β§ π§ β V) β π) β β’ ((π β§ π) β π) | ||
Theorem | el3v12 37090 | New way (elv 3481, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 11-Jul-2021.) |
β’ ((π₯ β V β§ π¦ β V β§ π) β π) β β’ (π β π) | ||
Theorem | el3v13 37091 | New way (elv 3481, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 11-Jul-2021.) |
β’ ((π₯ β V β§ π β§ π§ β V) β π) β β’ (π β π) | ||
Theorem | el3v23 37092 | New way (elv 3481, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 11-Jul-2021.) |
β’ ((π β§ π¦ β V β§ π§ β V) β π) β β’ (π β π) | ||
Theorem | anan 37093 | Multiple commutations in conjunction. (Contributed by Peter Mazsa, 7-Mar-2020.) |
β’ ((((π β§ π) β§ π) β§ ((π β§ π) β§ π)) β ((π β§ π) β§ (π β§ (π β§ π)))) | ||
Theorem | triantru3 37094 | A wff is equivalent to its conjunctions with truths. (Contributed by Peter Mazsa, 30-Nov-2018.) |
β’ π & β’ π β β’ (π β (π β§ π β§ π)) | ||
Theorem | bianbi 37095 | Exchanging conjunction in a biconditional. (Contributed by Peter Mazsa, 31-Jul-2023.) |
β’ (π β (π β§ π)) & β’ (π β π) β β’ (π β (π β§ π)) | ||
Theorem | bianim 37096 | Exchanging conjunction in a biconditional. (Contributed by Peter Mazsa, 31-Jul-2023.) |
β’ (π β (π β§ π)) & β’ (π β (π β π)) β β’ (π β (π β§ π)) | ||
Theorem | biorfd 37097 | A wff is equivalent to its disjunction with falsehood, deduction form. (Contributed by Peter Mazsa, 22-Aug-2023.) |
β’ (π β Β¬ π) β β’ (π β (π β (π β¨ π))) | ||
Theorem | eqbrtr 37098 | Substitution of equal classes in binary relation. (Contributed by Peter Mazsa, 14-Jun-2024.) |
β’ ((π΄ = π΅ β§ π΅π πΆ) β π΄π πΆ) | ||
Theorem | eqbrb 37099 | Substitution of equal classes in a binary relation. (Contributed by Peter Mazsa, 14-Jun-2024.) |
β’ ((π΄ = π΅ β§ π΄π πΆ) β (π΄ = π΅ β§ π΅π πΆ)) | ||
Theorem | eqeltr 37100 | Substitution of equal classes into element relation. (Contributed by Peter Mazsa, 22-Jul-2017.) |
β’ ((π΄ = π΅ β§ π΅ β πΆ) β π΄ β πΆ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |