Home | Metamath
Proof ExplorerTheorem List
(p. 276 of 315)
| < Previous Next > |

Browser slow? Try the
Unicode version. |

Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs

Color key: | Metamath Proof Explorer
(1-21492) |
Hilbert Space Explorer
(21493-23015) |
Users' Mathboxes
(23016-31423) |

Type | Label | Description | ||||||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|

Statement | ||||||||||||||||||||||||||||||||

Theorem | dp2cl 27501 | Define the closure for the decimal fraction constructor if both values are reals. (Contributed by David A. Wheeler, 15-May-2015.) | ||||||||||||||||||||||||||||||

_ | ||||||||||||||||||||||||||||||||

Theorem | dpval 27502 | Define the value of the decimal point operator. See df-dp 27500. (Contributed by David A. Wheeler, 15-May-2015.) | ||||||||||||||||||||||||||||||

_ | ||||||||||||||||||||||||||||||||

Theorem | dpcl 27503 | Prove that the closure of the decimal point is as we have defined it. See df-dp 27500. (Contributed by David A. Wheeler, 15-May-2015.) | ||||||||||||||||||||||||||||||

Theorem | dpfrac1 27504 | Prove a simple equivalence involving the decimal point. See df-dp 27500 and dpcl 27503. (Contributed by David A. Wheeler, 15-May-2015.) | ||||||||||||||||||||||||||||||

; | ||||||||||||||||||||||||||||||||

18.22.8 Signum (sgn or sign)
function | ||||||||||||||||||||||||||||||||

Syntax | csgn 27505 | Extend class notation to include the Signum function. | ||||||||||||||||||||||||||||||

sgn | ||||||||||||||||||||||||||||||||

Definition | df-sgn 27506 | Signum function. Pronounced "signum" , otherwise it might be confused with "sine". Defined as "sgn" in ISO 80000-2:2009(E) operation 2-9.13. It is named "sign" (with the same definition) in the "NIST Digital Library of Mathematical Functions" , front introduction, "Common Notations and Definitions" section at http://dlmf.nist.gov/front/introduction#Sx4. We define this over (df-xr 8868) instead of so that it can accept and . Note that df-psgn 26816 defines the sign of a permutation, which is different. Value shown in sgnval 27507. (Contributed by David A. Wheeler, 15-May-2015.) | ||||||||||||||||||||||||||||||

sgn | ||||||||||||||||||||||||||||||||

Theorem | sgnval 27507 | Value of Signum function. Pronounced "signum" . See df-sgn 27506. (Contributed by David A. Wheeler, 15-May-2015.) | ||||||||||||||||||||||||||||||

sgn | ||||||||||||||||||||||||||||||||

Theorem | sgn0 27508 | Proof that signum of 0 is 0. (Contributed by David A. Wheeler, 15-May-2015.) | ||||||||||||||||||||||||||||||

sgn | ||||||||||||||||||||||||||||||||

Theorem | sgnp 27509 | Proof that signum of positive extended real is 1. (Contributed by David A. Wheeler, 15-May-2015.) | ||||||||||||||||||||||||||||||

sgn | ||||||||||||||||||||||||||||||||

Theorem | sgnrrp 27510 | Proof that signum of positive reals is 1. (Contributed by David A. Wheeler, 18-May-2015.) | ||||||||||||||||||||||||||||||

sgn | ||||||||||||||||||||||||||||||||

Theorem | sgn1 27511 | Proof that the signum of 1 is 1. (Contributed by David A. Wheeler, 26-Jun-2016.) | ||||||||||||||||||||||||||||||

sgn | ||||||||||||||||||||||||||||||||

Theorem | sgnpnf 27512 | Proof that the signum of is 1. (Contributed by David A. Wheeler, 26-Jun-2016.) | ||||||||||||||||||||||||||||||

sgn | ||||||||||||||||||||||||||||||||

Theorem | sgnn 27513 | Proof that signum of negative extended real is -1. (Contributed by David A. Wheeler, 15-May-2015.) | ||||||||||||||||||||||||||||||

sgn | ||||||||||||||||||||||||||||||||

Theorem | sgnmnf 27514 | Proof that the signum of is -1. (Contributed by David A. Wheeler, 26-Jun-2016.) | ||||||||||||||||||||||||||||||

sgn | ||||||||||||||||||||||||||||||||

18.22.9 Ceiling function | ||||||||||||||||||||||||||||||||

Syntax | ccei 27515 | Extend class notation to include the ceiling function. | ||||||||||||||||||||||||||||||

⌈ | ||||||||||||||||||||||||||||||||

Definition | df-ceiling 27516 |
The ceiling function. Defined in ISO 80000-2:2009(E) operation 2-9.18 and
the "NIST Digital Library of Mathematical Functions" , front
introduction,
"Common Notations and Definitions" section at
http://dlmf.nist.gov/front/introduction#Sx4.
By convention metamath users tend to expand this construct directly, instead of using the definition. However, we want to make sure this is separately and formally defined. Proof ceicl 10951 shows that the ceiling function returns an integer when provided a real. Formalized by David A. Wheeler. (Contributed by David A. Wheeler, 19-May-2015.) | ||||||||||||||||||||||||||||||

⌈ | ||||||||||||||||||||||||||||||||

Theorem | ceilingval 27517 | The value of the ceiling function. (Contributed by David A. Wheeler, 19-May-2015.) | ||||||||||||||||||||||||||||||

⌈ | ||||||||||||||||||||||||||||||||

Theorem | ceilingcl 27518 | Closure of the ceiling function; the real work is in ceicl 10951. (Contributed by David A. Wheeler, 19-May-2015.) | ||||||||||||||||||||||||||||||

⌈ | ||||||||||||||||||||||||||||||||

18.22.10 Logarithm laws generalized to an
arbitrary base - logbDefine "log using an arbitrary base" function and then prove some of its properties. This builds on previous work by Stefan O'Rear. Note that logb is generalized to an arbitrary base and arbitrary parameter in , but it doesn't accept infinities as arguments, unlike . Metamath doesn't care what letters are used to represent classes. Usually classes begin with the letter "A", but here we use "B" and "X" to more clearly distinguish between "base" and "other parameter of log". There are different ways this could be defined in Metamath. The approach used here is intentionally similar to existing 2-parameter Metamath functions. The way defined here supports two notations, logb and logb where is the base and is the other parameter. An alternative would be to support the notational form logb; that looks a little more like traditional notation, but is different than other 2-parameter functions. It's not obvious to me which is better, so here we try out one way as an experiment. Feedback and help welcome. | ||||||||||||||||||||||||||||||||

Syntax | clogb 27519 | Extend class notation to include the logarithm generalized to an arbitrary base. | ||||||||||||||||||||||||||||||

logb | ||||||||||||||||||||||||||||||||

Definition | df-logb 27520* | Define the logb operator. This is the logarithm generalized to an arbitrary base. It can be used as logb for "log base B of X". In the most common traditional notation, base B is a subscript of "log". You could also use logb, which looks like a less-common notation that some use where the base is a preceding superscript. Note: This definition doesn't prevent bases of 1 or 0; proofs may need to forbid them. (Contributed by David A. Wheeler, 21-Jan-2017.) | ||||||||||||||||||||||||||||||

logb | ||||||||||||||||||||||||||||||||

Theorem | logbval 27521 | Define the value of the logb function, the logarithm generalized to an arbitrary base, when used as infix. Most Metamath statements select variables in order of their use, but to make the order clearer we use "B" for base and "X" for the other operand here. Proof is similar to modval 10971. (Contributed by David A. Wheeler, 21-Jan-2017.) (Revised by David A. Wheeler, 16-Jul-2017.) | ||||||||||||||||||||||||||||||

logb | ||||||||||||||||||||||||||||||||

Theorem | logb2aval 27522 | Define the value of the logb function, the logarithm generalized to an arbitrary base, when used in the 2-argument form logb (Contributed by David A. Wheeler, 21-Jan-2017.) (Revised by David A. Wheeler, 16-Jul-2017.) | ||||||||||||||||||||||||||||||

logb | ||||||||||||||||||||||||||||||||

Theorem | eldifpr 27523 | Membership in a set with two elements removed. Similar to eldifsn 3752 and eldiftp 27524. (Contributed by Mario Carneiro, 18-Jul-2017.) | ||||||||||||||||||||||||||||||

Theorem | eldiftp 27524 | Membership in a set with three elements removed. Similar to eldifsn 3752 and eldifpr 27523. (Contributed by David A. Wheeler, 22-Jul-2017.) | ||||||||||||||||||||||||||||||

Theorem | logeq0im1 27525 | if then (Contributed by David A. Wheeler, 22-Jul-2017.) | ||||||||||||||||||||||||||||||

Theorem | logccne0 27526 | log isn't 0 if argument isn't 0 or 1. Unlike logne0 19952, this handles complex numbers. (Contributed by David A. Wheeler, 17-Jul-2017.) | ||||||||||||||||||||||||||||||

Theorem | logccne0ALT 27527 | log isn't 0 if argument isn't 0 or 1. Unlike logne0 19952, this handles complex numbers. (Contributed by David A. Wheeler, 17-Jul-2017.) | ||||||||||||||||||||||||||||||

Theorem | logbcl 27528 | General logarithm closure. (Contributed by David A. Wheeler, 17-Jul-2017.) | ||||||||||||||||||||||||||||||

logb | ||||||||||||||||||||||||||||||||

Theorem | logbid1 27529 | General logarithm when base and arg match (Contributed by David A. Wheeler, 22-Jul-2017.) | ||||||||||||||||||||||||||||||

logb | ||||||||||||||||||||||||||||||||

18.22.11 Logarithm laws generalized to an
arbitrary base - log_Define "log using an arbitrary base" function and then prove some of its properties. This builds on previous work by Stefan O'Rear. This supports the notational form logb; that looks a little more like traditional notation, but is different than other 2-parameter functions. E.G., log_;; | ||||||||||||||||||||||||||||||||

Syntax | clog_ 27530 | Extend class notation to include the logarithm generalized to an arbitrary base. | ||||||||||||||||||||||||||||||

log_ | ||||||||||||||||||||||||||||||||

Definition | df-log_ 27531* | Define the log_ operator. This is the logarithm generalized to an arbitrary base. It can be used as log_ for "log base B of X". This formulation suggested by Mario Carneiro. (Contributed by David A. Wheeler, 14-Jul-2017.) | ||||||||||||||||||||||||||||||

log_ | ||||||||||||||||||||||||||||||||

18.22.12 MiscellaneousMiscellaneous proofs. | ||||||||||||||||||||||||||||||||

Theorem | 5m4e1 27532 | Prove that 5 - 4 = 1. (Contributed by David A. Wheeler, 31-Jan-2017.) | ||||||||||||||||||||||||||||||

Theorem | 2p2ne5 27533 | Prove that . In George Orwell's "1984", Part One, Chapter Seven, the protagonist Winston notes that, "In the end the Party would announce that two and two made five, and you would have to believe it." http://www.sparknotes.com/lit/1984/section4.rhtml. More generally, the phrase has come to represent an obviously false dogma one may be required to believe. See the Wikipedia article for more about this: https://en.wikipedia.org/wiki/2_%2B_2_%3D_5. Unsurprisingly, we can easily prove that this claim is false. (Contributed by David A. Wheeler, 31-Jan-2017.) | ||||||||||||||||||||||||||||||

Theorem | resolution 27534 | Resolution rule. This is the primary inference rule in some automated theorem provers such as prover9. The resolution rule can be traced back to Davis and Putnam (1960). (Contributed by David A. Wheeler, 9-Feb-2017.) | ||||||||||||||||||||||||||||||

18.23 Mathbox for Alan Sare | ||||||||||||||||||||||||||||||||

18.23.1 Conventional Metamath proofs, some
derived from VD proofs | ||||||||||||||||||||||||||||||||

Theorem | iidn3 27535 | idn3 27657 without virtual deduction connectives. Special theorem needed for Alan Sare's virtual deduction translation tool. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | ee222 27536 | e222 27678 without virtual deduction connectives. Special theorem needed for Alan Sare's virtual deduction translation tool. (Contributed by Alan Sare, 7-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | ee3bir 27537 | Right-biconditional form of e3 27782 without virtual deduction connectives. Special theorem needed for Alan Sare's virtual deduction translation tool. (Contributed by Alan Sare, 22-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | ee13 27538 | e13 27793 without virtual deduction connectives. Special theorem needed for Alan Sare's virtual deduction translation tool. (Contributed by Alan Sare, 28-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | ee121 27539 | e121 27698 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | ee122 27540 | e122 27695 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | ee333 27541 | e333 27778 without virtual deductions. (Contributed by Alan Sare, 17-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | ee323 27542 | e323 27811 without virtual deductions. (Contributed by Alan Sare, 17-Apr-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | 3ornot23 27543 | If the second and third disjuncts of a true triple disjunction are false, then the first disjunct is true. Automatically derived from 3ornot23VD 27893. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | orbi1r 27544 | orbi1 688 with order of disjuncts reversed. Derived from orbi1rVD 27894. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | bitr3 27545 | Closed nested implication form of bitr3i 244. Derived automatically from bitr3VD 27895. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | 3orbi123 27546 | pm4.39 843 with a 3-conjunct antecedent. This proof is 3orbi123VD 27896 automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | syl5imp 27547 | Closed form of syl5 30. Derived automatically from syl5impVD 27909. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | impexp3a 27548 |
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. After the
User's Proof was completed it was minimized. The completed User's Proof
before minimization is not shown. (Contributed by Alan Sare,
18-Mar-2012.) (Proof modification is discouraged.)
(New usage is discouraged.)
| ||||||||||||||||||||||||||||||

Theorem | com3rgbi 27549 |
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. The
completed Virtual Deduction Proof (not shown) was minimized. The
minimized proof is shown.
(Contributed by Alan Sare, 18-Mar-2012.)
(Proof modification is discouraged.) (New usage is discouraged.)
| ||||||||||||||||||||||||||||||

Theorem | impexp3acom3r 27550 |
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. The
completed Virtual Deduction Proof (not shown) was minimized. The
minimized proof is shown. (Contributed by Alan Sare, 18-Mar-2012.)
(Proof modification is discouraged.) (New usage is discouraged.)
| ||||||||||||||||||||||||||||||

Theorem | ee1111 27551 |
Non-virtual deduction form of e1111 27717. (Contributed by Alan Sare,
18-Mar-2012.)
(Proof modification is discouraged.) (New usage is discouraged.)
The following User's Proof is a Virtual Deduction proof
completed automatically by the tools program completeusersproof.cmd,
which invokes Mel O'Cat's mmj2 and Norm Megill's Metamath Proof
Assistant. The completed Virtual Deduction Proof (not shown) was
minimized. The minimized proof is shown.
| ||||||||||||||||||||||||||||||

Theorem | pm2.43bgbi 27552 |
Logical equivalence of a 2-left-nested implication and a 1-left-nested
implicated
when two antecedents of the former implication are identical.
(Contributed by Alan Sare, 18-Mar-2012.)
(Proof modification is discouraged.) (New usage is discouraged.)
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. The
completed Virtual
Deduction Proof (not shown) was minimized. The minimized proof is
shown.
| ||||||||||||||||||||||||||||||

Theorem | pm2.43cbi 27553 |
Logical equivalence of a 3-left-nested implication and a 2-left-nested
implicated when two antecedents of the former implication are identical.
(Contributed by Alan Sare, 18-Mar-2012.)
(Proof modification is discouraged.) (New usage is discouraged.)
The following User's Proof is
a Virtual Deduction proof completed automatically by the tools program
completeusersproof.cmd, which invokes Mel O'Cat's mmj2 and Norm Megill's
Metamath Proof Assistant. The completed Virtual Deduction Proof (not
shown) was minimized. The minimized proof is shown.
| ||||||||||||||||||||||||||||||

Theorem | ee233 27554 |
Non-virtual deduction form of e233 27810. (Contributed by Alan Sare,
18-Mar-2012.)
(Proof modification is discouraged.) (New usage is discouraged.)
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. The
completed Virtual
Deduction Proof (not shown) was minimized. The minimized proof is
shown.
| ||||||||||||||||||||||||||||||

Theorem | imbi12 27555 | Implication form of imbi12i 318. imbi12 27555 is imbi12VD 27919 without virtual deductions and was automatically derived from imbi12VD 27919 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | imbi13 27556 | Join three logical equivalences to form equivalence of implications. imbi13 27556 is imbi13VD 27920 without virtual deductions and was automatically derived from imbi13VD 27920 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | ee33 27557 |
Non-virtual deduction form of e33 27779. (Contributed by Alan Sare,
18-Mar-2012.) (Proof modification is discouraged.)
(New usage is discouraged.)
The following User's Proof is a Virtual Deduction proof
completed automatically by the tools program completeusersproof.cmd,
which invokes Mel O'Cat's mmj2 and Norm Megill's Metamath Proof
Assistant. The completed Virtual Deduction Proof (not shown) was
minimized. The minimized proof is shown.
| ||||||||||||||||||||||||||||||

Theorem | con5 27558 | Bi-conditional contraposition variation. This proof is con5VD 27946 automatically translated and minimized. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | con5i 27559 | Inference form of con5 27558. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | exlimexi 27560 | Inference similar to Theorem 19.23 of [Margaris] p. 90. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | sb5ALT 27561* | Equivalence for substitution. Alternate proof of sb5 2041. This proof is sb5ALTVD 27959 automatically translated and minimized. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | eexinst01 27562 | exinst01 27667 without virtual deductions. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | eexinst11 27563 | exinst11 27668 without virtual deductions. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | vk15.4j 27564 | Excercise 4j of Unit 15 of "Understanding Symbolic Logic", Fifth Edition (2008), by Virginia Klenk. This proof is the minimized Hilbert-style axiomatic version of the Fitch-style Natural Deduction proof found on page 442 of Klenk and was automatically derived from that proof. vk15.4j 27564 is vk15.4jVD 27960 automatically translated and minimized. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | notnot2ALT 27565 | Converse of double negation. Alternate proof of notnot2 106. This proof is notnot2ALTVD 27961 automatically translated and minimized. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | con3ALT 27566 | Contraposition. Alternate proof of con3 128. This proof is con3ALTVD 27962 automatically translated and minimized. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | ssralv2 27567* |
Quantification restricted to a subclass for two quantifiers. ssralv 3240
for two quantifiers. The proof of ssralv2 27567 was automatically generated
by minimizing the automatically translated proof of ssralv2VD 27912. The
automatic translation is by the tools program
translate_{without}_overwriting.cmd
(Contributed by Alan Sare,
18-Feb-2012.) (Proof modification is discouraged.)
(New usage is discouraged.)
| ||||||||||||||||||||||||||||||

Theorem | sbc3org 27568 | sbcorg 3039 with a 3-disjuncts. This proof is sbc3orgVD 27897 automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | alrim3con13v 27569* | Closed form of alrimi 1749 with 2 additional conjuncts having no occurences of the quantifying variable. This proof is 19.21a3con13vVD 27898 automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | rspsbc2 27570* | rspsbc 3072 with two quantifying variables. This proof is rspsbc2VD 27901 automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | sbcoreleleq 27571* | Substitution of a set variable for another set variable in a 3-conjunct formula. Derived automatically from sbcoreleleqVD 27905. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | tratrb 27572* | If a class is transitive and any two distinct elements of the class are E-comparable, then every element of that class is transitive. Derived automatically from tratrbVD 27907. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | 3ax5 27573 | ax-5 1546 for a 3 element left-nested implication. Derived automatically from 3ax5VD 27908. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | ordelordALT 27574 | An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36. This is an alternate proof of ordelord 4415 using the Axiom of Regularity indirectly through dford2 7318. dford2 is a weaker definition of ordinal number. Given the Axiom of Regularity, it need not be assumed that because this is inferred by the Axiom of Regularity. ordelordALT 27574 is ordelordALTVD 27913 without virtual deductions and was automatically derived from ordelordALTVD 27913 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | sbcim2g 27575 | Distribution of class substitution over a left-nested implication. Similar to sbcimg 3035. sbcim2g 27575 is sbcim2gVD 27921 without virtual deductions and was automatically derived from sbcim2gVD 27921 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | sbcbi 27576 | Implication form of sbcbiiOLD 3050. sbcbi 27576 is sbcbiVD 27922 without virtual deductions and was automatically derived from sbcbiVD 27922 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | trsbc 27577* | Formula-building inference rule for class substitution, substituting a class variable for the set variable of the transitivity predicate. trsbc 27577 is trsbcVD 27923 without virtual deductions and was automatically derived from trsbcVD 27923 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | truniALT 27578* | The union of a class of transitive sets is transitive. Alternate proof of truni 4130. truniALT 27578 is truniALTVD 27924 without virtual deductions and was automatically derived from truniALTVD 27924 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | sbcssOLD 27579 | Distribute proper substitution through a subclass relation. This theorem was automatically derived from sbcssVD 27929. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | onfrALTlem5 27580* | Lemma for onfrALT 27587. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | onfrALTlem4 27581* | Lemma for onfrALT 27587. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | onfrALTlem3 27582* | Lemma for onfrALT 27587. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | ggen31 27583* | gen31 27663 without virtual deductions. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | onfrALTlem2 27584* | |||||||||||||||||||||||||||||||

Theorem | cbvexsv 27585* | A theorem pertaining to the substitution for an existentially quantified variable when the substituted variable does not occur in the quantified wff. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | onfrALTlem1 27586* | |||||||||||||||||||||||||||||||

Theorem | onfrALT 27587 | The epsilon relation is foundational on the class of ordinal numbers. onfrALT 27587 is an alternate proof of onfr 4432. onfrALTVD 27937 is the Virtual Deduction proof from which onfrALT 27587 is derived. The Virtual Deduction proof mirrors the working proof of onfr 4432 which is the main part of the proof of Theorem 7.12 of the first edition of TakeutiZaring. The proof of the corresponding Proposition 7.12 of [TakeutiZaring] p. 38 (second edition) does not contain the working proof equivalent of onfrALTVD 27937. This theorem does not rely on the Axiom of Regularity. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | csbeq2g 27588 | Formula-building implication rule for class substitution. Closed form of csbeq2i 3110. csbeq2g 27588 is derived from the virtual deduction proof csbeq2gVD 27938. (Contributed by Alan Sare, 10-Nov-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | 19.41rg 27589 | Closed form of right-to-left implication of 19.41 1819, Theorem 19.41 of [Margaris] p. 90. Derived from 19.41rgVD 27948. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | opelopab4 27590* | Ordered pair membership in a class abstraction of pairs. Compare to elopab 4273. (Contributed by Alan Sare, 8-Feb-2014.) (Revised by Mario Carneiro, 6-May-2015.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | 2pm13.193 27591 | pm13.193 27012 for two variables. pm13.193 27012 is Theorem *13.193 in [WhiteheadRussell] p. 179. Derived from 2pm13.193VD 27949. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | hbntal 27592 | A closed form of hbn 1724. hbnt 1728 is another closed form of hbn 1724. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | hbimpg 27593 | A closed form of hbim 1729. Derived from hbimpgVD 27950. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | hbalg 27594 | Closed form of hbal 1713. Derived from hbalgVD 27951. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | hbexg 27595 | Closed form of nfex 1771. Derived from hbexgVD 27952. (Contributed by Alan Sare, 8-Feb-2014.) (Revised by Mario Carneiro, 12-Dec-2016.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | a9e2eq 27596* | Alternate form of a9e 1895 for non-distinct , and . a9e2eq 27596 is derived from a9e2eqVD 27953. (Contributed by Alan Sare, 25-Mar-2014.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | a9e2nd 27597* | If at least two sets exist (dtru 4202) , then the same is true expressed in an alternate form similar to the form of a9e 1895. a9e2nd 27597 is derived from a9e2ndVD 27954. (Contributed by Alan Sare, 25-Mar-2014.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | a9e2ndeq 27598* | "At least two sets exist" expressed in the form of dtru 4202 is logically equivalent to the same expressed in a form similar to a9e 1895 if dtru 4202 is false implies . a9e2ndeq 27598 is derived from a9e2ndeqVD 27955. (Contributed by Alan Sare, 25-Mar-2014.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | 2sb5nd 27599* | Equivalence for double substitution 2sb5 2056 without distinct , requirement. 2sb5nd 27599 is derived from 2sb5ndVD 27956. (Contributed by Alan Sare, 30-Apr-2014.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | 2uasbanh 27600* | Distribute the unabbreviated form of proper substitution in and out of a conjunction. 2uasbanh 27600 is derived from 2uasbanhVD 27957. (Contributed by Alan Sare, 31-May-2014.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |