Theorem List for Metamath Proof Explorer - 45601-45700 *Has distinct variable
group(s)
| Type | Label | Description |
|---|
| Statement |
|---|
| |
| Theorem | eelTT 45601 |
An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ (⊤
→ 𝜑) & ⊢ (⊤
→ 𝜓) & ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ 𝜒 |
| |
| Theorem | e0a 45602 |
Elimination rule identical to ax-mp 5. The non-virtual deduction form
is the virtual deduction form, which is ax-mp 5.
(Contributed by Alan
Sare, 14-Jun-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
| ⊢ 𝜑 & ⊢ (𝜑 → 𝜓) ⇒ ⊢ 𝜓 |
| |
| Theorem | eelT 45603 |
An elimination deduction. (Contributed by Alan Sare, 5-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ (⊤
→ 𝜑) & ⊢ (𝜑 → 𝜓) ⇒ ⊢ 𝜓 |
| |
| Theorem | eel0cT 45604 |
An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ 𝜑 & ⊢ (𝜑 → 𝜓) ⇒ ⊢ (⊤ → 𝜓) |
| |
| Theorem | eelT0 45605 |
An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ (⊤
→ 𝜑) & ⊢ 𝜓 & ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ 𝜒 |
| |
| Theorem | e0bi 45606 |
Elimination rule identical to mpbi 233. The non-virtual deduction form
is the virtual deduction form, which is mpbi 233.
(Contributed by Alan
Sare, 15-Jun-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
| ⊢ 𝜑 & ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ 𝜓 |
| |
| Theorem | e0bir 45607 |
Elimination rule identical to mpbir 234. The non-virtual deduction form
is the virtual deduction form, which is mpbir 234. (Contributed by Alan
Sare, 15-Jun-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
| ⊢ 𝜑 & ⊢ (𝜓 ↔ 𝜑) ⇒ ⊢ 𝜓 |
| |
| Theorem | uun0.1 45608 |
Convention notation form of un0.1 45609. (Contributed by Alan Sare,
23-Apr-2015.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
| ⊢ (⊤
→ 𝜑) & ⊢ (𝜓 → 𝜒)
& ⊢ ((⊤ ∧ 𝜓) → 𝜃) ⇒ ⊢ (𝜓 → 𝜃) |
| |
| Theorem | un0.1 45609 |
⊤ is the constant true, a tautology (see df-tru 1573). 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 45610 |
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 1573. (Revised by David
A. Wheeler, 8-May-2019.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
| ⊢ ((⊤
∧ 𝜑) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) |
| |
| Theorem | uunT1p1 45611 |
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 45612 |
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 45613 |
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 45614 |
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 45615 |
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 45616 |
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 45617 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
This would have been named uun221 if the zeroth permutation did not
exist in set.mm as anabss7 686. (Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ (((𝜓 ∧ 𝜑) ∧ 𝜑) → 𝜒) ⇒ ⊢ ((𝜓 ∧ 𝜑) → 𝜒) |
| |
| Theorem | un10 45618 |
A unionizing deduction. (Contributed by Alan Sare, 28-Apr-2015.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ ( ( 𝜑 , ⊤ ) ▶ 𝜓 )
⇒ ⊢ ( 𝜑 ▶ 𝜓 ) |
| |
| Theorem | un01 45619 |
A unionizing deduction. (Contributed by Alan Sare, 28-Apr-2015.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ ( ( ⊤ , 𝜑 ) ▶ 𝜓 )
⇒ ⊢ ( 𝜑 ▶ 𝜓 ) |
| |
| Theorem | un2122 45620 |
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 45621 |
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 45622 |
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 45623 |
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 45624 |
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 45625 |
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 45626 |
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 45627 |
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 45628 |
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 45629 |
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 45630 |
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 45631 |
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 45632 |
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 45633 |
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 45634 |
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 45635 |
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 45636 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
3anidm12 1446 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 45637 |
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 45638 |
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 45639 |
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 45640 |
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 45641 |
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 45642 |
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 45643 |
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 45644 |
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 45645 |
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 45646 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
Commuted version of 3impdir 1370. (Contributed by Alan Sare,
4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ (((𝜒 ∧ 𝜓) ∧ (𝜑 ∧ 𝜓)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃) |
| |
| Theorem | 3impcombi 45647 |
A 1-hypothesis propositional calculus deduction. (Contributed by Alan
Sare, 25-Sep-2017.)
|
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜑) → (𝜒 ↔ 𝜃)) ⇒ ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃) |
| |
| 21.43.6 Theorems proved using Virtual
Deduction
|
| |
| Theorem | trsspwALT 45648 |
Virtual deduction proof of the left-to-right implication of dftr4 5222. A
transitive class is a subset of its power class. This proof corresponds
to the virtual deduction proof of dftr4 5222 without accumulating results.
(Contributed by Alan Sare, 29-Apr-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ (Tr 𝐴 → 𝐴 ⊆ 𝒫 𝐴) |
| |
| Theorem | trsspwALT2 45649 |
Virtual deduction proof of trsspwALT 45648. This proof is the same as the
proof of trsspwALT 45648 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 45650 |
Short predicate calculus proof of the left-to-right implication of
dftr4 5222. 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 45649, which is the virtual deduction proof trsspwALT 45648
without virtual deductions. (Contributed by Alan Sare, 30-Apr-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ (Tr 𝐴 → 𝐴 ⊆ 𝒫 𝐴) |
| |
| Theorem | sspwtr 45651 |
Virtual deduction proof of the right-to-left implication of dftr4 5222. A
class which is a subclass of its power class is transitive. This proof
corresponds to the virtual deduction proof of sspwtr 45651 without
accumulating results. (Contributed by Alan Sare, 2-May-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ (𝐴 ⊆ 𝒫 𝐴 → Tr 𝐴) |
| |
| Theorem | sspwtrALT 45652 |
Virtual deduction proof of sspwtr 45651. This proof is the same as the
proof of sspwtr 45651 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 45653 |
Short predicate calculus proof of the right-to-left implication of
dftr4 5222. 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 45652, which is the virtual deduction proof sspwtr 45651
without virtual deductions. (Contributed by Alan Sare, 3-May-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ (𝐴 ⊆ 𝒫 𝐴 → Tr 𝐴) |
| |
| Theorem | pwtrVD 45654 |
Virtual deduction proof of pwtr 5431; see pwtrrVD 45655 for the converse.
(Contributed by Alan Sare, 25-Aug-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ (Tr 𝐴 → Tr 𝒫 𝐴) |
| |
| Theorem | pwtrrVD 45655 |
Virtual deduction proof of pwtr 5431; see pwtrVD 45654 for the converse.
(Contributed by Alan Sare, 25-Aug-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ 𝐴 ∈
V ⇒ ⊢ (Tr 𝒫 𝐴 → Tr 𝐴) |
| |
| Theorem | suctrALT 45656 |
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 45656 using completeusersproof, which is
verified by the Metamath program. The proof of
https://us.metamath.org/other/completeusersproof/suctrro.html 45656 is a
form of the completed proof which preserves the Virtual Deduction
proof's step numbers and their ordering. See suctr 6450 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 45657 |
Virtual deduction proof of snssiALT 45658. (Contributed by Alan Sare,
11-Sep-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
| ⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵) |
| |
| Theorem | snssiALT 45658 |
If a class is an element of another class, then its singleton is a
subclass of that other class. Alternate proof of snssi 4749. This
theorem was automatically generated from snssiALTVD 45657 using a
translation program. (Contributed by Alan Sare, 11-Sep-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵) |
| |
| Theorem | snsslVD 45659 |
Virtual deduction proof of snssl 45660. (Contributed by Alan Sare,
25-Aug-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
| ⊢ 𝐴 ∈
V ⇒ ⊢ ({𝐴} ⊆ 𝐵 → 𝐴 ∈ 𝐵) |
| |
| Theorem | snssl 45660 |
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 4748.
The proof of
this theorem was automatically generated from snsslVD 45659 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 45661 |
Virtual deduction proof of snelpwi 5423. (Contributed by Alan Sare,
25-Aug-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
| ⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ 𝒫 𝐵) |
| |
| Theorem | unipwrVD 45662 |
Virtual deduction proof of unipwr 45663. (Contributed by Alan Sare,
25-Aug-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
| ⊢ 𝐴 ⊆ ∪ 𝒫 𝐴 |
| |
| Theorem | unipwr 45663 |
A class is a subclass of the union of its power class. This theorem is
the right-to-left subclass lemma of unipw 5429. The proof of this theorem
was automatically generated from unipwrVD 45662 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 45664 |
Virtual deduction proof of sstrALT2 45665. (Contributed by Alan Sare,
11-Sep-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
| ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶) |
| |
| Theorem | sstrALT2 45665 |
Virtual deduction proof of sstr 3942, transitivity of subclasses, Theorem
6 of [Suppes] p. 23. This theorem was
automatically generated from
sstrALT2VD 45664 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 45666 |
Virtual deduction proof of suctrALT2 45667. (Contributed by Alan Sare,
11-Sep-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
| ⊢ (Tr 𝐴 → Tr suc 𝐴) |
| |
| Theorem | suctrALT2 45667 |
Virtual deduction proof of suctr 6450. The successor of a transitive
class is transitive. This proof was generated automatically from the
virtual deduction proof suctrALT2VD 45666 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 45668* |
Virtual deduction proof of elex2 2839. (Contributed by Alan Sare,
25-Sep-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
| ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 ∈ 𝐵) |
| |
| Theorem | elex22VD 45669* |
Virtual deduction proof of elex22 3477. (Contributed by Alan Sare,
24-Oct-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
| ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)) |
| |
| Theorem | eqsbc2VD 45670* |
Virtual deduction proof of eqsbc2 3805. (Contributed by Alan Sare,
24-Oct-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
| ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]𝐶 = 𝑥 ↔ 𝐶 = 𝐴)) |
| |
| Theorem | zfregs2VD 45671* |
Virtual deduction proof of zfregs2 9716. (Contributed by Alan Sare,
24-Oct-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
| ⊢ (𝐴 ≠ ∅ → ¬
∀𝑥 ∈ 𝐴 ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥)) |
| |
| Theorem | tpid3gVD 45672 |
Virtual deduction proof of tpid3g 4736. (Contributed by Alan Sare,
24-Oct-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
| ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ {𝐶, 𝐷, 𝐴}) |
| |
| Theorem | en3lplem1VD 45673* |
Virtual deduction proof of en3lplem1 9595. (Contributed by Alan Sare,
24-Oct-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
| ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → (𝑥 = 𝐴 → ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥))) |
| |
| Theorem | en3lplem2VD 45674* |
Virtual deduction proof of en3lplem2 9596. (Contributed by Alan Sare,
24-Oct-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
| ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → (𝑥 ∈ {𝐴, 𝐵, 𝐶} → ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥))) |
| |
| Theorem | en3lpVD 45675 |
Virtual deduction proof of en3lp 9597. (Contributed by Alan Sare,
24-Oct-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
| ⊢ ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) |
| |
| 21.43.7 Theorems proved using Virtual Deduction
with mmj2 assistance
|
| |
| Theorem | simplbi2VD 45676 |
Virtual deduction proof of simplbi2 506. 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 45602 | ⊢ ((𝜓 ∧ 𝜒) → 𝜑)
| | qed:3,?: e0a 45602 | ⊢ (𝜓 → (𝜒 → 𝜑))
|
The proof of simplbi2 506 was automatically derived from it.
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
| ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜓 → (𝜒 → 𝜑)) |
| |
| Theorem | 3ornot23VD 45677 |
Virtual deduction proof of 3ornot23 45340. 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 45458 | ⊢ ( (¬ 𝜑 ∧ ¬ 𝜓) ▶ ¬ 𝜑 )
| | 4:1,?: e1a 45458 | ⊢ ( (¬ 𝜑 ∧ ¬ 𝜓) ▶ ¬ 𝜓 )
| | 5:3,4,?: e11 45519 | ⊢ ( (¬ 𝜑 ∧ ¬ 𝜓) ▶ ¬ (𝜑
∨ 𝜓) )
| | 6:2,?: e2 45462 | ⊢ ( (¬ 𝜑 ∧ ¬ 𝜓) , (𝜒 ∨ 𝜑
∨ 𝜓) ▶ (𝜒 ∨ (𝜑 ∨ 𝜓)) )
| | 7:5,6,?: e12 45554 | ⊢ ( (¬ 𝜑 ∧ ¬ 𝜓) , (𝜒 ∨ 𝜑
∨ 𝜓) ▶ 𝜒 )
| | 8:7: | ⊢ ( (¬ 𝜑 ∧ ¬ 𝜓) ▶ ((𝜒
∨ 𝜑 ∨ 𝜓) → 𝜒) )
| | qed:8: | ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ((𝜒
∨ 𝜑 ∨ 𝜓) → 𝜒))
|
(Contributed by Alan Sare, 31-Dec-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ((𝜒 ∨ 𝜑 ∨ 𝜓) → 𝜒)) |
| |
| Theorem | orbi1rVD 45678 |
Virtual deduction proof of orbi1r 45341. 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 45462 | ⊢ ( (𝜑 ↔ 𝜓) , (𝜒 ∨ 𝜑)
▶ (𝜑 ∨ 𝜒) )
| | 4:1,3,?: e12 45554 | ⊢ ( (𝜑 ↔ 𝜓) , (𝜒 ∨ 𝜑)
▶ (𝜓 ∨ 𝜒) )
| | 5:4,?: e2 45462 | ⊢ ( (𝜑 ↔ 𝜓) , (𝜒 ∨ 𝜑)
▶ (𝜒 ∨ 𝜓) )
| | 6:5: | ⊢ ( (𝜑 ↔ 𝜓) ▶ ((𝜒 ∨ 𝜑)
→ (𝜒 ∨ 𝜓)) )
| | 7:: | ⊢ ( (𝜑 ↔ 𝜓) , (𝜒 ∨ 𝜓)
▶ (𝜒 ∨ 𝜓) )
| | 8:7,?: e2 45462 | ⊢ ( (𝜑 ↔ 𝜓) , (𝜒 ∨ 𝜓)
▶ (𝜓 ∨ 𝜒) )
| | 9:1,8,?: e12 45554 | ⊢ ( (𝜑 ↔ 𝜓) , (𝜒 ∨ 𝜓)
▶ (𝜑 ∨ 𝜒) )
| | 10:9,?: e2 45462 | ⊢ ( (𝜑 ↔ 𝜓) , (𝜒 ∨ 𝜓)
▶ (𝜒 ∨ 𝜑) )
| | 11:10: | ⊢ ( (𝜑 ↔ 𝜓) ▶ ((𝜒 ∨ 𝜓)
→ (𝜒 ∨ 𝜑)) )
| | 12:6,11,?: e11 45519 | ⊢ ( (𝜑 ↔ 𝜓) ▶ ((𝜒
∨ 𝜑) ↔ (𝜒 ∨ 𝜓)) )
| | qed:12: | ⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ∨ 𝜑)
↔ (𝜒 ∨ 𝜓)))
|
(Contributed by Alan Sare, 31-Dec-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓))) |
| |
| Theorem | bitr3VD 45679 |
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 45458 | ⊢ ( (𝜑 ↔ 𝜓) ▶ (𝜓
↔ 𝜑) )
| | 3:: | ⊢ ( (𝜑 ↔ 𝜓) , (𝜑 ↔ 𝜒)
▶ (𝜑 ↔ 𝜒) )
| | 4:3,?: e2 45462 | ⊢ ( (𝜑 ↔ 𝜓) , (𝜑 ↔ 𝜒)
▶ (𝜒 ↔ 𝜑) )
| | 5:2,4,?: e12 45554 | ⊢ ( (𝜑 ↔ 𝜓) , (𝜑 ↔ 𝜒)
▶ (𝜓 ↔ 𝜒) )
| | 6:5: | ⊢ ( (𝜑 ↔ 𝜓) ▶ ((𝜑
↔ 𝜒) → (𝜓 ↔ 𝜒)) )
| | qed:6: | ⊢ ((𝜑 ↔ 𝜓) → ((𝜑 ↔ 𝜒)
→ (𝜓 ↔ 𝜒)))
|
(Contributed by Alan Sare, 31-Dec-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ ((𝜑 ↔ 𝜓) → ((𝜑 ↔ 𝜒) → (𝜓 ↔ 𝜒))) |
| |
| Theorem | 3orbi123VD 45680 |
Virtual deduction proof of 3orbi123 45342. 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 45458 | ⊢ ( ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)
∧ (𝜏 ↔ 𝜂)) ▶ (𝜑 ↔ 𝜓) )
| | 3:1,?: e1a 45458 | ⊢ ( ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)
∧ (𝜏 ↔ 𝜂)) ▶ (𝜒 ↔ 𝜃) )
| | 4:1,?: e1a 45458 | ⊢ ( ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)
∧ (𝜏 ↔ 𝜂)) ▶ (𝜏 ↔ 𝜂) )
| | 5:2,3,?: e11 45519 | ⊢ ( ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)
∧ (𝜏 ↔ 𝜂)) ▶ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃)) )
| | 6:5,4,?: e11 45519 | ⊢ ( ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)
∧ (𝜏 ↔ 𝜂)) ▶ (((𝜑 ∨ 𝜒) ∨ 𝜏) ↔ ((𝜓 ∨ 𝜃)
∨ 𝜂)) )
| | 7:?: | ⊢ (((𝜑 ∨ 𝜒) ∨ 𝜏) ↔ (𝜑
∨ 𝜒 ∨ 𝜏))
| | 8:6,7,?: e10 45525 | ⊢ ( ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)
∧ (𝜏 ↔ 𝜂)) ▶ ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ ((𝜓 ∨ 𝜃)
∨ 𝜂)) )
| | 9:?: | ⊢ (((𝜓 ∨ 𝜃) ∨ 𝜂) ↔
(𝜓 ∨ 𝜃 ∨ 𝜂))
| | 10:8,9,?: e10 45525 | ⊢ ( ((𝜑 ↔ 𝜓) ∧ (𝜒
↔ 𝜃) ∧ (𝜏 ↔ 𝜂)) ▶ ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ (𝜓 ∨
𝜃 ∨ 𝜂)) )
| | qed:10: | ⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)
∧ (𝜏 ↔ 𝜂)) → ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ (𝜓 ∨ 𝜃
∨ 𝜂)))
|
(Contributed by Alan Sare, 31-Dec-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂)) → ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ (𝜓 ∨ 𝜃 ∨ 𝜂))) |
| |
| Theorem | sbc3orgVD 45681 |
Virtual deduction proof of the analogue of sbcor 3792 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 45458 | ⊢ ( 𝐴 ∈ 𝐵 ▶ ([𝐴 / 𝑥]((𝜑
∨ 𝜓) ∨ 𝜒) ↔ ([𝐴 / 𝑥](𝜑 ∨ 𝜓)
∨ [𝐴 / 𝑥]𝜒)) )
| | 3:: | ⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑
∨ 𝜓 ∨ 𝜒))
| | 32:3: | ⊢ ∀𝑥(((𝜑 ∨ 𝜓) ∨ 𝜒)
↔ (𝜑 ∨ 𝜓 ∨ 𝜒))
| | 33:1,32,?: e10 45525 | ⊢ ( 𝐴 ∈ 𝐵 ▶ [𝐴 / 𝑥](((𝜑
∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ 𝜓 ∨ 𝜒)) )
| | 4:1,33,?: e11 45519 | ⊢ ( 𝐴 ∈ 𝐵 ▶ ([𝐴 / 𝑥]((𝜑
∨ 𝜓) ∨ 𝜒) ↔ [𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒)) )
| | 5:2,4,?: e11 45519 | ⊢ ( 𝐴 ∈ 𝐵 ▶ ([𝐴 / 𝑥](𝜑
∨ 𝜓 ∨ 𝜒) ↔ ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ∨ [𝐴 / 𝑥]𝜒)) )
| | 6:1,?: e1a 45458 | ⊢ ( 𝐴 ∈ 𝐵 ▶ ([𝐴 / 𝑥](𝜑
∨ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓)) )
| | 7:6,?: e1a 45458 | ⊢ ( 𝐴 ∈ 𝐵 ▶ (([𝐴 / 𝑥](𝜑
∨ 𝜓) ∨ [𝐴 / 𝑥]𝜒) ↔ (([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓)
∨ [𝐴 / 𝑥]𝜒)) )
| | 8:5,7,?: e11 45519 | ⊢ ( 𝐴 ∈ 𝐵 ▶ ([𝐴 / 𝑥](𝜑
∨ 𝜓 ∨ 𝜒) ↔ (([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓)
∨ [𝐴 / 𝑥]𝜒)) )
| | 9:?: | ⊢ ((([𝐴 / 𝑥]𝜑
∨ [𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒) ↔ ([𝐴 / 𝑥]𝜑
∨ [𝐴 / 𝑥]𝜓 ∨ [𝐴 / 𝑥]𝜒))
| | 10:8,9,?: e10 45525 | ⊢ ( 𝐴 ∈ 𝐵 ▶ ([𝐴 / 𝑥](𝜑
∨ 𝜓 ∨ 𝜒) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓
∨ [𝐴 / 𝑥]𝜒)) )
| | qed:10: | ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](𝜑
∨ 𝜓 ∨ 𝜒) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓
∨ [𝐴 / 𝑥]𝜒)))
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
| ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓 ∨ [𝐴 / 𝑥]𝜒))) |
| |
| Theorem | 19.21a3con13vVD 45682* |
Virtual deduction proof of alrim3con13v 45364. 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 45462 | ⊢ ( (𝜑 → ∀𝑥𝜑) , (𝜓
∧ 𝜑 ∧ 𝜒) ▶ 𝜓 )
| | 4:2,?: e2 45462 | ⊢ ( (𝜑 → ∀𝑥𝜑) , (𝜓
∧ 𝜑 ∧ 𝜒) ▶ 𝜑 )
| | 5:2,?: e2 45462 | ⊢ ( (𝜑 → ∀𝑥𝜑) , (𝜓
∧ 𝜑 ∧ 𝜒) ▶ 𝜒 )
| | 6:1,4,?: e12 45554 | ⊢ ( (𝜑 → ∀𝑥𝜑) , (𝜓
∧ 𝜑 ∧ 𝜒) ▶ ∀𝑥𝜑 )
| | 7:3,?: e2 45462 | ⊢ ( (𝜑 → ∀𝑥𝜑) , (𝜓
∧ 𝜑 ∧ 𝜒) ▶ ∀𝑥𝜓 )
| | 8:5,?: e2 45462 | ⊢ ( (𝜑 → ∀𝑥𝜑) , (𝜓
∧ 𝜑 ∧ 𝜒) ▶ ∀𝑥𝜒 )
| | 9:7,6,8,?: e222 45467 | ⊢ ( (𝜑 → ∀𝑥𝜑) , (𝜓
∧ 𝜑 ∧ 𝜒) ▶ (∀𝑥𝜓 ∧ ∀𝑥𝜑 ∧ ∀𝑥𝜒) )
| | 10:9,?: e2 45462 | ⊢ ( (𝜑 → ∀𝑥𝜑) , (𝜓
∧ 𝜑 ∧ 𝜒) ▶ ∀𝑥(𝜓 ∧ 𝜑 ∧ 𝜒) )
| | 11:10:in2 | ⊢ ( (𝜑 → ∀𝑥𝜑) ▶ ((𝜓
∧ 𝜑 ∧ 𝜒) → ∀𝑥(𝜓 ∧ 𝜑 ∧ 𝜒)) )
| | qed:11:in1 | ⊢ ((𝜑 → ∀𝑥𝜑) → ((𝜓
∧ 𝜑 ∧ 𝜒) → ∀𝑥(𝜓 ∧ 𝜑 ∧ 𝜒)))
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
| ⊢ ((𝜑 → ∀𝑥𝜑) → ((𝜓 ∧ 𝜑 ∧ 𝜒) → ∀𝑥(𝜓 ∧ 𝜑 ∧ 𝜒))) |
| |
| Theorem | exbirVD 45683 |
Virtual deduction proof of exbir 45310. 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 45554 | ⊢ ( ((𝜑 ∧ 𝜓) → (𝜒
↔ 𝜃)), (𝜑 ∧ 𝜓) ▶ (𝜒 ↔ 𝜃) )
| | 6:3,5,?: e32 45588 | ⊢ ( ((𝜑 ∧ 𝜓) → (𝜒
↔ 𝜃)), (𝜑 ∧ 𝜓), 𝜃 ▶ 𝜒 )
| | 7:6: | ⊢ ( ((𝜑 ∧ 𝜓) → (𝜒
↔ 𝜃)), (𝜑 ∧ 𝜓) ▶ (𝜃 → 𝜒) )
| | 8:7: | ⊢ ( ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))
▶ ((𝜑 ∧ 𝜓) → (𝜃 → 𝜒)) )
| | 9:8,?: e1a 45458 | ⊢ ( ((𝜑 ∧ 𝜓) → (𝜒
↔ 𝜃)) ▶ (𝜑 → (𝜓 → (𝜃 → 𝜒))) )
| | qed:9: | ⊢ (((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))
→ (𝜑 → (𝜓 → (𝜃 → 𝜒))))
|
(Contributed by Alan Sare, 13-Dec-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ (((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) → (𝜑 → (𝜓 → (𝜃 → 𝜒)))) |
| |
| Theorem | exbiriVD 45684 |
Virtual deduction proof of exbiri 823. 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 45525 | ⊢ ( 𝜑 ▶ (𝜓 → (𝜒 ↔ 𝜃)) )
| | 6:3,5,?: e21 45560 | ⊢ ( 𝜑 , 𝜓 ▶ (𝜒 ↔ 𝜃) )
| | 7:4,6,?: e32 45588 | ⊢ ( 𝜑 , 𝜓 , 𝜃 ▶ 𝜒 )
| | 8:7: | ⊢ ( 𝜑 , 𝜓 ▶ (𝜃 → 𝜒) )
| | 9:8: | ⊢ ( 𝜑 ▶ (𝜓 → (𝜃 → 𝜒)) )
| | qed:9: | ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒)))
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
| ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒))) |
| |
| Theorem | rspsbc2VD 45685* |
Virtual deduction proof of rspsbc2 45365. 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 45578 | ⊢ ( 𝐴 ∈ 𝐵 , 𝐶 ∈ 𝐷 , ∀𝑥 ∈ 𝐵
∀𝑦 ∈ 𝐷𝜑 ▶ [𝐴 / 𝑥]∀𝑦 ∈ 𝐷𝜑 )
| | 5:1,4,?: e13 45578 | ⊢ ( 𝐴 ∈ 𝐵 , 𝐶 ∈ 𝐷 , ∀𝑥 ∈ 𝐵
∀𝑦 ∈ 𝐷𝜑 ▶ ∀𝑦 ∈ 𝐷[𝐴 / 𝑥]𝜑 )
| | 6:2,5,?: e23 45585 | ⊢ ( 𝐴 ∈ 𝐵 , 𝐶 ∈ 𝐷 , ∀𝑥 ∈ 𝐵
∀𝑦 ∈ 𝐷𝜑 ▶ [𝐶 / 𝑦][𝐴 / 𝑥]𝜑 )
| | 7:6: | ⊢ ( 𝐴 ∈ 𝐵 , 𝐶 ∈ 𝐷 ▶ (∀𝑥 ∈ 𝐵
∀𝑦 ∈ 𝐷𝜑 → [𝐶 / 𝑦][𝐴 / 𝑥]𝜑) )
| | 8:7: | ⊢ ( 𝐴 ∈ 𝐵 ▶ (𝐶 ∈ 𝐷
→ (∀𝑥 ∈ 𝐵∀𝑦 ∈ 𝐷𝜑 → [𝐶 / 𝑦][𝐴 / 𝑥]𝜑)) )
| | qed:8: | ⊢ (𝐴 ∈ 𝐵 → (𝐶 ∈ 𝐷
→ (∀𝑥 ∈ 𝐵∀𝑦 ∈ 𝐷𝜑 → [𝐶 / 𝑦][𝐴 / 𝑥]𝜑)))
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
| ⊢ (𝐴 ∈ 𝐵 → (𝐶 ∈ 𝐷 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑 → [𝐶 / 𝑦][𝐴 / 𝑥]𝜑))) |
| |
| Theorem | 3impexpVD 45686 |
Virtual deduction proof of 3impexp 1377. 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 45525 | ⊢ ( ((𝜑 ∧ 𝜓 ∧ 𝜒)
→ 𝜃) ▶ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) )
| | 4:3,?: e1a 45458 | ⊢ ( ((𝜑 ∧ 𝜓 ∧ 𝜒)
→ 𝜃) ▶ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) )
| | 5:4,?: e1a 45458 | ⊢ ( ((𝜑 ∧ 𝜓 ∧ 𝜒)
→ 𝜃) ▶ (𝜑 → (𝜓 → (𝜒 → 𝜃))) )
| | 6:5: | ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
→ (𝜑 → (𝜓 → (𝜒 → 𝜃))))
| | 7:: | ⊢ ( (𝜑 → (𝜓 → (𝜒
→ 𝜃))) ▶ (𝜑 → (𝜓 → (𝜒 → 𝜃))) )
| | 8:7,?: e1a 45458 | ⊢ ( (𝜑 → (𝜓 → (𝜒
→ 𝜃))) ▶ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) )
| | 9:8,?: e1a 45458 | ⊢ ( (𝜑 → (𝜓 → (𝜒
→ 𝜃))) ▶ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) )
| | 10:2,9,?: e01 45522 | ⊢ ( (𝜑 → (𝜓 → (𝜒
→ 𝜃))) ▶ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) )
| | 11:10: | ⊢ ((𝜑 → (𝜓 → (𝜒
→ 𝜃))) → ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃))
| | qed:6,11,?: e00 45598 | ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒)
→ 𝜃) ↔ (𝜑 → (𝜓 → (𝜒 → 𝜃))))
|
(Contributed by Alan Sare, 31-Dec-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ↔ (𝜑 → (𝜓 → (𝜒 → 𝜃)))) |
| |
| Theorem | 3impexpbicomVD 45687 |
Virtual deduction proof of 3impexpbicom 45311. 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 45525 | ⊢ ( ((𝜑 ∧ 𝜓 ∧ 𝜒)
→ (𝜃 ↔ 𝜏)) ▶ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜏 ↔ 𝜃)) )
| | 4:3,?: e1a 45458 | ⊢ ( ((𝜑 ∧ 𝜓 ∧ 𝜒)
→ (𝜃 ↔ 𝜏)) ▶ (𝜑 → (𝜓 → (𝜒 → (𝜏
↔ 𝜃)))) )
| | 5:4: | ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒)
→ (𝜃 ↔ 𝜏)) → (𝜑 → (𝜓 → (𝜒 → (𝜏
↔ 𝜃)))))
| | 6:: | ⊢ ( (𝜑 → (𝜓 → (𝜒
→ (𝜏 ↔ 𝜃)))) ▶ (𝜑 → (𝜓 → (𝜒 → (𝜏
↔ 𝜃)))) )
| | 7:6,?: e1a 45458 | ⊢ ( (𝜑 → (𝜓 → (𝜒
→ (𝜏 ↔ 𝜃)))) ▶ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜏
↔ 𝜃)) )
| | 8:7,2,?: e10 45525 | ⊢ ( (𝜑 → (𝜓 → (𝜒
→ (𝜏 ↔ 𝜃)))) ▶ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃
↔ 𝜏)) )
| | 9:8: | ⊢ ((𝜑 → (𝜓 → (𝜒
→ (𝜏 ↔ 𝜃)))) → ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃
↔ 𝜏)))
| | qed:5,9,?: e00 45598 | ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒)
→ (𝜃 ↔ 𝜏)) ↔ (𝜑 → (𝜓 → (𝜒 → (𝜏
↔ 𝜃)))))
|
(Contributed by Alan Sare, 31-Dec-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)) ↔ (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃))))) |
| |
| Theorem | 3impexpbicomiVD 45688 |
Virtual deduction proof of 3impexpbicomi 45312. 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 45602 | ⊢ (𝜑 → (𝜓 → (𝜒
→ (𝜏 ↔ 𝜃))))
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃)))) |
| |
| Theorem | sbcoreleleqVD 45689* |
Virtual deduction proof of sbcoreleleq 45366. 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 45458 | ⊢ ( 𝐴 ∈ 𝐵 ▶ ([𝐴 / 𝑦]𝑥 ∈
𝑦 ↔ 𝑥 ∈ 𝐴) )
| | 3:1,?: e1a 45458 | ⊢ ( 𝐴 ∈ 𝐵 ▶ ([𝐴 / 𝑦]𝑦 ∈
𝑥 ↔ 𝐴 ∈ 𝑥) )
| | 4:1,?: e1a 45458 | ⊢ ( 𝐴 ∈ 𝐵 ▶ ([𝐴 / 𝑦]𝑥 =
𝑦 ↔ 𝑥 = 𝐴) )
| | 5:2,3,4,?: e111 45505 | ⊢ ( 𝐴 ∈ 𝐵 ▶ ((𝑥 ∈ 𝐴
∨ 𝐴 ∈ 𝑥 ∨ 𝑥 = 𝐴) ↔ ([𝐴 / 𝑦]𝑥 ∈ 𝑦 ∨ [𝐴 / 𝑦]𝑦 ∈ 𝑥
∨ [𝐴 / 𝑦]𝑥 = 𝑦)) )
| | 6:1,?: e1a 45458 | ⊢ ( 𝐴 ∈ 𝐵
▶ ([𝐴 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ↔ ([𝐴 / 𝑦]𝑥
∈ 𝑦 ∨ [𝐴 / 𝑦]𝑦 ∈ 𝑥 ∨ [𝐴 / 𝑦]𝑥 = 𝑦)) )
| | 7:5,6: e11 45519 | ⊢ ( 𝐴 ∈ 𝐵 ▶ ([𝐴 / 𝑦](𝑥
∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ↔ (𝑥 ∈ 𝐴 ∨ 𝐴 ∈ 𝑥 ∨ 𝑥 = 𝐴)) )
| | qed:7: | ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑦](𝑥 ∈ 𝑦
∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ↔ (𝑥 ∈ 𝐴 ∨ 𝐴 ∈ 𝑥 ∨ 𝑥 = 𝐴)))
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
| ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ↔ (𝑥 ∈ 𝐴 ∨ 𝐴 ∈ 𝑥 ∨ 𝑥 = 𝐴))) |
| |
| Theorem | hbra2VD 45690* |
Virtual deduction proof of nfra2 3363. 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 45598 | ⊢ (∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐵𝜑 →
∀𝑦∀𝑦 ∈ 𝐵∀𝑥 ∈ 𝐴𝜑)
| | 4:2: | ⊢ ∀𝑦(∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐵𝜑 ↔
∀𝑦 ∈ 𝐵∀𝑥 ∈ 𝐴𝜑)
| | 5:4,?: e0a 45602 | ⊢ (∀𝑦∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐵𝜑 ↔
∀𝑦∀𝑦 ∈ 𝐵∀𝑥 ∈ 𝐴𝜑)
| | qed:3,5,?: e00 45598 | ⊢ (∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐵𝜑 →
∀𝑦∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐵𝜑)
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
| ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → ∀𝑦∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑) |
| |
| Theorem | tratrbVD 45691* |
Virtual deduction proof of tratrb 45367. 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 45458 | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) ▶ Tr 𝐴 )
| | 3:1,?: e1a 45458 | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)
▶ ∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) )
| | 4:1,?: e1a 45458 | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) ▶ 𝐵 ∈ 𝐴 )
| | 5:: | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦
∧ 𝑦 ∈ 𝐵) ▶ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) )
| | 6:5,?: e2 45462 | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦
∧ 𝑦 ∈ 𝐵) ▶ 𝑥 ∈ 𝑦 )
| | 7:5,?: e2 45462 | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦
∧ 𝑦 ∈ 𝐵) ▶ 𝑦 ∈ 𝐵 )
| | 8:2,7,4,?: e121 45487 | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦
∧ 𝑦 ∈ 𝐵) ▶ 𝑦 ∈ 𝐴 )
| | 9:2,6,8,?: e122 45484 | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦
∧ 𝑦 ∈ 𝐵) ▶ 𝑥 ∈ 𝐴 )
| | 10:: | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦
∧ 𝑦 ∈ 𝐵), 𝐵 ∈ 𝑥 ▶ 𝐵 ∈ 𝑥 )
| | 11:6,7,10,?: e223 45466 | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦
∧ 𝑦 ∈ 𝐵), 𝐵 ∈ 𝑥 ▶ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ∧ 𝐵 ∈ 𝑥) )
| | 12:11: | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦
∧ 𝑦 ∈ 𝐵) ▶ (𝐵 ∈ 𝑥 → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ∧ 𝐵 ∈ 𝑥)) )
| | 13:: | ⊢ ¬ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵
∧ 𝐵 ∈ 𝑥)
| | 14:12,13,?: e20 45557 | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦
∧ 𝑦 ∈ 𝐵) ▶ ¬ 𝐵 ∈ 𝑥 )
| | 15:: | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦
∧ 𝑦 ∈ 𝐵), 𝑥 = 𝐵 ▶ 𝑥 = 𝐵 )
| | 16:7,15,?: e23 45585 | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦
∧ 𝑦 ∈ 𝐵), 𝑥 = 𝐵 ▶ 𝑦 ∈ 𝑥 )
| | 17:6,16,?: e23 45585 | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦
∧ 𝑦 ∈ 𝐵), 𝑥 = 𝐵 ▶ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) )
| | 18:17: | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦
∧ 𝑦 ∈ 𝐵) ▶ (𝑥 = 𝐵 → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)) )
| | 19:: | ⊢ ¬ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)
| | 20:18,19,?: e20 45557 | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦
∧ 𝑦 ∈ 𝐵) ▶ ¬ 𝑥 = 𝐵 )
| | 21:3,?: e1a 45458 | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) ▶ ∀𝑦 ∈ 𝐴
∀𝑥 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) )
| | 22:21,9,4,?: e121 45487 | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦
∧ 𝑦 ∈ 𝐵) ▶ [𝑥 / 𝑥][𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥
∨ 𝑥 = 𝑦) )
| | 23:22,?: e2 45462 | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦
∧ 𝑦 ∈ 𝐵) ▶ [𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) )
| | 24:4,23,?: e12 45554 | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦
∧ 𝑦 ∈ 𝐵) ▶ (𝑥 ∈ 𝐵 ∨ 𝐵 ∈ 𝑥 ∨ 𝑥 = 𝐵) )
| | 25:14,20,24,?: e222 45467 | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦
∧ 𝑦 ∈ 𝐵) ▶ 𝑥 ∈ 𝐵 )
| | 26:25: | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) ▶ ((𝑥 ∈ 𝑦
∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐵) )
| | 27:: | ⊢ (∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦
∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) → ∀𝑦∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨
𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
| | 28:27,?: e0a 45602 | ⊢ ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)
→ ∀𝑦(Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥
∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴))
| | 29:28,26: | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)
▶ ∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐵) )
| | 30:: | ⊢ (∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦
∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) → ∀𝑥∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦
∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
| | 31:30,?: e0a 45602 | ⊢ ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) → ∀𝑥(Tr 𝐴
∧ ∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴))
| | 32:31,29: | ⊢ ( (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴
∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) ▶ ∀𝑥
∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐵) )
| | 33:32,?: e1a 45458 | ⊢ ( (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 45692 |
Virtual deduction proof of al2im 1847. 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 45458 | ⊢ ( ∀𝑥(𝜑 → (𝜓 → 𝜒))
▶ (∀𝑥𝜑 → ∀𝑥(𝜓 → 𝜒)) )
| | 3:: | ⊢ (∀𝑥(𝜓 → 𝜒) → (∀𝑥𝜓
→ ∀𝑥𝜒))
| | 4:2,3,?: e10 45525 | ⊢ ( ∀𝑥(𝜑 → (𝜓 → 𝜒))
▶ (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)) )
| | qed:4: | ⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒))
→ (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)))
|
(Contributed by Alan Sare, 31-Dec-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))) |
| |
| Theorem | syl5impVD 45693 |
Virtual deduction proof of syl5imp 45343. 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 45458 | ⊢ ( (𝜑 → (𝜓 → 𝜒)) ▶ (𝜓
→ (𝜑 → 𝜒)) )
| | 3:: | ⊢ ( (𝜑 → (𝜓 → 𝜒)) , (𝜃
→ 𝜓) ▶ (𝜃 → 𝜓) )
| | 4:3,2,?: e21 45560 | ⊢ ( (𝜑 → (𝜓 → 𝜒)) , (𝜃
→ 𝜓) ▶ (𝜃 → (𝜑 → 𝜒)) )
| | 5:4,?: e2 45462 | ⊢ ( (𝜑 → (𝜓 → 𝜒)) , (𝜃
→ 𝜓) ▶ (𝜑 → (𝜃 → 𝜒)) )
| | 6:5: | ⊢ ( (𝜑 → (𝜓 → 𝜒)) ▶ ((𝜃
→ 𝜓) → (𝜑 → (𝜃 → 𝜒))) )
| | qed:6: | ⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜃
→ 𝜓) → (𝜑 → (𝜃 → 𝜒))))
|
(Contributed by Alan Sare, 31-Dec-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| ⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜃 → 𝜓) → (𝜑 → (𝜃 → 𝜒)))) |
| |
| Theorem | idiVD 45694 |
Virtual deduction proof of idiALT 45309. 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 45602 | ⊢ 𝜑
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
| ⊢ 𝜑 ⇒ ⊢ 𝜑 |
| |
| Theorem | ancomstVD 45695 |
Closed form of ancoms 464. 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 45602 | ⊢ (((𝜑 ∧ 𝜓) → 𝜒) ↔ ((𝜓
∧ 𝜑) → 𝜒))
|
The proof of ancomst 470 is derived automatically from it.
(Contributed by
Alan Sare, 25-Dec-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
| ⊢ (((𝜑 ∧ 𝜓) → 𝜒) ↔ ((𝜓 ∧ 𝜑) → 𝜒)) |
| |
| Theorem | ssralv2VD 45696* |
Quantification restricted to a subclass for two quantifiers. ssralv 4003
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 45362 is ssralv2VD 45696 without
virtual deductions and was automatically derived from ssralv2VD 45696.
| 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 45697 |
An element of an ordinal class is ordinal. Proposition 7.6 of
[TakeutiZaring] p. 36. This is an alternate proof of ordelord 6383 using
the Axiom of Regularity indirectly through dford2 9603. 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 45368 is ordelordALTVD 45697
without virtual deductions and was automatically derived from
ordelordALTVD 45697 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 45698 |
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 4109 is equncomVD 45698 without
virtual deductions and was automatically derived from equncomVD 45698.
| 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 45699 |
Inference form of equncom 4109. 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 4110 is equncomiVD 45699 without
virtual deductions and was automatically derived from equncomiVD 45699.
| h1:: | ⊢ 𝐴 = (𝐵 ∪ 𝐶)
| | qed:1: | ⊢ 𝐴 = (𝐶 ∪ 𝐵)
|
(Contributed by Alan Sare, 18-Feb-2012.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
| ⊢ 𝐴 = (𝐵 ∪ 𝐶) ⇒ ⊢ 𝐴 = (𝐶 ∪ 𝐵) |
| |
| Theorem | sucidALTVD 45700 |
A set belongs to its successor. Alternate proof of sucid 6446.
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 45701 is sucidALTVD 45700
without virtual deductions and was automatically derived from
sucidALTVD 45700. 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 6367, 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 9603.
| 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 𝐴 |
Home
Hilbert Space Explorer
Users' Mathboxes