Home | Metamath
Proof Explorer Theorem List (p. 378 of 424) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description | ||||||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Statement | ||||||||||||||||||||||||||||||||
Definition | df-ptdf 37701* | Define the predicate PtDf, which is a utility definition used to shorten definitions and simplify proofs. (Contributed by Andrew Salmon, 15-Jul-2012.) | ||||||||||||||||||||||||||||||
⊢ PtDf(𝐴, 𝐵) = (𝑥 ∈ ℝ ↦ (((𝑥.𝑣(𝐵-𝑟𝐴)) +𝑣 𝐴) “ {1, 2, 3})) | ||||||||||||||||||||||||||||||||
Definition | df-rr3 37702 | Define the set of all points RR3. We define each point 𝐴 as a function to allow the use of vector addition and subtraction as well as scalar multiplication in our proofs. (Contributed by Andrew Salmon, 15-Jul-2012.) | ||||||||||||||||||||||||||||||
⊢ RR3 = (ℝ ↑𝑚 {1, 2, 3}) | ||||||||||||||||||||||||||||||||
Definition | df-line3 37703* | Define the set of all lines. A line is an infinite subset of RR3 that satisfies a PtDf property. (Contributed by Andrew Salmon, 15-Jul-2012.) | ||||||||||||||||||||||||||||||
⊢ line3 = {𝑥 ∈ 𝒫 RR3 ∣ (2𝑜 ≼ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑧 ≠ 𝑦 → ran PtDf(𝑦, 𝑧) = 𝑥))} | ||||||||||||||||||||||||||||||||
We are sad to report the passing of long-time contributor Alan Sare (Nov. 9, 1954 - Mar. 23, 2019). Alan's first contribution to Metamath was a shorter proof for tfrlem8 7367 in 2008. He developed a tool called "completeusersproof" that assists developing proofs using his "virtual deduction" method: http://us.metamath.org/other.html#completeusersproof. His virtual deduction method is explained in the comment for wvd1 37806. Below are some excerpts from his first emails to NM in 2007: ...I have been interested in proving set theory theorems for many years for mental exercise. I enjoy it. I have used a book by Martin Zuckerman. It is informal. I am interested in completely and perfectly proving theorems. Mr. Zuckerman leaves out most of the steps of a proof, of course, like most authors do, as you have noted. A complete proof for higher theorems would require a volume of writing similar to the metamath documents. So I am frustrated when I am not capable of constructing a proof and Zuckerman leaves out steps I do not understand. I could search for the steps in other texts, but I don't do that too much. Metamath may be the answer for me.... ...If we go beyond mathematics, I believe that it is possible to write down all human knowledge in a way similar to the way you have explicated large areas of mathematics. Of course, that would be a much, much more difficult job. For example, it is possible to take a hard science like physics construct axioms based on experimental results and to cast all of physics into a collection of axioms and theorems. Maybe his has already been attempted, although I am not familiar with it. When one then moves on to the soft sciences such as social science, this job gets much more difficult. The key is: All human thought consists of logical operations on abstract objects. Usually, these logical operations are done informally. There is no reason why one cannot take any subject and explicate it and take it down to the indivisible postulates in a formal rigorous way.... ...When I read a math book or an engineering book I come across something I don't understand and I am compelled to understand it. But, often it is hopeless. I don't have the time. Or, I would have to read the same thing by multiple authors in the hope that different authors would give parts of the working proof that others have omitted. It is very inefficient. Because I have always been inclined to "get to the bottom" for a 100% fully understood proof.... | ||||||||||||||||||||||||||||||||
Theorem | idiALT 37704 | Placeholder for idi 2. Though unnecessary, this theorem is sometimes used in proofs in this mathbox for pedagogical purposes. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ 𝜑 ⇒ ⊢ 𝜑 | ||||||||||||||||||||||||||||||||
Theorem | exbir 37705 | Exportation implication also converting the consequent from a biconditional to an implication. Derived automatically from exbirVD 38110. (Contributed by Alan Sare, 31-Dec-2011.) | ||||||||||||||||||||||||||||||
⊢ (((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) → (𝜑 → (𝜓 → (𝜃 → 𝜒)))) | ||||||||||||||||||||||||||||||||
Theorem | 3impexpbicom 37706 | Version of 3impexp 1281 where in addition the consequent is commuted. (Contributed by Alan Sare, 31-Dec-2011.) | ||||||||||||||||||||||||||||||
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)) ↔ (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃))))) | ||||||||||||||||||||||||||||||||
Theorem | 3impexpbicomi 37707 | Inference associated with 3impexpbicom 37706. Derived automatically from 3impexpbicomiVD 38115. (Contributed by Alan Sare, 31-Dec-2011.) | ||||||||||||||||||||||||||||||
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃)))) | ||||||||||||||||||||||||||||||||
Theorem | bi1imp 37708 | Importation inference similar to imp 444, except the outermost implication of the hypothesis is a biconditional. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 ↔ (𝜓 → 𝜒)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||||||||||||||||||||||||||||||||
Theorem | bi2imp 37709 | Importation inference similar to imp 444, except both implications of the hypothesis are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 ↔ (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||||||||||||||||||||||||||||||||
Theorem | bi3impb 37710 | Similar to 3impb 1252 with implication in hypothesis replaced by biconditional. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||||||||||||||||||||||||||||||||
Theorem | bi3impa 37711 | Similar to 3impa 1251 with implication in hypothesis replaced by biconditional. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||||||||||||||||||||||||||||||||
Theorem | bi23impib 37712 | 3impib 1254 with the inner implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ 𝜃)) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||||||||||||||||||||||||||||||||
Theorem | bi13impib 37713 | 3impib 1254 with the outer implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 ↔ ((𝜓 ∧ 𝜒) → 𝜃)) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||||||||||||||||||||||||||||||||
Theorem | bi123impib 37714 | 3impib 1254 with the implications of the hypothesis biconditionals. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 ↔ ((𝜓 ∧ 𝜒) ↔ 𝜃)) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||||||||||||||||||||||||||||||||
Theorem | bi13impia 37715 | 3impia 1253 with the outer implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
⊢ ((𝜑 ∧ 𝜓) ↔ (𝜒 → 𝜃)) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||||||||||||||||||||||||||||||||
Theorem | bi123impia 37716 | 3impia 1253 with the implications of the hypothesis biconditionals. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
⊢ ((𝜑 ∧ 𝜓) ↔ (𝜒 ↔ 𝜃)) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||||||||||||||||||||||||||||||||
Theorem | bi33imp12 37717 | 3imp 1249 with innermost implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||||||||||||||||||||||||||||||||
Theorem | bi23imp13 37718 | 3imp 1249 with middle implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 → (𝜓 ↔ (𝜒 → 𝜃))) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||||||||||||||||||||||||||||||||
Theorem | bi13imp23 37719 | 3imp 1249 with outermost implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 ↔ (𝜓 → (𝜒 → 𝜃))) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||||||||||||||||||||||||||||||||
Theorem | bi13imp2 37720 | Similar to 3imp 1249 except the outermost and innermost implications are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 ↔ (𝜓 → (𝜒 ↔ 𝜃))) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||||||||||||||||||||||||||||||||
Theorem | bi12imp3 37721 | Similar to 3imp 1249 except all but innermost implication are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 ↔ (𝜓 ↔ (𝜒 → 𝜃))) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||||||||||||||||||||||||||||||||
Theorem | bi23imp1 37722 | Similar to 3imp 1249 except all but outermost implication are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 → (𝜓 ↔ (𝜒 ↔ 𝜃))) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||||||||||||||||||||||||||||||||
Theorem | bi123imp0 37723 | Similar to 3imp 1249 except all implications are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 ↔ (𝜓 ↔ (𝜒 ↔ 𝜃))) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||||||||||||||||||||||||||||||||
Theorem | 4animp1 37724 | A single hypothesis unification deduction with an assertion which is an implication with a 4-right-nested conjunction antecedent. (Contributed by Alan Sare, 30-May-2018.) | ||||||||||||||||||||||||||||||
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜏 ↔ 𝜃)) ⇒ ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) | ||||||||||||||||||||||||||||||||
Theorem | 4an31 37725 | A rearrangement of conjuncts for a 4-right-nested conjunction. (Contributed by Alan Sare, 30-May-2018.) | ||||||||||||||||||||||||||||||
⊢ ((((𝜒 ∧ 𝜓) ∧ 𝜑) ∧ 𝜃) → 𝜏) ⇒ ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) | ||||||||||||||||||||||||||||||||
Theorem | 4an4132 37726 | A rearrangement of conjuncts for a 4-right-nested conjunction. (Contributed by Alan Sare, 30-May-2018.) | ||||||||||||||||||||||||||||||
⊢ ((((𝜃 ∧ 𝜒) ∧ 𝜓) ∧ 𝜑) → 𝜏) ⇒ ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) | ||||||||||||||||||||||||||||||||
Theorem | expcomdg 37727 | Biconditional form of expcomd 453. (Contributed by Alan Sare, 22-Jul-2012.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ ((𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) ↔ (𝜑 → (𝜒 → (𝜓 → 𝜃)))) | ||||||||||||||||||||||||||||||||
Theorem | iidn3 37728 | idn3 37861 without virtual deduction connectives. Special theorem needed for the Virtual Deduction translation tool. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜒))) | ||||||||||||||||||||||||||||||||
Theorem | ee222 37729 | e222 37882 without virtual deduction connectives. Special theorem needed for the Virtual Deduction translation tool. (Contributed by Alan Sare, 7-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜓 → 𝜃)) & ⊢ (𝜑 → (𝜓 → 𝜏)) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜂)) | ||||||||||||||||||||||||||||||||
Theorem | ee3bir 37730 | Right-biconditional form of e3 37985 without virtual deduction connectives. Special theorem needed for the Virtual Deduction translation tool. (Contributed by Alan Sare, 22-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜏 ↔ 𝜃) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏))) | ||||||||||||||||||||||||||||||||
Theorem | ee13 37731 | e13 37996 without virtual deduction connectives. Special theorem needed for the Virtual Deduction translation tool. (Contributed by Alan Sare, 28-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏))) & ⊢ (𝜓 → (𝜏 → 𝜂)) ⇒ ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜂))) | ||||||||||||||||||||||||||||||||
Theorem | ee121 37732 | e121 37902 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → (𝜒 → 𝜃)) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜒 → 𝜂)) | ||||||||||||||||||||||||||||||||
Theorem | ee122 37733 | e122 37899 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → (𝜒 → 𝜃)) & ⊢ (𝜑 → (𝜒 → 𝜏)) & ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜒 → 𝜂)) | ||||||||||||||||||||||||||||||||
Theorem | ee333 37734 | e333 37981 without virtual deductions. (Contributed by Alan Sare, 17-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏))) & ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) & ⊢ (𝜃 → (𝜏 → (𝜂 → 𝜁))) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜁))) | ||||||||||||||||||||||||||||||||
Theorem | ee323 37735 | e323 38014 without virtual deductions. (Contributed by Alan Sare, 17-Apr-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜑 → (𝜓 → 𝜏)) & ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) & ⊢ (𝜃 → (𝜏 → (𝜂 → 𝜁))) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜁))) | ||||||||||||||||||||||||||||||||
Theorem | 3ornot23 37736 | If the second and third disjuncts of a true triple disjunction are false, then the first disjunct is true. Automatically derived from 3ornot23VD 38104. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ((𝜒 ∨ 𝜑 ∨ 𝜓) → 𝜒)) | ||||||||||||||||||||||||||||||||
Theorem | orbi1r 37737 | orbi1 738 with order of disjuncts reversed. Derived from orbi1rVD 38105. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓))) | ||||||||||||||||||||||||||||||||
Theorem | 3orbi123 37738 | pm4.39 911 with a 3-conjunct antecedent. This proof is 3orbi123VD 38107 automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂)) → ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ (𝜓 ∨ 𝜃 ∨ 𝜂))) | ||||||||||||||||||||||||||||||||
Theorem | syl5imp 37739 | Closed form of syl5 33. Derived automatically from syl5impVD 38121. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜃 → 𝜓) → (𝜑 → (𝜃 → 𝜒)))) | ||||||||||||||||||||||||||||||||
Theorem | impexpd 37740 |
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. After the
User's Proof was completed, it was minimized. The completed User's Proof
before minimization is not shown. (Contributed by Alan Sare,
18-Mar-2012.) (Proof modification is discouraged.)
(New usage is discouraged.)
| ||||||||||||||||||||||||||||||
⊢ ((𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) ↔ (𝜑 → (𝜓 → (𝜒 → 𝜃)))) | ||||||||||||||||||||||||||||||||
Theorem | com3rgbi 37741 |
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. The
completed Virtual Deduction Proof (not shown) was minimized. The
minimized proof is shown.
(Contributed by Alan Sare, 18-Mar-2012.)
(Proof modification is discouraged.) (New usage is discouraged.)
| ||||||||||||||||||||||||||||||
⊢ ((𝜑 → (𝜓 → (𝜒 → 𝜃))) ↔ (𝜒 → (𝜑 → (𝜓 → 𝜃)))) | ||||||||||||||||||||||||||||||||
Theorem | impexpdcom 37742 |
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. The
completed Virtual Deduction Proof (not shown) was minimized. The
minimized proof is shown. (Contributed by Alan Sare, 18-Mar-2012.)
(Proof modification is discouraged.) (New usage is discouraged.)
| ||||||||||||||||||||||||||||||
⊢ ((𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) ↔ (𝜓 → (𝜒 → (𝜑 → 𝜃)))) | ||||||||||||||||||||||||||||||||
Theorem | ee1111 37743 |
Non-virtual deduction form of e1111 37921. (Contributed by Alan Sare,
18-Mar-2012.)
(Proof modification is discouraged.) (New usage is discouraged.)
The following User's Proof is a Virtual Deduction proof
completed automatically by the tools program completeusersproof.cmd,
which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof
Assistant. The completed Virtual Deduction Proof (not shown) was
minimized. The minimized proof is shown.
| ||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))) ⇒ ⊢ (𝜑 → 𝜂) | ||||||||||||||||||||||||||||||||
Theorem | pm2.43bgbi 37744 |
Logical equivalence of a 2-left-nested implication and a 1-left-nested
implicated
when two antecedents of the former implication are identical.
(Contributed by Alan Sare, 18-Mar-2012.)
(Proof modification is discouraged.) (New usage is discouraged.)
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. The
completed Virtual
Deduction Proof (not shown) was minimized. The minimized proof is
shown.
| ||||||||||||||||||||||||||||||
⊢ ((𝜑 → (𝜓 → (𝜑 → 𝜒))) ↔ (𝜓 → (𝜑 → 𝜒))) | ||||||||||||||||||||||||||||||||
Theorem | pm2.43cbi 37745 |
Logical equivalence of a 3-left-nested implication and a 2-left-nested
implicated when two antecedents of the former implication are identical.
(Contributed by Alan Sare, 18-Mar-2012.)
(Proof modification is discouraged.) (New usage is discouraged.)
The following User's Proof is
a Virtual Deduction proof completed automatically by the tools program
completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm
Megill's Metamath Proof Assistant. The completed Virtual Deduction Proof
(not shown) was minimized. The minimized proof is shown.
| ||||||||||||||||||||||||||||||
⊢ ((𝜑 → (𝜓 → (𝜒 → (𝜑 → 𝜃)))) ↔ (𝜓 → (𝜒 → (𝜑 → 𝜃)))) | ||||||||||||||||||||||||||||||||
Theorem | ee233 37746 |
Non-virtual deduction form of e233 38013. (Contributed by Alan Sare,
18-Mar-2012.)
(Proof modification is discouraged.) (New usage is discouraged.)
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. The
completed Virtual
Deduction Proof (not shown) was minimized. The minimized proof is
shown.
| ||||||||||||||||||||||||||||||
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜏))) & ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜂))) & ⊢ (𝜒 → (𝜏 → (𝜂 → 𝜁))) ⇒ ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜁))) | ||||||||||||||||||||||||||||||||
Theorem | imbi13 37747 | Join three logical equivalences to form equivalence of implications. imbi13 37747 is imbi13VD 38132 without virtual deductions and was automatically derived from imbi13VD 38132 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ↔ 𝜃) → ((𝜏 ↔ 𝜂) → ((𝜑 → (𝜒 → 𝜏)) ↔ (𝜓 → (𝜃 → 𝜂)))))) | ||||||||||||||||||||||||||||||||
Theorem | ee33 37748 |
Non-virtual deduction form of e33 37982. (Contributed by Alan Sare,
18-Mar-2012.) (Proof modification is discouraged.)
(New usage is discouraged.)
The following User's Proof is a Virtual Deduction proof
completed automatically by the tools program completeusersproof.cmd,
which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof
Assistant. The completed Virtual Deduction Proof (not shown) was
minimized. The minimized proof is shown.
| ||||||||||||||||||||||||||||||
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏))) & ⊢ (𝜃 → (𝜏 → 𝜂)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) | ||||||||||||||||||||||||||||||||
Theorem | con5 37749 | Biconditional contraposition variation. This proof is con5VD 38158 automatically translated and minimized. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ ((𝜑 ↔ ¬ 𝜓) → (¬ 𝜑 → 𝜓)) | ||||||||||||||||||||||||||||||||
Theorem | con5i 37750 | Inference form of con5 37749. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 ↔ ¬ 𝜓) ⇒ ⊢ (¬ 𝜑 → 𝜓) | ||||||||||||||||||||||||||||||||
Theorem | exlimexi 37751 | Inference similar to Theorem 19.23 of [Margaris] p. 90. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (∃𝑥𝜑 → (𝜑 → 𝜓)) ⇒ ⊢ (∃𝑥𝜑 → 𝜓) | ||||||||||||||||||||||||||||||||
Theorem | sb5ALT 37752* | Equivalence for substitution. Alternate proof of sb5 2418. This proof is sb5ALTVD 38171 automatically translated and minimized. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | ||||||||||||||||||||||||||||||||
Theorem | eexinst01 37753 | exinst01 37871 without virtual deductions. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ ∃𝑥𝜓 & ⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜒 → ∀𝑥𝜒) ⇒ ⊢ (𝜑 → 𝜒) | ||||||||||||||||||||||||||||||||
Theorem | eexinst11 37754 | exinst11 37872 without virtual deductions. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 → ∃𝑥𝜓) & ⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜒 → ∀𝑥𝜒) ⇒ ⊢ (𝜑 → 𝜒) | ||||||||||||||||||||||||||||||||
Theorem | vk15.4j 37755 | Excercise 4j of Unit 15 of "Understanding Symbolic Logic", Fifth Edition (2008), by Virginia Klenk. This proof is the minimized Hilbert-style axiomatic version of the Fitch-style Natural Deduction proof found on page 442 of Klenk and was automatically derived from that proof. vk15.4j 37755 is vk15.4jVD 38172 automatically translated and minimized. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ ¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒)) & ⊢ (∀𝑥𝜒 → ¬ ∃𝑥(𝜃 ∧ 𝜏)) & ⊢ ¬ ∀𝑥(𝜏 → 𝜑) ⇒ ⊢ (¬ ∃𝑥 ¬ 𝜃 → ¬ ∀𝑥𝜓) | ||||||||||||||||||||||||||||||||
Theorem | notnotrALT 37756 | Converse of double negation. Alternate proof of notnotr 124. This proof is notnotrALTVD 38173 automatically translated and minimized. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (¬ ¬ 𝜑 → 𝜑) | ||||||||||||||||||||||||||||||||
Theorem | con3ALT2 37757 | Contraposition. Alternate proof of con3 148. This proof is con3ALTVD 38174 automatically translated and minimized. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ ((𝜑 → 𝜓) → (¬ 𝜓 → ¬ 𝜑)) | ||||||||||||||||||||||||||||||||
Theorem | ssralv2 37758* | Quantification restricted to a subclass for two quantifiers. ssralv 3629 for two quantifiers. The proof of ssralv2 37758 was automatically generated by minimizing the automatically translated proof of ssralv2VD 38124. The automatic translation is by the tools program translatewithout_overwriting.cmd. (Contributed by Alan Sare, 18-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝜑)) | ||||||||||||||||||||||||||||||||
Theorem | sbc3or 37759 | sbcor 3446 with a 3-disjuncts. This proof is sbc3orgVD 38108 automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.) (Revised by NM, 24-Aug-2018.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ ([𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓 ∨ [𝐴 / 𝑥]𝜒)) | ||||||||||||||||||||||||||||||||
Theorem | sbcangOLD 37760 | Distribution of class substitution over conjunction. (Contributed by NM, 21-May-2004.) Obsolete as of 17-Aug-2018. Use sbcan 3445 instead. (New usage is discouraged.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓))) | ||||||||||||||||||||||||||||||||
Theorem | sbcorgOLD 37761 | Distribution of class substitution over disjunction. (Contributed by NM, 21-May-2004.) Obsolete as of 17-Aug-2018. Use sbcor 3446 instead. (New usage is discouraged.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓))) | ||||||||||||||||||||||||||||||||
Theorem | sbcbiiOLD 37762 | Formula-building inference rule for class substitution. (Contributed by NM, 11-Nov-2005.) Obsolete as of 17-Aug-2018. Use sbcbii 3458 instead. (New usage is discouraged.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)) | ||||||||||||||||||||||||||||||||
Theorem | sbc3orgOLD 37763 | sbcorgOLD 37761 with a 3-disjuncts. This proof is sbc3orgVD 38108 automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓 ∨ [𝐴 / 𝑥]𝜒))) | ||||||||||||||||||||||||||||||||
Theorem | alrim3con13v 37764* | Closed form of alrimi 2069 with 2 additional conjuncts having no occurrences of the quantifying variable. This proof is 19.21a3con13vVD 38109 automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ ((𝜑 → ∀𝑥𝜑) → ((𝜓 ∧ 𝜑 ∧ 𝜒) → ∀𝑥(𝜓 ∧ 𝜑 ∧ 𝜒))) | ||||||||||||||||||||||||||||||||
Theorem | rspsbc2 37765* | rspsbc 3484 with two quantifying variables. This proof is rspsbc2VD 38112 automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (𝐴 ∈ 𝐵 → (𝐶 ∈ 𝐷 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑 → [𝐶 / 𝑦][𝐴 / 𝑥]𝜑))) | ||||||||||||||||||||||||||||||||
Theorem | sbcoreleleq 37766* | Substitution of a setvar variable for another setvar variable in a 3-conjunct formula. Derived automatically from sbcoreleleqVD 38117. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ↔ (𝑥 ∈ 𝐴 ∨ 𝐴 ∈ 𝑥 ∨ 𝑥 = 𝐴))) | ||||||||||||||||||||||||||||||||
Theorem | tratrb 37767* | If a class is transitive and any two distinct elements of the class are E-comparable, then every element of that class is transitive. Derived automatically from tratrbVD 38119. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) → Tr 𝐵) | ||||||||||||||||||||||||||||||||
Theorem | ordelordALT 37768 | An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36. This is an alternate proof of ordelord 5662 using the Axiom of Regularity indirectly through dford2 8400. 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. ordelordALT 37768 is ordelordALTVD 38125 without virtual deductions and was automatically derived from ordelordALTVD 38125 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐵) | ||||||||||||||||||||||||||||||||
Theorem | sbcim2g 37769 | Distribution of class substitution over a left-nested implication. Similar to sbcimg 3444. sbcim2g 37769 is sbcim2gVD 38133 without virtual deductions and was automatically derived from sbcim2gVD 38133 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)))) | ||||||||||||||||||||||||||||||||
Theorem | sbcbi 37770 | Implication form of sbcbiiOLD 37762. sbcbi 37770 is sbcbiVD 38134 without virtual deductions and was automatically derived from sbcbiVD 38134 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝜑 ↔ 𝜓) → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓))) | ||||||||||||||||||||||||||||||||
Theorem | trsbc 37771* | Formula-building inference rule for class substitution, substituting a class variable for the setvar variable of the transitivity predicate. trsbc 37771 is trsbcVD 38135 without virtual deductions and was automatically derived from trsbcVD 38135 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]Tr 𝑥 ↔ Tr 𝐴)) | ||||||||||||||||||||||||||||||||
Theorem | truniALT 37772* | The union of a class of transitive sets is transitive. Alternate proof of truni 4695. truniALT 37772 is truniALTVD 38136 without virtual deductions and was automatically derived from truniALTVD 38136 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → Tr ∪ 𝐴) | ||||||||||||||||||||||||||||||||
Theorem | sbcalgOLD 37773* | Move universal quantifier in and out of class substitution. (Contributed by NM, 16-Jan-2004.) Obsolete as of 17-Aug-2018. Use sbcal 3452 instead. (New usage is discouraged.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝐴 / 𝑦]𝜑)) | ||||||||||||||||||||||||||||||||
Theorem | sbcexgOLD 37774* | Move existential quantifier in and out of class substitution. (Contributed by NM, 21-May-2004.) Obsolete as of 17-Aug-2018. Use sbcex 3412 instead. (New usage is discouraged.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑦]∃𝑥𝜑 ↔ ∃𝑥[𝐴 / 𝑦]𝜑)) | ||||||||||||||||||||||||||||||||
Theorem | sbcel12gOLD 37775 | Distribute proper substitution through a membership relation. (Contributed by NM, 10-Nov-2005.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) Obsolete as of 18-Aug-2018. Use sbcel12 3935 instead. (New usage is discouraged.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 ∈ 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 ∈ ⦋𝐴 / 𝑥⦌𝐶)) | ||||||||||||||||||||||||||||||||
Theorem | sbcel2gOLD 37776* | Move proper substitution in and out of a membership relation. (Contributed by NM, 14-Nov-2005.) Obsolete as of 18-Aug-2018. Use sbcel2 3941 instead. (New usage is discouraged.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 ∈ 𝐶 ↔ 𝐵 ∈ ⦋𝐴 / 𝑥⦌𝐶)) | ||||||||||||||||||||||||||||||||
Theorem | sbcssOLD 37777 | Distribute proper substitution through a subclass relation. This theorem was automatically derived from sbcssgVD 38141. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]𝐶 ⊆ 𝐷 ↔ ⦋𝐴 / 𝑥⦌𝐶 ⊆ ⦋𝐴 / 𝑥⦌𝐷)) | ||||||||||||||||||||||||||||||||
Theorem | onfrALTlem5 37778* | Lemma for onfrALT 37785. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ ([(𝑎 ∩ 𝑥) / 𝑏]((𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅) ↔ (((𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) ∧ (𝑎 ∩ 𝑥) ≠ ∅) → ∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)) | ||||||||||||||||||||||||||||||||
Theorem | onfrALTlem4 37779* | Lemma for onfrALT 37785. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅) ↔ (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅)) | ||||||||||||||||||||||||||||||||
Theorem | onfrALTlem3 37780* | Lemma for onfrALT 37785. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ ((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → ((𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅) → ∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)) | ||||||||||||||||||||||||||||||||
Theorem | ggen31 37781* | gen31 37867 without virtual deductions. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → ∀𝑥𝜃))) | ||||||||||||||||||||||||||||||||
Theorem | onfrALTlem2 37782* | Lemma for onfrALT 37785. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ ((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → ((𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅) → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅)) | ||||||||||||||||||||||||||||||||
Theorem | cbvexsv 37783* | A theorem pertaining to the substitution for an existentially quantified variable when the substituted variable does not occur in the quantified wff. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (∃𝑥𝜑 ↔ ∃𝑦[𝑦 / 𝑥]𝜑) | ||||||||||||||||||||||||||||||||
Theorem | onfrALTlem1 37784* | Lemma for onfrALT 37785. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ ((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → ((𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅) → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅)) | ||||||||||||||||||||||||||||||||
Theorem | onfrALT 37785 | The epsilon relation is foundational on the class of ordinal numbers. onfrALT 37785 is an alternate proof of onfr 5680. onfrALTVD 38149 is the Virtual Deduction proof from which onfrALT 37785 is derived. The Virtual Deduction proof mirrors the working proof of onfr 5680 which is the main part of the proof of Theorem 7.12 of the first edition of TakeutiZaring. The proof of the corresponding Proposition 7.12 of [TakeutiZaring] p. 38 (second edition) does not contain the working proof equivalent of onfrALTVD 38149. This theorem does not rely on the Axiom of Regularity. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ E Fr On | ||||||||||||||||||||||||||||||||
Theorem | csbeq2gOLD 37786 | Formula-building implication rule for class substitution. Closed form of csbeq2i 3945. csbeq2gOLD 37786 is derived from the virtual deduction proof csbeq2gVD 38150. (Contributed by Alan Sare, 10-Nov-2012.) Obsolete version of csbeq2 3503 as of 11-Oct-2018. (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (𝐴 ∈ 𝑉 → (∀𝑥 𝐵 = 𝐶 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)) | ||||||||||||||||||||||||||||||||
Theorem | 19.41rg 37787 | Closed form of right-to-left implication of 19.41 2090, Theorem 19.41 of [Margaris] p. 90. Derived from 19.41rgVD 38160. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (∀𝑥(𝜓 → ∀𝑥𝜓) → ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓))) | ||||||||||||||||||||||||||||||||
Theorem | opelopab4 37788* | Ordered pair membership in a class abstraction of pairs. Compare to elopab 4908. (Contributed by Alan Sare, 8-Feb-2014.) (Revised by Mario Carneiro, 6-May-2015.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (〈𝑢, 𝑣〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)) | ||||||||||||||||||||||||||||||||
Theorem | 2pm13.193 37789 | pm13.193 37634 for two variables. pm13.193 37634 is Theorem *13.193 in [WhiteheadRussell] p. 179. Derived from 2pm13.193VD 38161. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)) | ||||||||||||||||||||||||||||||||
Theorem | hbntal 37790 | A closed form of hbn 2131. hbnt 2129 is another closed form of hbn 2131. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑥(¬ 𝜑 → ∀𝑥 ¬ 𝜑)) | ||||||||||||||||||||||||||||||||
Theorem | hbimpg 37791 | A closed form of hbim 2112. Derived from hbimpgVD 38162. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ ((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → ∀𝑥((𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓))) | ||||||||||||||||||||||||||||||||
Theorem | hbalg 37792 | Closed form of hbal 2023. Derived from hbalgVD 38163. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑦(∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)) | ||||||||||||||||||||||||||||||||
Theorem | hbexg 37793 | Closed form of nfex 2140. Derived from hbexgVD 38164. (Contributed by Alan Sare, 8-Feb-2014.) (Revised by Mario Carneiro, 12-Dec-2016.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑥∀𝑦(∃𝑦𝜑 → ∀𝑥∃𝑦𝜑)) | ||||||||||||||||||||||||||||||||
Theorem | ax6e2eq 37794* | Alternate form of ax6e 2238 for non-distinct 𝑥, 𝑦 and 𝑢 = 𝑣. ax6e2eq 37794 is derived from ax6e2eqVD 38165. (Contributed by Alan Sare, 25-Mar-2014.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (∀𝑥 𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))) | ||||||||||||||||||||||||||||||||
Theorem | ax6e2nd 37795* | If at least two sets exist (dtru 4783) , then the same is true expressed in an alternate form similar to the form of ax6e 2238. ax6e2nd 37795 is derived from ax6e2ndVD 38166. (Contributed by Alan Sare, 25-Mar-2014.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) | ||||||||||||||||||||||||||||||||
Theorem | ax6e2ndeq 37796* | "At least two sets exist" expressed in the form of dtru 4783 is logically equivalent to the same expressed in a form similar to ax6e 2238 if dtru 4783 is false implies 𝑢 = 𝑣. ax6e2ndeq 37796 is derived from ax6e2ndeqVD 38167. (Contributed by Alan Sare, 25-Mar-2014.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣) ↔ ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) | ||||||||||||||||||||||||||||||||
Theorem | 2sb5nd 37797* | Equivalence for double substitution 2sb5 2431 without distinct 𝑥, 𝑦 requirement. 2sb5nd 37797 is derived from 2sb5ndVD 38168. (Contributed by Alan Sare, 30-Apr-2014.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑))) | ||||||||||||||||||||||||||||||||
Theorem | 2uasbanh 37798* | Distribute the unabbreviated form of proper substitution in and out of a conjunction. 2uasbanh 37798 is derived from 2uasbanhVD 38169. (Contributed by Alan Sare, 31-May-2014.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (𝜒 ↔ (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓))) ⇒ ⊢ (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓)) ↔ (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓))) | ||||||||||||||||||||||||||||||||
Theorem | 2uasban 37799* | Distribute the unabbreviated form of proper substitution in and out of a conjunction. (Contributed by Alan Sare, 31-May-2014.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓)) ↔ (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓))) | ||||||||||||||||||||||||||||||||
Theorem | e2ebind 37800 | Absorption of an existential quantifier of a double existential quantifier of non-distinct variables. e2ebind 37800 is derived from e2ebindVD 38170. (Contributed by Alan Sare, 27-Nov-2014.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
⊢ (∀𝑥 𝑥 = 𝑦 → (∃𝑥∃𝑦𝜑 ↔ ∃𝑦𝜑)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |