Theorem List for Metamath Proof Explorer - 41101-41200 *Has distinct variable
group(s)
| Type | Label | Description |
|---|
| Statement |
|---|
| |
| Theorem | eel0cT 41101 |
An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ 𝜑 & ⊢ (𝜑 → 𝜓) ⇒ ⊢ (⊤ → 𝜓) |
| |
| Theorem | eelT0 41102 |
An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ (⊤
→ 𝜑) & ⊢ 𝜓 & ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ 𝜒 |
| |
| Theorem | e0bi 41103 |
Elimination rule identical to mpbi 232. The non-virtual deduction form
is the virtual deduction form, which is mpbi 232.
(Contributed by Alan
Sare, 15-Jun-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
| ⊢ 𝜑 & ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ 𝜓 |
| |
| Theorem | e0bir 41104 |
Elimination rule identical to mpbir 233. The non-virtual deduction form
is the virtual deduction form, which is mpbir 233. (Contributed by Alan
Sare, 15-Jun-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
| ⊢ 𝜑 & ⊢ (𝜓 ↔ 𝜑) ⇒ ⊢ 𝜓 |
| |
| Theorem | uun0.1 41105 |
Convention notation form of un0.1 41106. (Contributed by Alan Sare,
23-Apr-2015.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
| ⊢ (⊤
→ 𝜑) & ⊢ (𝜓 → 𝜒)
& ⊢ ((⊤ ∧ 𝜓) → 𝜃) ⇒ ⊢ (𝜓 → 𝜃) |
| |
| Theorem | un0.1 41106 |
⊤ is the constant true, a tautology (see df-tru 1536). 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 41107 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
(Contributed by Alan Sare, 3-Dec-2015.) Proof was revised to
accommodate a possible future version of df-tru 1536. (Revised by David
A. Wheeler, 8-May-2019.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
| ⊢ ((⊤
∧ 𝜑) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) |
| |
| Theorem | uunT1p1 41108 |
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 41109 |
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 41110 |
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 41111 |
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 41112 |
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 41113 |
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 41114 |
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 671. (Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ (((𝜓 ∧ 𝜑) ∧ 𝜑) → 𝜒) ⇒ ⊢ ((𝜓 ∧ 𝜑) → 𝜒) |
| |
| Theorem | un10 41115 |
A unionizing deduction. (Contributed by Alan Sare, 28-Apr-2015.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ ( ( 𝜑 , ⊤ ) ▶ 𝜓 )
⇒ ⊢ ( 𝜑 ▶ 𝜓 ) |
| |
| Theorem | un01 41116 |
A unionizing deduction. (Contributed by Alan Sare, 28-Apr-2015.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ ( ( ⊤ , 𝜑 ) ▶ 𝜓 )
⇒ ⊢ ( 𝜑 ▶ 𝜓 ) |
| |
| Theorem | un2122 41117 |
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 41118 |
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 41119 |
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 41120 |
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 41121 |
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 41122 |
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 41123 |
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 41124 |
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 41125 |
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 41126 |
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 41127 |
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 41128 |
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 41129 |
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 41130 |
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 41131 |
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 41132 |
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 41133 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
3anidm12 1415 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 41134 |
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 41135 |
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 41136 |
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 41137 |
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 41138 |
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 41139 |
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 41140 |
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 41141 |
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 41142 |
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 41143 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
Commuted version of 3impdir 1347. (Contributed by Alan Sare,
4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ (((𝜒 ∧ 𝜓) ∧ (𝜑 ∧ 𝜓)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃) |
| |
| Theorem | 3impcombi 41144 |
A 1-hypothesis propositional calculus deduction. (Contributed by Alan
Sare, 25-Sep-2017.)
|
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜑) → (𝜒 ↔ 𝜃)) ⇒ ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃) |
| |
| 20.36.6 Theorems proved using Virtual
Deduction
|
| |
| Theorem | trsspwALT 41145 |
Virtual deduction proof of the left-to-right implication of dftr4 5169. A
transitive class is a subset of its power class. This proof corresponds
to the virtual deduction proof of dftr4 5169 without accumulating results.
(Contributed by Alan Sare, 29-Apr-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ (Tr 𝐴 → 𝐴 ⊆ 𝒫 𝐴) |
| |
| Theorem | trsspwALT2 41146 |
Virtual deduction proof of trsspwALT 41145. This proof is the same as the
proof of trsspwALT 41145 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.)
|
| ⊢ (Tr 𝐴 → 𝐴 ⊆ 𝒫 𝐴) |
| |
| Theorem | trsspwALT3 41147 |
Short predicate calculus proof of the left-to-right implication of
dftr4 5169. 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 41146, which is the virtual deduction proof trsspwALT 41145
without virtual deductions. (Contributed by Alan Sare, 30-Apr-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ (Tr 𝐴 → 𝐴 ⊆ 𝒫 𝐴) |
| |
| Theorem | sspwtr 41148 |
Virtual deduction proof of the right-to-left implication of dftr4 5169. A
class which is a subclass of its power class is transitive. This proof
corresponds to the virtual deduction proof of sspwtr 41148 without
accumulating results. (Contributed by Alan Sare, 2-May-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ (𝐴 ⊆ 𝒫 𝐴 → Tr 𝐴) |
| |
| Theorem | sspwtrALT 41149 |
Virtual deduction proof of sspwtr 41148. This proof is the same as the
proof of sspwtr 41148 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.)
|
| ⊢ (𝐴 ⊆ 𝒫 𝐴 → Tr 𝐴) |
| |
| Theorem | sspwtrALT2 41150 |
Short predicate calculus proof of the right-to-left implication of
dftr4 5169. 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 41149, which is the virtual deduction proof sspwtr 41148
without virtual deductions. (Contributed by Alan Sare, 3-May-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ (𝐴 ⊆ 𝒫 𝐴 → Tr 𝐴) |
| |
| Theorem | pwtrVD 41151 |
Virtual deduction proof of pwtr 5337; see pwtrrVD 41152 for the converse.
(Contributed by Alan Sare, 25-Aug-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ (Tr 𝐴 → Tr 𝒫 𝐴) |
| |
| Theorem | pwtrrVD 41152 |
Virtual deduction proof of pwtr 5337; see pwtrVD 41151 for the converse.
(Contributed by Alan Sare, 25-Aug-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ 𝐴 ∈
V ⇒ ⊢ (Tr 𝒫 𝐴 → Tr 𝐴) |
| |
| Theorem | suctrALT 41153 |
The successor of a transitive class is transitive. The proof of
https://us.metamath.org/other/completeusersproof/suctrvd.html
is a
Virtual Deduction proof verified by automatically transforming it into
the Metamath proof of suctrALT 41153 using completeusersproof, which is
verified by the Metamath program. The proof of
https://us.metamath.org/other/completeusersproof/suctrro.html 41153 is a
form of the completed proof which preserves the Virtual Deduction
proof's step numbers and their ordering. See suctr 6268 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.)
|
| ⊢ (Tr 𝐴 → Tr suc 𝐴) |
| |
| Theorem | snssiALTVD 41154 |
Virtual deduction proof of snssiALT 41155. (Contributed by Alan Sare,
11-Sep-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
| ⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵) |
| |
| Theorem | snssiALT 41155 |
If a class is an element of another class, then its singleton is a
subclass of that other class. Alternate proof of snssi 4734. This
theorem was automatically generated from snssiALTVD 41154 using a
translation program. (Contributed by Alan Sare, 11-Sep-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵) |
| |
| Theorem | snsslVD 41156 |
Virtual deduction proof of snssl 41157. (Contributed by Alan Sare,
25-Aug-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
| ⊢ 𝐴 ∈
V ⇒ ⊢ ({𝐴} ⊆ 𝐵 → 𝐴 ∈ 𝐵) |
| |
| Theorem | snssl 41157 |
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 4711.
The proof of
this theorem was automatically generated from snsslVD 41156 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.)
|
| ⊢ 𝐴 ∈
V ⇒ ⊢ ({𝐴} ⊆ 𝐵 → 𝐴 ∈ 𝐵) |
| |
| Theorem | snelpwrVD 41158 |
Virtual deduction proof of snelpwi 5328. (Contributed by Alan Sare,
25-Aug-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
| ⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ 𝒫 𝐵) |
| |
| Theorem | unipwrVD 41159 |
Virtual deduction proof of unipwr 41160. (Contributed by Alan Sare,
25-Aug-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
| ⊢ 𝐴 ⊆ ∪ 𝒫 𝐴 |
| |
| Theorem | unipwr 41160 |
A class is a subclass of the union of its power class. This theorem is
the right-to-left subclass lemma of unipw 5334. The proof of this theorem
was automatically generated from unipwrVD 41159 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 41161 |
Virtual deduction proof of sstrALT2 41162. (Contributed by Alan Sare,
11-Sep-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
| ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶) |
| |
| Theorem | sstrALT2 41162 |
Virtual deduction proof of sstr 3974, transitivity of subclasses, Theorem
6 of [Suppes] p. 23. This theorem was
automatically generated from
sstrALT2VD 41161 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 41163 |
Virtual deduction proof of suctrALT2 41164. (Contributed by Alan Sare,
11-Sep-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
| ⊢ (Tr 𝐴 → Tr suc 𝐴) |
| |
| Theorem | suctrALT2 41164 |
Virtual deduction proof of suctr 6268. The sucessor of a transitive class
is transitive. This proof was generated automatically from the virtual
deduction proof suctrALT2VD 41163 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.)
|
| ⊢ (Tr 𝐴 → Tr suc 𝐴) |
| |
| Theorem | elex2VD 41165* |
Virtual deduction proof of elex2 3516. (Contributed by Alan Sare,
25-Sep-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
| ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 ∈ 𝐵) |
| |
| Theorem | elex22VD 41166* |
Virtual deduction proof of elex22 3517. (Contributed by Alan Sare,
24-Oct-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
| ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)) |
| |
| Theorem | eqsbc3rVD 41167* |
Virtual deduction proof of eqsbc3r 3836. (Contributed by Alan Sare,
24-Oct-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
| ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]𝐶 = 𝑥 ↔ 𝐶 = 𝐴)) |
| |
| Theorem | zfregs2VD 41168* |
Virtual deduction proof of zfregs2 9169. (Contributed by Alan Sare,
24-Oct-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
| ⊢ (𝐴 ≠ ∅ → ¬
∀𝑥 ∈ 𝐴 ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥)) |
| |
| Theorem | tpid3gVD 41169 |
Virtual deduction proof of tpid3g 4701. (Contributed by Alan Sare,
24-Oct-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
| ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ {𝐶, 𝐷, 𝐴}) |
| |
| Theorem | en3lplem1VD 41170* |
Virtual deduction proof of en3lplem1 9069. (Contributed by Alan Sare,
24-Oct-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
| ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → (𝑥 = 𝐴 → ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥))) |
| |
| Theorem | en3lplem2VD 41171* |
Virtual deduction proof of en3lplem2 9070. (Contributed by Alan Sare,
24-Oct-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
| ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → (𝑥 ∈ {𝐴, 𝐵, 𝐶} → ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥))) |
| |
| Theorem | en3lpVD 41172 |
Virtual deduction proof of en3lp 9071. (Contributed by Alan Sare,
24-Oct-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
| ⊢ ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) |
| |
| 20.36.7 Theorems proved using Virtual Deduction
with mmj2 assistance
|
| |
| Theorem | simplbi2VD 41173 |
Virtual deduction proof of simplbi2 503. 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 41099 | ⊢ ((𝜓 ∧ 𝜒) → 𝜑)
| | qed:3,?: e0a 41099 | ⊢ (𝜓 → (𝜒 → 𝜑))
|
The proof of simplbi2 503 was automatically derived from it.
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
| ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜓 → (𝜒 → 𝜑)) |
| |
| Theorem | 3ornot23VD 41174 |
Virtual deduction proof of 3ornot23 40836. 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 40954 | ⊢ ( (¬ 𝜑 ∧ ¬ 𝜓) ▶ ¬ 𝜑 )
| | 4:1,?: e1a 40954 | ⊢ ( (¬ 𝜑 ∧ ¬ 𝜓) ▶ ¬ 𝜓 )
| | 5:3,4,?: e11 41015 | ⊢ ( (¬ 𝜑 ∧ ¬ 𝜓) ▶ ¬ (𝜑
∨ 𝜓) )
| | 6:2,?: e2 40958 | ⊢ ( (¬ 𝜑 ∧ ¬ 𝜓) , (𝜒 ∨ 𝜑
∨ 𝜓) ▶ (𝜒 ∨ (𝜑 ∨ 𝜓)) )
| | 7:5,6,?: e12 41051 | ⊢ ( (¬ 𝜑 ∧ ¬ 𝜓) , (𝜒 ∨ 𝜑
∨ 𝜓) ▶ 𝜒 )
| | 8:7: | ⊢ ( (¬ 𝜑 ∧ ¬ 𝜓) ▶ ((𝜒
∨ 𝜑 ∨ 𝜓) → 𝜒) )
| | qed:8: | ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ((𝜒
∨ 𝜑 ∨ 𝜓) → 𝜒))
|
(Contributed by Alan Sare, 31-Dec-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ((𝜒 ∨ 𝜑 ∨ 𝜓) → 𝜒)) |
| |
| Theorem | orbi1rVD 41175 |
Virtual deduction proof of orbi1r 40837. 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 40958 | ⊢ ( (𝜑 ↔ 𝜓) , (𝜒 ∨ 𝜑)
▶ (𝜑 ∨ 𝜒) )
| | 4:1,3,?: e12 41051 | ⊢ ( (𝜑 ↔ 𝜓) , (𝜒 ∨ 𝜑)
▶ (𝜓 ∨ 𝜒) )
| | 5:4,?: e2 40958 | ⊢ ( (𝜑 ↔ 𝜓) , (𝜒 ∨ 𝜑)
▶ (𝜒 ∨ 𝜓) )
| | 6:5: | ⊢ ( (𝜑 ↔ 𝜓) ▶ ((𝜒 ∨ 𝜑)
→ (𝜒 ∨ 𝜓)) )
| | 7:: | ⊢ ( (𝜑 ↔ 𝜓) , (𝜒 ∨ 𝜓)
▶ (𝜒 ∨ 𝜓) )
| | 8:7,?: e2 40958 | ⊢ ( (𝜑 ↔ 𝜓) , (𝜒 ∨ 𝜓)
▶ (𝜓 ∨ 𝜒) )
| | 9:1,8,?: e12 41051 | ⊢ ( (𝜑 ↔ 𝜓) , (𝜒 ∨ 𝜓)
▶ (𝜑 ∨ 𝜒) )
| | 10:9,?: e2 40958 | ⊢ ( (𝜑 ↔ 𝜓) , (𝜒 ∨ 𝜓)
▶ (𝜒 ∨ 𝜑) )
| | 11:10: | ⊢ ( (𝜑 ↔ 𝜓) ▶ ((𝜒 ∨ 𝜓)
→ (𝜒 ∨ 𝜑)) )
| | 12:6,11,?: e11 41015 | ⊢ ( (𝜑 ↔ 𝜓) ▶ ((𝜒
∨ 𝜑) ↔ (𝜒 ∨ 𝜓)) )
| | qed:12: | ⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ∨ 𝜑)
↔ (𝜒 ∨ 𝜓)))
|
(Contributed by Alan Sare, 31-Dec-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓))) |
| |
| Theorem | bitr3VD 41176 |
Virtual deduction proof of bitr3 355. 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 40954 | ⊢ ( (𝜑 ↔ 𝜓) ▶ (𝜓
↔ 𝜑) )
| | 3:: | ⊢ ( (𝜑 ↔ 𝜓) , (𝜑 ↔ 𝜒)
▶ (𝜑 ↔ 𝜒) )
| | 4:3,?: e2 40958 | ⊢ ( (𝜑 ↔ 𝜓) , (𝜑 ↔ 𝜒)
▶ (𝜒 ↔ 𝜑) )
| | 5:2,4,?: e12 41051 | ⊢ ( (𝜑 ↔ 𝜓) , (𝜑 ↔ 𝜒)
▶ (𝜓 ↔ 𝜒) )
| | 6:5: | ⊢ ( (𝜑 ↔ 𝜓) ▶ ((𝜑
↔ 𝜒) → (𝜓 ↔ 𝜒)) )
| | qed:6: | ⊢ ((𝜑 ↔ 𝜓) → ((𝜑 ↔ 𝜒)
→ (𝜓 ↔ 𝜒)))
|
(Contributed by Alan Sare, 31-Dec-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ ((𝜑 ↔ 𝜓) → ((𝜑 ↔ 𝜒) → (𝜓 ↔ 𝜒))) |
| |
| Theorem | 3orbi123VD 41177 |
Virtual deduction proof of 3orbi123 40838. 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 40954 | ⊢ ( ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)
∧ (𝜏 ↔ 𝜂)) ▶ (𝜑 ↔ 𝜓) )
| | 3:1,?: e1a 40954 | ⊢ ( ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)
∧ (𝜏 ↔ 𝜂)) ▶ (𝜒 ↔ 𝜃) )
| | 4:1,?: e1a 40954 | ⊢ ( ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)
∧ (𝜏 ↔ 𝜂)) ▶ (𝜏 ↔ 𝜂) )
| | 5:2,3,?: e11 41015 | ⊢ ( ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)
∧ (𝜏 ↔ 𝜂)) ▶ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃)) )
| | 6:5,4,?: e11 41015 | ⊢ ( ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)
∧ (𝜏 ↔ 𝜂)) ▶ (((𝜑 ∨ 𝜒) ∨ 𝜏) ↔ ((𝜓 ∨ 𝜃)
∨ 𝜂)) )
| | 7:?: | ⊢ (((𝜑 ∨ 𝜒) ∨ 𝜏) ↔ (𝜑
∨ 𝜒 ∨ 𝜏))
| | 8:6,7,?: e10 41021 | ⊢ ( ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)
∧ (𝜏 ↔ 𝜂)) ▶ ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ ((𝜓 ∨ 𝜃)
∨ 𝜂)) )
| | 9:?: | ⊢ (((𝜓 ∨ 𝜃) ∨ 𝜂) ↔
(𝜓 ∨ 𝜃 ∨ 𝜂))
| | 10:8,9,?: e10 41021 | ⊢ ( ((𝜑 ↔ 𝜓) ∧ (𝜒
↔ 𝜃) ∧ (𝜏 ↔ 𝜂)) ▶ ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ (𝜓 ∨
𝜃 ∨ 𝜂)) )
| | qed:10: | ⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)
∧ (𝜏 ↔ 𝜂)) → ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ (𝜓 ∨ 𝜃
∨ 𝜂)))
|
(Contributed by Alan Sare, 31-Dec-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂)) → ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ (𝜓 ∨ 𝜃 ∨ 𝜂))) |
| |
| Theorem | sbc3orgVD 41178 |
Virtual deduction proof of the analogue of sbcor 3821 with three disjuncts.
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 40954 | ⊢ ( 𝐴 ∈ 𝐵 ▶ ([𝐴 / 𝑥]((𝜑
∨ 𝜓) ∨ 𝜒) ↔ ([𝐴 / 𝑥](𝜑 ∨ 𝜓)
∨ [𝐴 / 𝑥]𝜒)) )
| | 3:: | ⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑
∨ 𝜓 ∨ 𝜒))
| | 32:3: | ⊢ ∀𝑥(((𝜑 ∨ 𝜓) ∨ 𝜒)
↔ (𝜑 ∨ 𝜓 ∨ 𝜒))
| | 33:1,32,?: e10 41021 | ⊢ ( 𝐴 ∈ 𝐵 ▶ [𝐴 / 𝑥](((𝜑
∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ 𝜓 ∨ 𝜒)) )
| | 4:1,33,?: e11 41015 | ⊢ ( 𝐴 ∈ 𝐵 ▶ ([𝐴 / 𝑥]((𝜑
∨ 𝜓) ∨ 𝜒) ↔ [𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒)) )
| | 5:2,4,?: e11 41015 | ⊢ ( 𝐴 ∈ 𝐵 ▶ ([𝐴 / 𝑥](𝜑
∨ 𝜓 ∨ 𝜒) ↔ ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ∨ [𝐴 / 𝑥]𝜒)) )
| | 6:1,?: e1a 40954 | ⊢ ( 𝐴 ∈ 𝐵 ▶ ([𝐴 / 𝑥](𝜑
∨ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓)) )
| | 7:6,?: e1a 40954 | ⊢ ( 𝐴 ∈ 𝐵 ▶ (([𝐴 / 𝑥](𝜑
∨ 𝜓) ∨ [𝐴 / 𝑥]𝜒) ↔ (([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓)
∨ [𝐴 / 𝑥]𝜒)) )
| | 8:5,7,?: e11 41015 | ⊢ ( 𝐴 ∈ 𝐵 ▶ ([𝐴 / 𝑥](𝜑
∨ 𝜓 ∨ 𝜒) ↔ (([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓)
∨ [𝐴 / 𝑥]𝜒)) )
| | 9:?: | ⊢ ((([𝐴 / 𝑥]𝜑
∨ [𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒) ↔ ([𝐴 / 𝑥]𝜑
∨ [𝐴 / 𝑥]𝜓 ∨ [𝐴 / 𝑥]𝜒))
| | 10:8,9,?: e10 41021 | ⊢ ( 𝐴 ∈ 𝐵 ▶ ([𝐴 / 𝑥](𝜑
∨ 𝜓 ∨ 𝜒) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓
∨ [𝐴 / 𝑥]𝜒)) )
| | qed:10: | ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](𝜑
∨ 𝜓 ∨ 𝜒) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓
∨ [𝐴 / 𝑥]𝜒)))
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
| ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓 ∨ [𝐴 / 𝑥]𝜒))) |
| |
| Theorem | 19.21a3con13vVD 41179* |
Virtual deduction proof of alrim3con13v 40860. 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 40958 | ⊢ ( (𝜑 → ∀𝑥𝜑) , (𝜓
∧ 𝜑 ∧ 𝜒) ▶ 𝜓 )
| | 4:2,?: e2 40958 | ⊢ ( (𝜑 → ∀𝑥𝜑) , (𝜓
∧ 𝜑 ∧ 𝜒) ▶ 𝜑 )
| | 5:2,?: e2 40958 | ⊢ ( (𝜑 → ∀𝑥𝜑) , (𝜓
∧ 𝜑 ∧ 𝜒) ▶ 𝜒 )
| | 6:1,4,?: e12 41051 | ⊢ ( (𝜑 → ∀𝑥𝜑) , (𝜓
∧ 𝜑 ∧ 𝜒) ▶ ∀𝑥𝜑 )
| | 7:3,?: e2 40958 | ⊢ ( (𝜑 → ∀𝑥𝜑) , (𝜓
∧ 𝜑 ∧ 𝜒) ▶ ∀𝑥𝜓 )
| | 8:5,?: e2 40958 | ⊢ ( (𝜑 → ∀𝑥𝜑) , (𝜓
∧ 𝜑 ∧ 𝜒) ▶ ∀𝑥𝜒 )
| | 9:7,6,8,?: e222 40963 | ⊢ ( (𝜑 → ∀𝑥𝜑) , (𝜓
∧ 𝜑 ∧ 𝜒) ▶ (∀𝑥𝜓 ∧ ∀𝑥𝜑 ∧ ∀𝑥𝜒) )
| | 10:9,?: e2 40958 | ⊢ ( (𝜑 → ∀𝑥𝜑) , (𝜓
∧ 𝜑 ∧ 𝜒) ▶ ∀𝑥(𝜓 ∧ 𝜑 ∧ 𝜒) )
| | 11:10:in2 | ⊢ ( (𝜑 → ∀𝑥𝜑) ▶ ((𝜓
∧ 𝜑 ∧ 𝜒) → ∀𝑥(𝜓 ∧ 𝜑 ∧ 𝜒)) )
| | qed:11:in1 | ⊢ ((𝜑 → ∀𝑥𝜑) → ((𝜓
∧ 𝜑 ∧ 𝜒) → ∀𝑥(𝜓 ∧ 𝜑 ∧ 𝜒)))
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
| ⊢ ((𝜑 → ∀𝑥𝜑) → ((𝜓 ∧ 𝜑 ∧ 𝜒) → ∀𝑥(𝜓 ∧ 𝜑 ∧ 𝜒))) |
| |
| Theorem | exbirVD 41180 |
Virtual deduction proof of exbir 40805. 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 41051 | ⊢ ( ((𝜑 ∧ 𝜓) → (𝜒
↔ 𝜃)), (𝜑 ∧ 𝜓) ▶ (𝜒 ↔ 𝜃) )
| | 6:3,5,?: e32 41085 | ⊢ ( ((𝜑 ∧ 𝜓) → (𝜒
↔ 𝜃)), (𝜑 ∧ 𝜓), 𝜃 ▶ 𝜒 )
| | 7:6: | ⊢ ( ((𝜑 ∧ 𝜓) → (𝜒
↔ 𝜃)), (𝜑 ∧ 𝜓) ▶ (𝜃 → 𝜒) )
| | 8:7: | ⊢ ( ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))
▶ ((𝜑 ∧ 𝜓) → (𝜃 → 𝜒)) )
| | 9:8,?: e1a 40954 | ⊢ ( ((𝜑 ∧ 𝜓) → (𝜒
↔ 𝜃)) ▶ (𝜑 → (𝜓 → (𝜃 → 𝜒))) )
| | qed:9: | ⊢ (((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))
→ (𝜑 → (𝜓 → (𝜃 → 𝜒))))
|
(Contributed by Alan Sare, 13-Dec-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ (((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) → (𝜑 → (𝜓 → (𝜃 → 𝜒)))) |
| |
| Theorem | exbiriVD 41181 |
Virtual deduction proof of exbiri 809. 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 41021 | ⊢ ( 𝜑 ▶ (𝜓 → (𝜒 ↔ 𝜃)) )
| | 6:3,5,?: e21 41057 | ⊢ ( 𝜑 , 𝜓 ▶ (𝜒 ↔ 𝜃) )
| | 7:4,6,?: e32 41085 | ⊢ ( 𝜑 , 𝜓 , 𝜃 ▶ 𝜒 )
| | 8:7: | ⊢ ( 𝜑 , 𝜓 ▶ (𝜃 → 𝜒) )
| | 9:8: | ⊢ ( 𝜑 ▶ (𝜓 → (𝜃 → 𝜒)) )
| | qed:9: | ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒)))
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
| ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒))) |
| |
| Theorem | rspsbc2VD 41182* |
Virtual deduction proof of rspsbc2 40861. 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 41075 | ⊢ ( 𝐴 ∈ 𝐵 , 𝐶 ∈ 𝐷 , ∀𝑥 ∈ 𝐵
∀𝑦 ∈ 𝐷𝜑 ▶ [𝐴 / 𝑥]∀𝑦 ∈ 𝐷𝜑 )
| | 5:1,4,?: e13 41075 | ⊢ ( 𝐴 ∈ 𝐵 , 𝐶 ∈ 𝐷 , ∀𝑥 ∈ 𝐵
∀𝑦 ∈ 𝐷𝜑 ▶ ∀𝑦 ∈ 𝐷[𝐴 / 𝑥]𝜑 )
| | 6:2,5,?: e23 41082 | ⊢ ( 𝐴 ∈ 𝐵 , 𝐶 ∈ 𝐷 , ∀𝑥 ∈ 𝐵
∀𝑦 ∈ 𝐷𝜑 ▶ [𝐶 / 𝑦][𝐴 / 𝑥]𝜑 )
| | 7:6: | ⊢ ( 𝐴 ∈ 𝐵 , 𝐶 ∈ 𝐷 ▶ (∀𝑥 ∈ 𝐵
∀𝑦 ∈ 𝐷𝜑 → [𝐶 / 𝑦][𝐴 / 𝑥]𝜑) )
| | 8:7: | ⊢ ( 𝐴 ∈ 𝐵 ▶ (𝐶 ∈ 𝐷
→ (∀𝑥 ∈ 𝐵∀𝑦 ∈ 𝐷𝜑 → [𝐶 / 𝑦][𝐴 / 𝑥]𝜑)) )
| | qed:8: | ⊢ (𝐴 ∈ 𝐵 → (𝐶 ∈ 𝐷
→ (∀𝑥 ∈ 𝐵∀𝑦 ∈ 𝐷𝜑 → [𝐶 / 𝑦][𝐴 / 𝑥]𝜑)))
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
| ⊢ (𝐴 ∈ 𝐵 → (𝐶 ∈ 𝐷 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑 → [𝐶 / 𝑦][𝐴 / 𝑥]𝜑))) |
| |
| Theorem | 3impexpVD 41183 |
Virtual deduction proof of 3impexp 1354. 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 41021 | ⊢ ( ((𝜑 ∧ 𝜓 ∧ 𝜒)
→ 𝜃) ▶ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) )
| | 4:3,?: e1a 40954 | ⊢ ( ((𝜑 ∧ 𝜓 ∧ 𝜒)
→ 𝜃) ▶ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) )
| | 5:4,?: e1a 40954 | ⊢ ( ((𝜑 ∧ 𝜓 ∧ 𝜒)
→ 𝜃) ▶ (𝜑 → (𝜓 → (𝜒 → 𝜃))) )
| | 6:5: | ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
→ (𝜑 → (𝜓 → (𝜒 → 𝜃))))
| | 7:: | ⊢ ( (𝜑 → (𝜓 → (𝜒
→ 𝜃))) ▶ (𝜑 → (𝜓 → (𝜒 → 𝜃))) )
| | 8:7,?: e1a 40954 | ⊢ ( (𝜑 → (𝜓 → (𝜒
→ 𝜃))) ▶ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) )
| | 9:8,?: e1a 40954 | ⊢ ( (𝜑 → (𝜓 → (𝜒
→ 𝜃))) ▶ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) )
| | 10:2,9,?: e01 41018 | ⊢ ( (𝜑 → (𝜓 → (𝜒
→ 𝜃))) ▶ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) )
| | 11:10: | ⊢ ((𝜑 → (𝜓 → (𝜒
→ 𝜃))) → ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃))
| | qed:6,11,?: e00 41095 | ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒)
→ 𝜃) ↔ (𝜑 → (𝜓 → (𝜒 → 𝜃))))
|
(Contributed by Alan Sare, 31-Dec-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ↔ (𝜑 → (𝜓 → (𝜒 → 𝜃)))) |
| |
| Theorem | 3impexpbicomVD 41184 |
Virtual deduction proof of 3impexpbicom 40806. 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 41021 | ⊢ ( ((𝜑 ∧ 𝜓 ∧ 𝜒)
→ (𝜃 ↔ 𝜏)) ▶ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜏 ↔ 𝜃)) )
| | 4:3,?: e1a 40954 | ⊢ ( ((𝜑 ∧ 𝜓 ∧ 𝜒)
→ (𝜃 ↔ 𝜏)) ▶ (𝜑 → (𝜓 → (𝜒 → (𝜏
↔ 𝜃)))) )
| | 5:4: | ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒)
→ (𝜃 ↔ 𝜏)) → (𝜑 → (𝜓 → (𝜒 → (𝜏
↔ 𝜃)))))
| | 6:: | ⊢ ( (𝜑 → (𝜓 → (𝜒
→ (𝜏 ↔ 𝜃)))) ▶ (𝜑 → (𝜓 → (𝜒 → (𝜏
↔ 𝜃)))) )
| | 7:6,?: e1a 40954 | ⊢ ( (𝜑 → (𝜓 → (𝜒
→ (𝜏 ↔ 𝜃)))) ▶ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜏
↔ 𝜃)) )
| | 8:7,2,?: e10 41021 | ⊢ ( (𝜑 → (𝜓 → (𝜒
→ (𝜏 ↔ 𝜃)))) ▶ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃
↔ 𝜏)) )
| | 9:8: | ⊢ ((𝜑 → (𝜓 → (𝜒
→ (𝜏 ↔ 𝜃)))) → ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃
↔ 𝜏)))
| | qed:5,9,?: e00 41095 | ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒)
→ (𝜃 ↔ 𝜏)) ↔ (𝜑 → (𝜓 → (𝜒 → (𝜏
↔ 𝜃)))))
|
(Contributed by Alan Sare, 31-Dec-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)) ↔ (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃))))) |
| |
| Theorem | 3impexpbicomiVD 41185 |
Virtual deduction proof of 3impexpbicomi 40807. 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:: | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃
↔ 𝜏))
| | qed:1,?: e0a 41099 | ⊢ (𝜑 → (𝜓 → (𝜒
→ (𝜏 ↔ 𝜃))))
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃)))) |
| |
| Theorem | sbcoreleleqVD 41186* |
Virtual deduction proof of sbcoreleleq 40862. 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 40954 | ⊢ ( 𝐴 ∈ 𝐵 ▶ ([𝐴 / 𝑦]𝑥 ∈
𝑦 ↔ 𝑥 ∈ 𝐴) )
| | 3:1,?: e1a 40954 | ⊢ ( 𝐴 ∈ 𝐵 ▶ ([𝐴 / 𝑦]𝑦 ∈
𝑥 ↔ 𝐴 ∈ 𝑥) )
| | 4:1,?: e1a 40954 | ⊢ ( 𝐴 ∈ 𝐵 ▶ ([𝐴 / 𝑦]𝑥 =
𝑦 ↔ 𝑥 = 𝐴) )
| | 5:2,3,4,?: e111 41001 | ⊢ ( 𝐴 ∈ 𝐵 ▶ ((𝑥 ∈ 𝐴
∨ 𝐴 ∈ 𝑥 ∨ 𝑥 = 𝐴) ↔ ([𝐴 / 𝑦]𝑥 ∈ 𝑦 ∨ [𝐴 / 𝑦]𝑦 ∈ 𝑥
∨ [𝐴 / 𝑦]𝑥 = 𝑦)) )
| | 6:1,?: e1a 40954 | ⊢ ( 𝐴 ∈ 𝐵
▶ ([𝐴 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ↔ ([𝐴 / 𝑦]𝑥
∈ 𝑦 ∨ [𝐴 / 𝑦]𝑦 ∈ 𝑥 ∨ [𝐴 / 𝑦]𝑥 = 𝑦)) )
| | 7:5,6: e11 41015 | ⊢ ( 𝐴 ∈ 𝐵 ▶ ([𝐴 / 𝑦](𝑥
∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ↔ (𝑥 ∈ 𝐴 ∨ 𝐴 ∈ 𝑥 ∨ 𝑥 = 𝐴)) )
| | qed:7: | ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑦](𝑥 ∈ 𝑦
∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ↔ (𝑥 ∈ 𝐴 ∨ 𝐴 ∈ 𝑥 ∨ 𝑥 = 𝐴)))
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
| ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ↔ (𝑥 ∈ 𝐴 ∨ 𝐴 ∈ 𝑥 ∨ 𝑥 = 𝐴))) |
| |
| Theorem | hbra2VD 41187* |
Virtual deduction proof of nfra2 3228. 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 41095 | ⊢ (∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐵𝜑 →
∀𝑦∀𝑦 ∈ 𝐵∀𝑥 ∈ 𝐴𝜑)
| | 4:2: | ⊢ ∀𝑦(∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐵𝜑 ↔
∀𝑦 ∈ 𝐵∀𝑥 ∈ 𝐴𝜑)
| | 5:4,?: e0a 41099 | ⊢ (∀𝑦∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐵𝜑 ↔
∀𝑦∀𝑦 ∈ 𝐵∀𝑥 ∈ 𝐴𝜑)
| | qed:3,5,?: e00 41095 | ⊢ (∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐵𝜑 →
∀𝑦∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐵𝜑)
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
| ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → ∀𝑦∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑) |
| |
| Theorem | tratrbVD 41188* |
Virtual deduction proof of tratrb 40863. 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:: | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)
▶ (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)
∧ 𝐵 ∈ 𝐴) )
| | 2:1,?: e1a 40954 | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) ▶ Tr 𝐴 )
| | 3:1,?: e1a 40954 | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)
▶ ∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) )
| | 4:1,?: e1a 40954 | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) ▶ 𝐵 ∈ 𝐴 )
| | 5:: | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦
∧ 𝑦 ∈ 𝐵) ▶ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) )
| | 6:5,?: e2 40958 | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦
∧ 𝑦 ∈ 𝐵) ▶ 𝑥 ∈ 𝑦 )
| | 7:5,?: e2 40958 | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦
∧ 𝑦 ∈ 𝐵) ▶ 𝑦 ∈ 𝐵 )
| | 8:2,7,4,?: e121 40983 | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦
∧ 𝑦 ∈ 𝐵) ▶ 𝑦 ∈ 𝐴 )
| | 9:2,6,8,?: e122 40980 | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦
∧ 𝑦 ∈ 𝐵) ▶ 𝑥 ∈ 𝐴 )
| | 10:: | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦
∧ 𝑦 ∈ 𝐵), 𝐵 ∈ 𝑥 ▶ 𝐵 ∈ 𝑥 )
| | 11:6,7,10,?: e223 40962 | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦
∧ 𝑦 ∈ 𝐵), 𝐵 ∈ 𝑥 ▶ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ∧ 𝐵 ∈ 𝑥) )
| | 12:11: | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦
∧ 𝑦 ∈ 𝐵) ▶ (𝐵 ∈ 𝑥 → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ∧ 𝐵 ∈ 𝑥)) )
| | 13:: | ⊢ ¬ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵
∧ 𝐵 ∈ 𝑥)
| | 14:12,13,?: e20 41054 | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦
∧ 𝑦 ∈ 𝐵) ▶ ¬ 𝐵 ∈ 𝑥 )
| | 15:: | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦
∧ 𝑦 ∈ 𝐵), 𝑥 = 𝐵 ▶ 𝑥 = 𝐵 )
| | 16:7,15,?: e23 41082 | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦
∧ 𝑦 ∈ 𝐵), 𝑥 = 𝐵 ▶ 𝑦 ∈ 𝑥 )
| | 17:6,16,?: e23 41082 | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦
∧ 𝑦 ∈ 𝐵), 𝑥 = 𝐵 ▶ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) )
| | 18:17: | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦
∧ 𝑦 ∈ 𝐵) ▶ (𝑥 = 𝐵 → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)) )
| | 19:: | ⊢ ¬ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)
| | 20:18,19,?: e20 41054 | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦
∧ 𝑦 ∈ 𝐵) ▶ ¬ 𝑥 = 𝐵 )
| | 21:3,?: e1a 40954 | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) ▶ ∀𝑦 ∈ 𝐴
∀𝑥 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) )
| | 22:21,9,4,?: e121 40983 | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦
∧ 𝑦 ∈ 𝐵) ▶ [𝑥 / 𝑥][𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥
∨ 𝑥 = 𝑦) )
| | 23:22,?: e2 40958 | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦
∧ 𝑦 ∈ 𝐵) ▶ [𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) )
| | 24:4,23,?: e12 41051 | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦
∧ 𝑦 ∈ 𝐵) ▶ (𝑥 ∈ 𝐵 ∨ 𝐵 ∈ 𝑥 ∨ 𝑥 = 𝐵) )
| | 25:14,20,24,?: e222 40963 | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦
∧ 𝑦 ∈ 𝐵) ▶ 𝑥 ∈ 𝐵 )
| | 26:25: | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) ▶ ((𝑥 ∈ 𝑦
∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐵) )
| | 27:: | ⊢ (∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦
∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) → ∀𝑦∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨
𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
| | 28:27,?: e0a 41099 | ⊢ ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)
→ ∀𝑦(Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥
∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴))
| | 29:28,26: | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)
▶ ∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐵) )
| | 30:: | ⊢ (∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦
∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) → ∀𝑥∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦
∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
| | 31:30,?: e0a 41099 | ⊢ ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) → ∀𝑥(Tr 𝐴
∧ ∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴))
| | 32:31,29: | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) ▶ ∀𝑥
∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐵) )
| | 33:32,?: e1a 40954 | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) ▶ Tr 𝐵 )
| | qed:33: | ⊢ ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) → Tr 𝐵)
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
| ⊢ ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) → Tr 𝐵) |
| |
| Theorem | al2imVD 41189 |
Virtual deduction proof of al2im 1811. 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 40954 | ⊢ ( ∀𝑥(𝜑 → (𝜓 → 𝜒))
▶ (∀𝑥𝜑 → ∀𝑥(𝜓 → 𝜒)) )
| | 3:: | ⊢ (∀𝑥(𝜓 → 𝜒) → (∀𝑥𝜓
→ ∀𝑥𝜒))
| | 4:2,3,?: e10 41021 | ⊢ ( ∀𝑥(𝜑 → (𝜓 → 𝜒))
▶ (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)) )
| | qed:4: | ⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒))
→ (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)))
|
(Contributed by Alan Sare, 31-Dec-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))) |
| |
| Theorem | syl5impVD 41190 |
Virtual deduction proof of syl5imp 40839. 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 40954 | ⊢ ( (𝜑 → (𝜓 → 𝜒)) ▶ (𝜓
→ (𝜑 → 𝜒)) )
| | 3:: | ⊢ ( (𝜑 → (𝜓 → 𝜒)) , (𝜃
→ 𝜓) ▶ (𝜃 → 𝜓) )
| | 4:3,2,?: e21 41057 | ⊢ ( (𝜑 → (𝜓 → 𝜒)) , (𝜃
→ 𝜓) ▶ (𝜃 → (𝜑 → 𝜒)) )
| | 5:4,?: e2 40958 | ⊢ ( (𝜑 → (𝜓 → 𝜒)) , (𝜃
→ 𝜓) ▶ (𝜑 → (𝜃 → 𝜒)) )
| | 6:5: | ⊢ ( (𝜑 → (𝜓 → 𝜒)) ▶ ((𝜃
→ 𝜓) → (𝜑 → (𝜃 → 𝜒))) )
| | qed:6: | ⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜃
→ 𝜓) → (𝜑 → (𝜃 → 𝜒))))
|
(Contributed by Alan Sare, 31-Dec-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜃 → 𝜓) → (𝜑 → (𝜃 → 𝜒)))) |
| |
| Theorem | idiVD 41191 |
Virtual deduction proof of idiALT 40804. 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:: | ⊢ 𝜑
| | qed:1,?: e0a 41099 | ⊢ 𝜑
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
| ⊢ 𝜑 ⇒ ⊢ 𝜑 |
| |
| Theorem | ancomstVD 41192 |
Closed form of ancoms 461. 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:: | ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑))
| | qed:1,?: e0a 41099 | ⊢ (((𝜑 ∧ 𝜓) → 𝜒) ↔ ((𝜓
∧ 𝜑) → 𝜒))
|
The proof of ancomst 467 is derived automatically from it.
(Contributed by
Alan Sare, 25-Dec-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
| ⊢ (((𝜑 ∧ 𝜓) → 𝜒) ↔ ((𝜓 ∧ 𝜑) → 𝜒)) |
| |
| Theorem | ssralv2VD 41193* |
Quantification restricted to a subclass for two quantifiers. ssralv 4032
for two quantifiers. The following User's Proof is a Virtual Deduction
proof completed automatically by the tools program
completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm
Megill's Metamath Proof Assistant. ssralv2 40858 is ssralv2VD 41193 without
virtual deductions and was automatically derived from ssralv2VD 41193.
| 1:: | ⊢ ( (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) ▶ (𝐴 ⊆ 𝐵
∧ 𝐶 ⊆ 𝐷) )
| | 2:: | ⊢ ( (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) , ∀𝑥 ∈ 𝐵
∀𝑦 ∈ 𝐷𝜑 ▶ ∀𝑥 ∈ 𝐵∀𝑦 ∈ 𝐷𝜑 )
| | 3:1: | ⊢ ( (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) ▶ 𝐴 ⊆ 𝐵 )
| | 4:3,2: | ⊢ ( (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) , ∀𝑥 ∈ 𝐵
∀𝑦 ∈ 𝐷𝜑 ▶ ∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐷𝜑 )
| | 5:4: | ⊢ ( (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) , ∀𝑥 ∈ 𝐵
∀𝑦 ∈ 𝐷𝜑 ▶ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐷𝜑) )
| | 6:5: | ⊢ ( (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) , ∀𝑥 ∈ 𝐵
∀𝑦 ∈ 𝐷𝜑 ▶ (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐷𝜑) )
| | 7:: | ⊢ ( (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) , ∀𝑥 ∈ 𝐵
∀𝑦 ∈ 𝐷𝜑, 𝑥 ∈ 𝐴 ▶ 𝑥 ∈ 𝐴 )
| | 8:7,6: | ⊢ ( (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) , ∀𝑥 ∈ 𝐵
∀𝑦 ∈ 𝐷𝜑, 𝑥 ∈ 𝐴 ▶ ∀𝑦 ∈ 𝐷𝜑 )
| | 9:1: | ⊢ ( (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) ▶ 𝐶 ⊆ 𝐷 )
| | 10:9,8: | ⊢ ( (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) , ∀𝑥 ∈ 𝐵
∀𝑦 ∈ 𝐷𝜑, 𝑥 ∈ 𝐴 ▶ ∀𝑦 ∈ 𝐶𝜑 )
| | 11:10: | ⊢ ( (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) , ∀𝑥 ∈ 𝐵
∀𝑦 ∈ 𝐷𝜑 ▶ (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐶𝜑) )
| | 12:: | ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)
→ ∀𝑥(𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷))
| | 13:: | ⊢ (∀𝑥 ∈ 𝐵∀𝑦 ∈ 𝐷𝜑
→ ∀𝑥∀𝑥 ∈ 𝐵∀𝑦 ∈ 𝐷𝜑)
| | 14:12,13,11: | ⊢ ( (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) , ∀𝑥 ∈ 𝐵
∀𝑦 ∈ 𝐷𝜑 ▶ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐶𝜑) )
| | 15:14: | ⊢ ( (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) , ∀𝑥 ∈ 𝐵
∀𝑦 ∈ 𝐷𝜑 ▶ ∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐶𝜑 )
| | 16:15: | ⊢ ( (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)
▶ (∀𝑥 ∈ 𝐵∀𝑦 ∈ 𝐷𝜑 → ∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐶𝜑) )
| | qed:16: | ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)
→ (∀𝑥 ∈ 𝐵∀𝑦 ∈ 𝐷𝜑 → ∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐶𝜑))
|
(Contributed by Alan Sare, 10-Feb-2012.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
| ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝜑)) |
| |
| Theorem | ordelordALTVD 41194 |
An element of an ordinal class is ordinal. Proposition 7.6 of
[TakeutiZaring] p. 36. This is an alternate proof of ordelord 6207 using
the Axiom of Regularity indirectly through dford2 9077. dford2 is a
weaker definition of ordinal number. Given the Axiom of Regularity, it
need not be assumed that E Fr 𝐴 because this is inferred by the
Axiom of Regularity. The following User's Proof is a Virtual Deduction
proof completed automatically by the tools program
completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm
Megill's Metamath Proof Assistant. ordelordALT 40864 is ordelordALTVD 41194
without virtual deductions and was automatically derived from
ordelordALTVD 41194 using the tools program
translate..without..overwriting.cmd and the Metamath program "MM-PA>
MINIMIZE_WITH *" command.
| 1:: | ⊢ ( (Ord 𝐴 ∧ 𝐵 ∈ 𝐴) ▶ (Ord 𝐴
∧ 𝐵 ∈ 𝐴) )
| | 2:1: | ⊢ ( (Ord 𝐴 ∧ 𝐵 ∈ 𝐴) ▶ Ord 𝐴 )
| | 3:1: | ⊢ ( (Ord 𝐴 ∧ 𝐵 ∈ 𝐴) ▶ 𝐵 ∈ 𝐴 )
| | 4:2: | ⊢ ( (Ord 𝐴 ∧ 𝐵 ∈ 𝐴) ▶ Tr 𝐴 )
| | 5:2: | ⊢ ( (Ord 𝐴 ∧ 𝐵 ∈ 𝐴) ▶ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) )
| | 6:4,3: | ⊢ ( (Ord 𝐴 ∧ 𝐵 ∈ 𝐴) ▶ 𝐵 ⊆ 𝐴 )
| | 7:6,6,5: | ⊢ ( (Ord 𝐴 ∧ 𝐵 ∈ 𝐴) ▶ ∀𝑥 ∈ 𝐵
∀𝑦 ∈ 𝐵(𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) )
| | 8:: | ⊢ ((𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥)
↔ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
| | 9:8: | ⊢ ∀𝑦((𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥)
↔ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
| | 10:9: | ⊢ ∀𝑦 ∈ 𝐴((𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦
∨ 𝑦 ∈ 𝑥) ↔ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
| | 11:10: | ⊢ (∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦
∨ 𝑦 ∈ 𝑥) ↔ ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
| | 12:11: | ⊢ ∀𝑥(∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦
∨ 𝑦 ∈ 𝑥) ↔ ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
| | 13:12: | ⊢ ∀𝑥 ∈ 𝐴(∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦
∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
| | 14:13: | ⊢ (∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦
∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ ∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥
∨ 𝑥 = 𝑦))
| | 15:14,5: | ⊢ ( (Ord 𝐴 ∧ 𝐵 ∈ 𝐴) ▶ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) )
| | 16:4,15,3: | ⊢ ( (Ord 𝐴 ∧ 𝐵 ∈ 𝐴) ▶ Tr 𝐵 )
| | 17:16,7: | ⊢ ( (Ord 𝐴 ∧ 𝐵 ∈ 𝐴) ▶ Ord 𝐵 )
| | qed:17: | ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐵)
|
(Contributed by Alan Sare, 12-Feb-2012.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
| ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐵) |
| |
| Theorem | equncomVD 41195 |
If a class equals the union of two other classes, then it equals the union
of those two classes commuted. The following User's Proof is a Virtual
Deduction proof completed automatically by the tools program
completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm
Megill's Metamath Proof Assistant. equncom 4129 is equncomVD 41195 without
virtual deductions and was automatically derived from equncomVD 41195.
| 1:: | ⊢ ( 𝐴 = (𝐵 ∪ 𝐶) ▶ 𝐴 = (𝐵 ∪ 𝐶) )
| | 2:: | ⊢ (𝐵 ∪ 𝐶) = (𝐶 ∪ 𝐵)
| | 3:1,2: | ⊢ ( 𝐴 = (𝐵 ∪ 𝐶) ▶ 𝐴 = (𝐶 ∪ 𝐵) )
| | 4:3: | ⊢ (𝐴 = (𝐵 ∪ 𝐶) → 𝐴 = (𝐶 ∪ 𝐵))
| | 5:: | ⊢ ( 𝐴 = (𝐶 ∪ 𝐵) ▶ 𝐴 = (𝐶 ∪ 𝐵) )
| | 6:5,2: | ⊢ ( 𝐴 = (𝐶 ∪ 𝐵) ▶ 𝐴 = (𝐵 ∪ 𝐶) )
| | 7:6: | ⊢ (𝐴 = (𝐶 ∪ 𝐵) → 𝐴 = (𝐵 ∪ 𝐶))
| | 8:4,7: | ⊢ (𝐴 = (𝐵 ∪ 𝐶) ↔ 𝐴 = (𝐶 ∪ 𝐵))
|
(Contributed by Alan Sare, 17-Feb-2012.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ (𝐴 = (𝐵 ∪ 𝐶) ↔ 𝐴 = (𝐶 ∪ 𝐵)) |
| |
| Theorem | equncomiVD 41196 |
Inference form of equncom 4129. The following User's Proof is a
Virtual Deduction proof completed automatically by the tools program
completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm
Megill's Metamath Proof Assistant. equncomi 4130 is equncomiVD 41196 without
virtual deductions and was automatically derived from equncomiVD 41196.
| h1:: | ⊢ 𝐴 = (𝐵 ∪ 𝐶)
| | qed:1: | ⊢ 𝐴 = (𝐶 ∪ 𝐵)
|
(Contributed by Alan Sare, 18-Feb-2012.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
| ⊢ 𝐴 = (𝐵 ∪ 𝐶) ⇒ ⊢ 𝐴 = (𝐶 ∪ 𝐵) |
| |
| Theorem | sucidALTVD 41197 |
A set belongs to its successor. Alternate proof of sucid 6264.
The following User's Proof is a Virtual Deduction proof
completed automatically by the tools program
completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm
Megill's Metamath Proof Assistant. sucidALT 41198 is sucidALTVD 41197
without virtual deductions and was automatically derived from
sucidALTVD 41197. This proof illustrates that
completeusersproof.cmd will generate a Metamath proof from any
User's Proof which is "conventional" in the sense that no step
is a virtual deduction, provided that all necessary unification
theorems and transformation deductions are in set.mm.
completeusersproof.cmd automatically converts such a
conventional proof into a Virtual Deduction proof for which each
step happens to be a 0-virtual hypothesis virtual deduction.
The user does not need to search for reference theorem labels or
deduction labels nor does he(she) need to use theorems and
deductions which unify with reference theorems and deductions in
set.mm. All that is necessary is that each theorem or deduction
of the User's Proof unifies with some reference theorem or
deduction in set.mm or is a semantic variation of some theorem
or deduction which unifies with some reference theorem or
deduction in set.mm. The definition of "semantic variation" has
not been precisely defined. If it is obvious that a theorem or
deduction has the same meaning as another theorem or deduction,
then it is a semantic variation of the latter theorem or
deduction. For example, step 4 of the User's Proof is a
semantic variation of the definition (axiom)
suc 𝐴 = (𝐴 ∪ {𝐴}), which unifies with df-suc 6191, a
reference definition (axiom) in set.mm. Also, a theorem or
deduction is said to be a semantic variation of another
theorem or deduction if it is obvious upon cursory inspection
that it has the same meaning as a weaker form of the latter
theorem or deduction. For example, the deduction Ord 𝐴
infers ∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) is a
semantic variation of the theorem (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥))), which unifies with
the set.mm reference definition (axiom) dford2 9077.
| h1:: | ⊢ 𝐴 ∈ V
| | 2:1: | ⊢ 𝐴 ∈ {𝐴}
| | 3:2: | ⊢ 𝐴 ∈ ({𝐴} ∪ 𝐴)
| | 4:: | ⊢ suc 𝐴 = ({𝐴} ∪ 𝐴)
| | qed:3,4: | ⊢ 𝐴 ∈ suc 𝐴
|
(Contributed by Alan Sare, 18-Feb-2012.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
| ⊢ 𝐴 ∈
V ⇒ ⊢ 𝐴 ∈ suc 𝐴 |
| |
| Theorem | sucidALT 41198 |
A set belongs to its successor. This proof was automatically derived
from sucidALTVD 41197 using translate_without_overwriting.cmd and
minimizing. (Contributed by Alan Sare, 18-Feb-2012.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ 𝐴 ∈
V ⇒ ⊢ 𝐴 ∈ suc 𝐴 |
| |
| Theorem | sucidVD 41199 |
A set belongs to its successor. The following User's Proof is a
Virtual Deduction proof completed automatically by the tools
program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2
and Norm Megill's Metamath Proof Assistant.
sucid 6264 is sucidVD 41199 without virtual deductions and was automatically
derived from sucidVD 41199.
| h1:: | ⊢ 𝐴 ∈ V
| | 2:1: | ⊢ 𝐴 ∈ {𝐴}
| | 3:2: | ⊢ 𝐴 ∈ (𝐴 ∪ {𝐴})
| | 4:: | ⊢ suc 𝐴 = (𝐴 ∪ {𝐴})
| | qed:3,4: | ⊢ 𝐴 ∈ suc 𝐴
|
(Contributed by Alan Sare, 18-Feb-2012.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
| ⊢ 𝐴 ∈
V ⇒ ⊢ 𝐴 ∈ suc 𝐴 |
| |
| Theorem | imbi12VD 41200 |
Implication form of imbi12i 353. The following User's Proof is a Virtual
Deduction proof completed automatically by the tools program
completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm
Megill's Metamath Proof Assistant. imbi12 349 is imbi12VD 41200 without virtual
deductions and was automatically derived from imbi12VD 41200.
| 1:: | ⊢ ( (𝜑 ↔ 𝜓) ▶ (𝜑 ↔ 𝜓) )
| | 2:: | ⊢ ( (𝜑 ↔ 𝜓) , (𝜒 ↔ 𝜃)
▶ (𝜒 ↔ 𝜃) )
| | 3:: | ⊢ ( (𝜑 ↔ 𝜓) , (𝜒 ↔ 𝜃) , (𝜑
→ 𝜒) ▶ (𝜑 → 𝜒) )
| | 4:1,3: | ⊢ ( (𝜑 ↔ 𝜓) , (𝜒 ↔ 𝜃) , (𝜑
→ 𝜒) ▶ (𝜓 → 𝜒) )
| | 5:2,4: | ⊢ ( (𝜑 ↔ 𝜓) , (𝜒 ↔ 𝜃) , (𝜑
→ 𝜒) ▶ (𝜓 → 𝜃) )
| | 6:5: | ⊢ ( (𝜑 ↔ 𝜓) , (𝜒 ↔ 𝜃)
▶ ((𝜑 → 𝜒) → (𝜓 → 𝜃)) )
| | 7:: | ⊢ ( (𝜑 ↔ 𝜓) , (𝜒 ↔ 𝜃) , (𝜓
→ 𝜃) ▶ (𝜓 → 𝜃) )
| | 8:1,7: | ⊢ ( (𝜑 ↔ 𝜓) , (𝜒 ↔ 𝜃) , (𝜓
→ 𝜃) ▶ (𝜑 → 𝜃) )
| | 9:2,8: | ⊢ ( (𝜑 ↔ 𝜓) , (𝜒 ↔ 𝜃) , (𝜓
→ 𝜃) ▶ (𝜑 → 𝜒) )
| | 10:9: | ⊢ ( (𝜑 ↔ 𝜓) , (𝜒 ↔ 𝜃)
▶ ((𝜓 → 𝜃) → (𝜑 → 𝜒)) )
| | 11:6,10: | ⊢ ( (𝜑 ↔ 𝜓) , (𝜒 ↔ 𝜃)
▶ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃)) )
| | 12:11: | ⊢ ( (𝜑 ↔ 𝜓) ▶ ((𝜒 ↔ 𝜃)
→ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃))) )
| | qed:12: | ⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ↔ 𝜃)
→ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃))))
|
(Contributed by Alan Sare, 18-Mar-2012.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ↔ 𝜃) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃)))) |
Home
Hilbert Space Explorer
Users' Mathboxes