Home | Metamath
Proof Explorer Theorem List (p. 286 of 324) | < Previous Next > |
Browser slow? Try the
Unicode version. |
Color key: | Metamath Proof Explorer
(1-22341) |
Hilbert Space Explorer
(22342-23864) |
Users' Mathboxes
(23865-32387) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | e03 28501 | A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | ee03 28502 | e03 28501 without virtual deductions. (Contributed by Alan Sare, 17-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | e03an 28503 | Conjunction form of e03 28501. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | ee03an 28504 | Conjunction form of ee03 28502. (Contributed by Alan Sare, 18-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | e30 28505 | A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | ee30 28506 | e30 28505 without virtual deductions. (Contributed by Alan Sare, 17-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | e30an 28507 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | ee30an 28508 | Conjunction form of ee30 28506. (Contributed by Alan Sare, 17-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | e13 28509 | A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | e13an 28510 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | ee13an 28511 | e13an 28510 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | e31 28512 | A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | ee31 28513 | e31 28512 without virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | e31an 28514 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | ee31an 28515 | e31an 28514 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | e23 28516 | A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | e23an 28517 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | ee23an 28518 | e23an 28517 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | e32 28519 | A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | ee32 28520 | e32 28519 without virtual deductions. (Contributed by Alan Sare, 18-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | e32an 28521 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | ee32an 28522 | e33an 28496 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | e123 28523 | A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | ee123 28524 | e123 28523 without virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | el123 28525 | A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | e233 28526 | A virtual deduction elimination rule. (Contributed by Alan Sare, 29-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | e323 28527 | A virtual deduction elimination rule. (Contributed by Alan Sare, 17-Apr-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | e000 28528 | A virtual deduction elimination rule. The non-virtual deduction form of e000 28528 is the virtual deduction form. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | e00 28529 | Elimination rule identical to mp2 9. The non-virtual deduction form is the virtual deduction form, which is mp2 9. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | e00an 28530 | Elimination rule identical to mp2an 654. The non-virtual deduction form is the virtual deduction form, which is mp2an 654. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | eel00cT 28531 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | eelTT 28532 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | e0_ 28533 | Elimination rule identical to ax-mp 8. The non-virtual deduction form is the virtual deduction form, which is ax-mp 8. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | eelT 28534 | An elimination deduction. (Contributed by Alan Sare, 5-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | eel0cT 28535 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | eelT0 28536 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | e0bi 28537 | Elimination rule identical to mpbi 200. The non-virtual deduction form is the virtual deduction form, which is mpbi 200. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | e0bir 28538 | Elimination rule identical to mpbir 201. The non-virtual deduction form is the virtual deduction form, which is mpbir 201. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | uun0.1 28539 | Convention notation form of un0.1 28540. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | un0.1 28540 | is the constant true, a tautology ( see: df-tru 1325). Kleene's "empty conjunction" is logically equivalent to . In a virtual deduction we shall interpret to be the empty wff or the empty collection of virtual hypotheses. in a virtual deduction translated into conventional notation we shall interpret to be Kleene's empty conjunction. If is true given the empty collection of virtual hypotheses and another collection of virtual hypotheses, then it is true given only the other collection of virtual hypotheses. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | uunT1 28541 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 3-Dec-2015.) (Proof modification is discouraged.) (New usage is discouraged.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | uunT1p1 28542 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | uunT21 28543 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 3-Dec-2015.) (Proof modification is discouraged.) (New usage is discouraged.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | uun121 28544 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | uun121p1 28545 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | uun132 28546 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | uun132p1 28547 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | anabss7p1 28548 | A deduction unionizing a non-unionized collection of virtual hypotheses. This would have been named uun221 if the 0th permutation did not exist in set.mm as anabss7 795. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | un10 28549 | A unionizing deduction (Contributed by Alan Sare, 28-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | un01 28550 | A unionizing deduction (Contributed by Alan Sare, 28-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | un2122 28551 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 3-Dec-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | uun2131 28552 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | uun2131p1 28553 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | uunTT1 28554 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | uunTT1p1 28555 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | uunTT1p2 28556 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | uunT11 28557 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | uunT11p1 28558 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | uunT11p2 28559 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | uunT12 28560 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | uunT12p1 28561 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | uunT12p2 28562 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | uunT12p3 28563 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | uunT12p4 28564 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | uunT12p5 28565 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | uun111 28566 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | 3anidm12p1 28567 | A deduction unionizing a non-unionized collection of virtual hypotheses. 3anidm12 1241 denotes the deduction which would have been named uun112 if it did not pre-exist in set.mm. This second permutation's name is based on this pre-existing name. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | 3anidm12p2 28568 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | uun123 28569 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | uun123p1 28570 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | uun123p2 28571 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | uun123p3 28572 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | uun123p4 28573 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | uun2221 28574 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 30-Dec-2016.) (Proof modification is discouraged.) (New usage is discouraged.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | uun2221p1 28575 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | uun2221p2 28576 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | 3impdirp1 28577 | A deduction unionizing a non-unionized collection of virtual hypotheses. 3impdir 1240 is ~? uun3132 and is in set.mm. 3impdirp1 28577 is ~? uun3132p1. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | 3impcombi 28578 | A 1-hypothesis propositional calculus deduction (Contributed by Alan Sare, 25-Sep-2017.) |
Theorem | 3imp231 28579 | Importation inference. (Contributed by Alan Sare, 17-Oct-2017.) |
Theorem | trsspwALT 28580 | Virtual deduction proof of the left-to-right implication of dftr4 4262. A transitive class is a subset of its power class. This proof corresponds to the virtual deduction proof of dftr4 4262 without accumulating results. (Contributed by Alan Sare, 29-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | trsspwALT2 28581 | Virtual deduction proof of trsspwALT 28580. This proof is the same as the proof of trsspwALT 28580 except each virtual deduction symbol is replaced by its non-virtual deduction symbol equivalent. A transitive class is a subset of its power class. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | trsspwALT3 28582 | Short predicate calculus proof of the left-to-right implication of dftr4 4262. A transitive class is a subset of its power class. This proof was constructed by applying Metamath's minimize command to the proof of trsspwALT2 28581, which is the virtual deduction proof trsspwALT 28580 without virtual deductions. (Contributed by Alan Sare, 30-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | sspwtr 28583 | Virtual deduction proof of the right-to-left implication of dftr4 4262. A class which is a subclass of its power class is transitive. This proof corresponds to the virtual deduction proof of sspwtr 28583 without accumulating results. (Contributed by Alan Sare, 2-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | sspwtrALT 28584 | Virtual deduction proof of sspwtr 28583. This proof is the same as the proof of sspwtr 28583 except each virtual deduction symbol is replaced by its non-virtual deduction symbol equivalent. A class which is a subclass of its power class is transitive. (Contributed by Alan Sare, 3-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | sspwtrALT2 28585 | Short predicate calculus proof of the right-to-left implication of dftr4 4262. A class which is a subclass of its power class is transitive. This proof was constructed by applying Metamath's minimize command to the proof of sspwtrALT 28584, which is the virtual deduction proof sspwtr 28583 without virtual deductions. (Contributed by Alan Sare, 3-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | pwtrVD 28586 | Virtual deduction proof of pwtr 4371. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | pwtrrVD 28587 | Virtual deduction proof of pwtr 4371. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | snssiALTVD 28588 | Virtual deduction proof of snssiALT 28589. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | snssiALT 28589 | If a class is an element of another class, then its singleton is a subclass of that other class. Alternate proof of snssi 3899. This theorem was automatically generated from snssiALTVD 28588 using a translation program. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | snsslVD 28590 | Virtual deduction proof of snssl 28591. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | snssl 28591 | If a singleton is a subclass of another class, then the singleton's element is an element of that other class. This theorem is the right-to-left implication of the biconditional snss 3883. The proof of this theorem was automatically generated from snsslVD 28590 using a tools command file, translateMWO.cmd , by translating the proof into its non-virtual deduction form and minimizing it. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | snelpwrVD 28592 | Virtual deduction proof of snelpwi 4364. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | unipwrVD 28593 | Virtual deduction proof of unipwr 28594. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | unipwr 28594 | A class is a subclass of the union of its power class. This theorem is the right-to-left subclass lemma of unipw 4369. The proof of this theorem was automatically generated from unipwrVD 28593 using a tools command file , translateMWO.cmd , by translating the proof into its non-virtual deduction form and minimizing it. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | sstrALT2VD 28595 | Virtual deduction proof of sstrALT2 28596. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | sstrALT2 28596 | Virtual deduction proof of sstr 3313, transitivity of subclasses, Theorem 6 of [Suppes] p. 23. This theorem was automatically generated from sstrALT2VD 28595 using the command file translate_{without}_overwriting.cmd . It was not minimized because the automated minimization excluding duplicates generates a minimized proof which, although not directly containing any duplicates, indirectly contains a duplicate. That is, the trace back of the minimized proof contains a duplicate. This is undesirable because some step(s) of the minimized proof use the proven theorem. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | suctrALT2VD 28597 | Virtual deduction proof of suctrALT2 28598. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | suctrALT2 28598 | Virtual deduction proof of suctr 4619. The sucessor of a transitive class is transitive. This proof was generated automatically from the virtual deduction proof suctrALT2VD 28597 using the tools command file translate_{without}_overwriting_{minimize}_excluding_{duplicates}.cmd . (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | elex2VD 28599* | Virtual deduction proof of elex2 2925. (Contributed by Alan Sare, 25-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | elex22VD 28600* | Virtual deduction proof of elex22 2924. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |