Theorem List for Metamath Proof Explorer - 39001-39100 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | eel0cT 39001 |
An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
|
|
Theorem | eelT0 39002 |
An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
|
|
Theorem | e0bi 39003 |
Elimination rule identical to mpbi 220. The non-virtual deduction form
is the virtual deduction form, which is mpbi 220.
(Contributed by Alan
Sare, 15-Jun-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
|
|
Theorem | e0bir 39004 |
Elimination rule identical to mpbir 221. The non-virtual deduction form
is the virtual deduction form, which is mpbir 221. (Contributed by Alan
Sare, 15-Jun-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
|
|
Theorem | uun0.1 39005 |
Convention notation form of un0.1 39006. (Contributed by Alan Sare,
23-Apr-2015.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
|
|
Theorem | un0.1 39006 |
is the constant
true, a tautology (see df-tru 1486). 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 39007 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
(Contributed by Alan Sare, 3-Dec-2015.) Proof was revised to accomodate
a possible future version of df-tru 1486. (Revised by David A. Wheeler,
8-May-2019.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
|
|
Theorem | uunT1p1 39008 |
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 39009 |
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 39010 |
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 39011 |
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 39012 |
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 39013 |
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 39014 |
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 862. (Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
|
|
Theorem | un10 39015 |
A unionizing deduction. (Contributed by Alan Sare, 28-Apr-2015.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
|
|
Theorem | un01 39016 |
A unionizing deduction. (Contributed by Alan Sare, 28-Apr-2015.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
|
|
Theorem | un2122 39017 |
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 39018 |
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 39019 |
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 39020 |
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 39021 |
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 39022 |
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 39023 |
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 39024 |
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 39025 |
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 39026 |
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 39027 |
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 39028 |
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 39029 |
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 39030 |
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 39031 |
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 39032 |
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 39033 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
3anidm12 1383 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 39034 |
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 39035 |
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 39036 |
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 39037 |
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 39038 |
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 39039 |
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 39040 |
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 39041 |
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 39042 |
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 39043 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
Commuted version of 3impdir 1382. (Contributed by Alan Sare,
4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
|
|
Theorem | 3impcombi 39044 |
A 1-hypothesis propositional calculus deduction. (Contributed by Alan
Sare, 25-Sep-2017.)
|
|
|
20.31.6 Theorems proved using Virtual
Deduction
|
|
Theorem | trsspwALT 39045 |
Virtual deduction proof of the left-to-right implication of dftr4 4757. A
transitive class is a subset of its power class. This proof corresponds
to the virtual deduction proof of dftr4 4757 without accumulating results.
(Contributed by Alan Sare, 29-Apr-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
|
|
Theorem | trsspwALT2 39046 |
Virtual deduction proof of trsspwALT 39045. This proof is the same as the
proof of trsspwALT 39045 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 39047 |
Short predicate calculus proof of the left-to-right implication of
dftr4 4757. 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 39046, which is the virtual deduction proof trsspwALT 39045
without virtual deductions. (Contributed by Alan Sare, 30-Apr-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
|
|
Theorem | sspwtr 39048 |
Virtual deduction proof of the right-to-left implication of dftr4 4757. A
class which is a subclass of its power class is transitive. This proof
corresponds to the virtual deduction proof of sspwtr 39048 without
accumulating results. (Contributed by Alan Sare, 2-May-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
|
|
Theorem | sspwtrALT 39049 |
Virtual deduction proof of sspwtr 39048. This proof is the same as the
proof of sspwtr 39048 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 | csbabgOLD 39050* |
Move substitution into a class abstraction. (Contributed by NM,
13-Dec-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) Obsolete
as of 19-Aug-2018. Use csbab 4008 instead. (New usage is discouraged.)
(Proof modification is discouraged.)
|
|
|
Theorem | csbunigOLD 39051 |
Distribute proper substitution through the union of a class.
(Contributed by Alan Sare, 10-Nov-2012.) Obsolete as of 22-Aug-2018.
Use csbuni 4466 instead. (New usage is discouraged.)
(Proof modification is discouraged.)
|
|
|
Theorem | csbfv12gALTOLD 39052 |
Move class substitution in and out of a function value. The proof is
derived from the virtual deduction proof csbfv12gALTVD 39135. (Contributed
by Alan Sare, 10-Nov-2012.) Obsolete as of 20-Aug-2018. Use csbfv12 6231
instead. (Proof modification is discouraged.)
(New usage is discouraged.)
|
|
|
Theorem | csbxpgOLD 39053 |
Distribute proper substitution through the Cartesian product of two
classes. (Contributed by Alan Sare, 10-Nov-2012.) Obsolete as of
23-Aug-2018. Use csbrn 5596 instead. (New usage is discouraged.)
(Proof modification is discouraged.)
|
|
|
Theorem | csbingOLD 39054 |
Distribute proper substitution through an intersection relation.
(Contributed by Alan Sare, 22-Jul-2012.) Obsolete as of 18-Aug-2018.
Use csbin 4010 instead. (New usage is discouraged.)
(Proof modification is discouraged.)
|
|
|
Theorem | csbresgOLD 39055 |
Distribute proper substitution through the restriction of a class.
csbresgOLD 39055 is derived from the virtual deduction proof
csbresgVD 39131.
(Contributed by Alan Sare, 10-Nov-2012.) Obsolete as of 23-Aug-2018. Use
csbres 5399 instead. (New usage is discouraged.)
(Proof modification is discouraged.)
|
|
|
Theorem | csbrngOLD 39056 |
Distribute proper substitution through the range of a class.
(Contributed by Alan Sare, 10-Nov-2012.) Obsolete as of 23-Aug-2018.
Use csbrn 5596 instead. (New usage is discouraged.)
(Proof modification is discouraged.)
|
|
|
Theorem | csbima12gALTOLD 39057 |
Move class substitution in and out of the image of a function. The proof
is derived from the virtual deduction proof csbima12gALTVD 39133.
(Contributed by Alan Sare, 10-Nov-2012.) Obsolete as of 20-Aug-2018. Use
csbfv12 6231 instead. (Proof modification is
discouraged.) (Proof
modification is discouraged.) (New usage is discouraged.)
|
|
|
Theorem | sspwtrALT2 39058 |
Short predicate calculus proof of the right-to-left implication of
dftr4 4757. 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 39049, which is the virtual deduction proof sspwtr 39048
without virtual deductions. (Contributed by Alan Sare, 3-May-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
|
|
Theorem | pwtrVD 39059 |
Virtual deduction proof of pwtr 4921; see pwtrrVD 39060 for the converse.
(Contributed by Alan Sare, 25-Aug-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
|
|
Theorem | pwtrrVD 39060 |
Virtual deduction proof of pwtr 4921; see pwtrVD 39059 for the converse.
(Contributed by Alan Sare, 25-Aug-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
|
|
Theorem | suctrALT 39061 |
The successor of a transitive class is transitive. The proof of
http://us.metamath.org/other/completeusersproof/suctrvd.html
is a
Virtual Deduction proof verified by automatically transforming it into
the Metamath proof of suctrALT 39061 using completeusersproof, which is
verified by the Metamath program. The proof of
http://us.metamath.org/other/completeusersproof/suctrro.html
is a form
of the completed proof which preserves the Virtual Deduction proof's
step numbers and their ordering. See suctr 5808 for the original proof.
(Contributed by Alan Sare, 11-Apr-2009.) (Revised by Alan Sare,
12-Jun-2018.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
|
|
Theorem | snssiALTVD 39062 |
Virtual deduction proof of snssiALT 39063. (Contributed by Alan Sare,
11-Sep-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
|
|
Theorem | snssiALT 39063 |
If a class is an element of another class, then its singleton is a
subclass of that other class. Alternate proof of snssi 4339. This
theorem was automatically generated from snssiALTVD 39062 using a
translation program. (Contributed by Alan Sare, 11-Sep-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
|
|
Theorem | snsslVD 39064 |
Virtual deduction proof of snssl 39065. (Contributed by Alan Sare,
25-Aug-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
|
|
Theorem | snssl 39065 |
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 4316.
The proof of
this theorem was automatically generated from snsslVD 39064 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 39066 |
Virtual deduction proof of snelpwi 4912. (Contributed by Alan Sare,
25-Aug-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
|
|
Theorem | unipwrVD 39067 |
Virtual deduction proof of unipwr 39068. (Contributed by Alan Sare,
25-Aug-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
|
|
Theorem | unipwr 39068 |
A class is a subclass of the union of its power class. This theorem is
the right-to-left subclass lemma of unipw 4918. The proof of this theorem
was automatically generated from unipwrVD 39067 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 39069 |
Virtual deduction proof of sstrALT2 39070. (Contributed by Alan Sare,
11-Sep-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
|
|
Theorem | sstrALT2 39070 |
Virtual deduction proof of sstr 3611, transitivity of subclasses, Theorem
6 of [Suppes] p. 23. This theorem was
automatically generated from
sstrALT2VD 39069 using the command file translatewithout_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 39071 |
Virtual deduction proof of suctrALT2 39072. (Contributed by Alan Sare,
11-Sep-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
|
|
Theorem | suctrALT2 39072 |
Virtual deduction proof of suctr 5808. The sucessor of a transitive class
is transitive. This proof was generated automatically from the virtual
deduction proof suctrALT2VD 39071 using the tools command file
translatewithout_overwritingminimize_excludingduplicates.cmd .
(Contributed by Alan Sare, 11-Sep-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
|
|
Theorem | elex2VD 39073* |
Virtual deduction proof of elex2 3216. (Contributed by Alan Sare,
25-Sep-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
|
|
Theorem | elex22VD 39074* |
Virtual deduction proof of elex22 3217. (Contributed by Alan Sare,
24-Oct-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
|
|
Theorem | eqsbc3rVD 39075* |
Virtual deduction proof of eqsbc3r 3492. (Contributed by Alan Sare,
24-Oct-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
|
|
Theorem | zfregs2VD 39076* |
Virtual deduction proof of zfregs2 8609. (Contributed by Alan Sare,
24-Oct-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
|
|
Theorem | tpid3gVD 39077 |
Virtual deduction proof of tpid3g 4305. (Contributed by Alan Sare,
24-Oct-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
|
|
Theorem | en3lplem1VD 39078* |
Virtual deduction proof of en3lplem1 8511. (Contributed by Alan Sare,
24-Oct-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
|
|
Theorem | en3lplem2VD 39079* |
Virtual deduction proof of en3lplem2 8512. (Contributed by Alan Sare,
24-Oct-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
|
|
Theorem | en3lpVD 39080 |
Virtual deduction proof of en3lp 8513. (Contributed by Alan Sare,
24-Oct-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
|
|
20.31.7 Theorems proved using Virtual Deduction
with mmj2 assistance
|
|
Theorem | simplbi2VD 39081 |
Virtual deduction proof of simplbi2 655. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
h1:: |
| 3:1,?: e0a 38999 |
| qed:3,?: e0a 38999 |
|
The proof of simplbi2 655 was automatically derived from it.
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
|
|
Theorem | 3ornot23VD 39082 |
Virtual deduction proof of 3ornot23 38715. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
1::
| 2:: |
| 3:1,?: e1a 38852 |
| 4:1,?: e1a 38852 |
| 5:3,4,?: e11 38913 |
| 6:2,?: e2 38856 |
| 7:5,6,?: e12 38951 |
| 8:7: |
| qed:8: |
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
|
|
Theorem | orbi1rVD 39083 |
Virtual deduction proof of orbi1r 38716. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
1:: |
| 2:: |
| 3:2,?: e2 38856 |
| 4:1,3,?: e12 38951 |
| 5:4,?: e2 38856 |
| 6:5: |
| 7:: |
| 8:7,?: e2 38856 |
| 9:1,8,?: e12 38951 |
| 10:9,?: e2 38856 |
| 11:10: |
| 12:6,11,?: e11 38913 |
| qed:12: |
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
|
|
Theorem | bitr3VD 39084 |
Virtual deduction proof of bitr3 342. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
1:: |
| 2:1,?: e1a 38852 |
| 3:: |
| 4:3,?: e2 38856 |
| 5:2,4,?: e12 38951 |
| 6:5: |
| qed:6: |
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
|
|
Theorem | 3orbi123VD 39085 |
Virtual deduction proof of 3orbi123 38717. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
1:: |
| 2:1,?: e1a 38852 |
| 3:1,?: e1a 38852 |
| 4:1,?: e1a 38852 |
| 5:2,3,?: e11 38913 |
| 6:5,4,?: e11 38913 |
| 7:?: |
| 8:6,7,?: e10 38919 |
| 9:?: |
| 10:8,9,?: e10 38919 |
| qed:10: |
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
|
|
Theorem | sbc3orgVD 39086 |
Virtual deduction proof of sbc3orgOLD 38742. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
1:: |
| 2:1,?: e1a 38852 |
| 3:: |
| 32:3: |
| 33:1,32,?: e10 38919 |
| 4:1,33,?: e11 38913 |
| 5:2,4,?: e11 38913 |
| 6:1,?: e1a 38852 |
| 7:6,?: e1a 38852 |
| 8:5,7,?: e11 38913 |
| 9:?: |
| 10:8,9,?: e10 38919 |
| qed:10: |
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
|
|
Theorem | 19.21a3con13vVD 39087* |
Virtual deduction proof of alrim3con13v 38743. The following user's
proof is completed by invoking mmj2's unify command and using mmj2's
StepSelector to pick all remaining steps of the Metamath proof.
1:: |
| 2:: |
| 3:2,?: e2 38856 |
| 4:2,?: e2 38856 |
| 5:2,?: e2 38856 |
| 6:1,4,?: e12 38951 |
| 7:3,?: e2 38856 |
| 8:5,?: e2 38856 |
| 9:7,6,8,?: e222 38861 |
| 10:9,?: e2 38856 |
| 11:10:in2 |
| qed:11:in1 |
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
|
|
Theorem | exbirVD 39088 |
Virtual deduction proof of exbir 38684. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
1:: |
| 2:: |
| 3:: |
| 5:1,2,?: e12 38951 |
| 6:3,5,?: e32 38985 |
| 7:6: |
| 8:7: |
| 9:8,?: e1a 38852 |
| qed:9: |
|
(Contributed by Alan Sare, 13-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
|
|
Theorem | exbiriVD 39089 |
Virtual deduction proof of exbiri 652. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
h1:: |
| 2:: |
| 3:: |
| 4:: |
| 5:2,1,?: e10 38919 |
| 6:3,5,?: e21 38957 |
| 7:4,6,?: e32 38985 |
| 8:7: |
| 9:8: |
| qed:9: |
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
|
|
Theorem | rspsbc2VD 39090* |
Virtual deduction proof of rspsbc2 38744. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
1:: |
| 2:: |
| 3:: |
| 4:1,3,?: e13 38975 |
| 5:1,4,?: e13 38975 |
| 6:2,5,?: e23 38982 |
| 7:6: |
| 8:7: |
| qed:8: |
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
|
|
Theorem | 3impexpVD 39091 |
Virtual deduction proof of 3impexp 1289. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
1:: |
| 2:: |
| 3:1,2,?: e10 38919 |
| 4:3,?: e1a 38852 |
| 5:4,?: e1a 38852 |
| 6:5: |
| 7:: |
| 8:7,?: e1a 38852 |
| 9:8,?: e1a 38852 |
| 10:2,9,?: e01 38916 |
| 11:10: |
| qed:6,11,?: e00 38995 |
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
|
|
Theorem | 3impexpbicomVD 39092 |
Virtual deduction proof of 3impexpbicom 38685. The following user's proof
is completed by invoking mmj2's unify command and using mmj2's
StepSelector to pick all remaining steps of the Metamath proof.
1:: |
| 2:: |
| 3:1,2,?: e10 38919 |
| 4:3,?: e1a 38852 |
| 5:4: |
| 6:: |
| 7:6,?: e1a 38852 |
| 8:7,2,?: e10 38919 |
| 9:8: |
| qed:5,9,?: e00 38995 |
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
|
|
Theorem | 3impexpbicomiVD 39093 |
Virtual deduction proof of 3impexpbicomi 38686. The following user's proof
is completed by invoking mmj2's unify command and using mmj2's
StepSelector to pick all remaining steps of the Metamath proof.
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
|
|
Theorem | sbcel1gvOLD 39094* |
Class substitution into a membership relation. (Contributed by NM,
17-Nov-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
Obsolete as of 17-Aug-2018. Use sbcel1v 3495 instead.
(New usage is discouraged.) (Proof modification is discouraged.)
|
|
|
Theorem | sbcoreleleqVD 39095* |
Virtual deduction proof of sbcoreleleq 38745. The following user's proof
is completed by invoking mmj2's unify command and using mmj2's
StepSelector to pick all remaining steps of the Metamath proof.
1:: |
| 2:1,?: e1a 38852 |
| 3:1,?: e1a 38852 |
| 4:1,?: e1a 38852 |
| 5:2,3,4,?: e111 38899 |
| 6:1,?: e1a 38852 |
| 7:5,6: e11 38913 |
| qed:7: |
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
|
|
Theorem | hbra2VD 39096* |
Virtual deduction proof of nfra2 2946. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's
StepSelector to pick all remaining steps of the Metamath proof.
1:: |
| 2:: |
| 3:1,2,?: e00 38995 |
| 4:2: |
| 5:4,?: e0a 38999 |
| qed:3,5,?: e00 38995 |
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
|
|
Theorem | tratrbVD 39097* |
Virtual deduction proof of tratrb 38746. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
1:: |
| 2:1,?: e1a 38852 |
| 3:1,?: e1a 38852 |
| 4:1,?: e1a 38852 |
| 5:: |
| 6:5,?: e2 38856 |
| 7:5,?: e2 38856 |
| 8:2,7,4,?: e121 38881 |
| 9:2,6,8,?: e122 38878 |
| 10:: |
| 11:6,7,10,?: e223 38860 |
| 12:11: |
| 13:: |
| 14:12,13,?: e20 38954 |
| 15:: |
| 16:7,15,?: e23 38982 |
| 17:6,16,?: e23 38982 |
| 18:17: |
| 19:: |
| 20:18,19,?: e20 38954 |
| 21:3,?: e1a 38852 |
| 22:21,9,4,?: e121 38881 |
| 23:22,?: e2 38856 |
| 24:4,23,?: e12 38951 |
| 25:14,20,24,?: e222 38861 |
| 26:25: |
| 27:: |
| 28:27,?: e0a 38999 |
| 29:28,26: |
| 30:: |
| 31:30,?: e0a 38999 |
| 32:31,29: |
| 33:32,?: e1a 38852 |
| qed:33: |
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
|
|
Theorem | al2imVD 39098 |
Virtual deduction proof of al2im 1742. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
1:: |
| 2:1,?: e1a 38852 |
| 3:: |
| 4:2,3,?: e10 38919 |
| qed:4: |
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
|
|
Theorem | syl5impVD 39099 |
Virtual deduction proof of syl5imp 38718. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
1:: |
| 2:1,?: e1a 38852 |
| 3:: |
| 4:3,2,?: e21 38957 |
| 5:4,?: e2 38856 |
| 6:5: |
| qed:6: |
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
|
|
Theorem | idiVD 39100 |
Virtual deduction proof of idiALT 38683. The following user's
proof is completed by invoking mmj2's unify command and using mmj2's
StepSelector to pick all remaining steps of the Metamath proof.
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
|