Home | Metamath
Proof Explorer Theorem List (p. 301 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-afs 30001* | The outer five segment configuration is an abbreviation for the conditions of the Five Segment Axiom (axtg5seg 25164). See df-ofs 31260. Definition 2.10 of [Schwabhauser] p. 28. (Contributed by Scott Fenton, 21-Sep-2013.) (Modified by Thierry Arnoux, 15-Mar-2019.) |
⊢ AFS = (𝑔 ∈ TarskiG ↦ {〈𝑒, 𝑓〉 ∣ [(Base‘𝑔) / 𝑝][(dist‘𝑔) / ℎ][(Itv‘𝑔) / 𝑖]∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 ∃𝑐 ∈ 𝑝 ∃𝑑 ∈ 𝑝 ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 ∃𝑤 ∈ 𝑝 (𝑒 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑓 = 〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎ℎ𝑏) = (𝑥ℎ𝑦) ∧ (𝑏ℎ𝑐) = (𝑦ℎ𝑧)) ∧ ((𝑎ℎ𝑑) = (𝑥ℎ𝑤) ∧ (𝑏ℎ𝑑) = (𝑦ℎ𝑤))))}) | ||
Theorem | afsval 30002* | Value of the AFS relation for a given geometry structure. (Contributed by Thierry Arnoux, 20-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) ⇒ ⊢ (𝜑 → (AFS‘𝐺) = {〈𝑒, 𝑓〉 ∣ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ∃𝑤 ∈ 𝑃 (𝑒 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑓 = 〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 − 𝑏) = (𝑥 − 𝑦) ∧ (𝑏 − 𝑐) = (𝑦 − 𝑧)) ∧ ((𝑎 − 𝑑) = (𝑥 − 𝑤) ∧ (𝑏 − 𝑑) = (𝑦 − 𝑤))))}) | ||
Theorem | brafs 30003 | Binary relationship form of the outer five segment predicate. (Contributed by Scott Fenton, 21-Sep-2013.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝑂 = (AFS‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑊 ∈ 𝑃) ⇒ ⊢ (𝜑 → (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉𝑂〈〈𝑋, 𝑌〉, 〈𝑍, 𝑊〉〉 ↔ ((𝐵 ∈ (𝐴𝐼𝐶) ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ ((𝐴 − 𝐵) = (𝑋 − 𝑌) ∧ (𝐵 − 𝐶) = (𝑌 − 𝑍)) ∧ ((𝐴 − 𝐷) = (𝑋 − 𝑊) ∧ (𝐵 − 𝐷) = (𝑌 − 𝑊))))) | ||
Theorem | tg5segofs 30004 | Rephrase axtg5seg 25164 using the outer five segment predicate. Theorem 2.10 of [Schwabhauser] p. 28. (Contributed by Thierry Arnoux, 23-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ 𝑂 = (AFS‘𝐺) & ⊢ (𝜑 → 𝐻 ∈ 𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑃) & ⊢ (𝜑 → 〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉𝑂〈〈𝐸, 𝐹〉, 〈𝐻, 𝐼〉〉) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → (𝐶 − 𝐷) = (𝐻 − 𝐼)) | ||
Note: On 4-Sep-2016 and after, 745 unused theorems were deleted from this mathbox, and 359 theorems used only once or twice were merged into their referencing theorems. The originals can be recovered from set.mm versions prior to this date. | ||
Syntax | w-bnj17 30005 | Extend wff notation with the 4-way conjunction. (New usage is discouraged.) |
wff (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) | ||
Definition | df-bnj17 30006 | Define the 4-way conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) | ||
Syntax | c-bnj14 30007 | Extend class notation with the function giving: the class of all elements of 𝐴 that are "smaller" than 𝑋 according to 𝑅. (New usage is discouraged.) |
class pred(𝑋, 𝐴, 𝑅) | ||
Definition | df-bnj14 30008* | Define the function giving: the class of all elements of 𝐴 that are "smaller" than 𝑋 according to 𝑅. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ pred(𝑋, 𝐴, 𝑅) = {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑋} | ||
Syntax | w-bnj13 30009 | Extend wff notation with the following predicate: 𝑅 is set-like on 𝐴. (New usage is discouraged.) |
wff 𝑅 Se 𝐴 | ||
Definition | df-bnj13 30010* | Define the following predicate: 𝑅 is set-like on 𝐴. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝑅 Se 𝐴 ↔ ∀𝑥 ∈ 𝐴 pred(𝑥, 𝐴, 𝑅) ∈ V) | ||
Syntax | w-bnj15 30011 | Extend wff notation with the following predicate: 𝑅 is both well-founded and set-like on 𝐴. (New usage is discouraged.) |
wff 𝑅 FrSe 𝐴 | ||
Definition | df-bnj15 30012 | Define the following predicate: 𝑅 is both well-founded and set-like on 𝐴. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝑅 FrSe 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴)) | ||
Syntax | c-bnj18 30013 | Extend class notation with the function giving: the transitive closure of 𝑋 in 𝐴 by 𝑅. (New usage is discouraged.) |
class trCl(𝑋, 𝐴, 𝑅) | ||
Definition | df-bnj18 30014* | Define the function giving: the transitive closure of 𝑋 in 𝐴 by 𝑅. This definition has been designed for facilitating verification that it is eliminable and that the $d restrictions are sound and complete. For a more readable definition see bnj882 30250. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ trCl(𝑋, 𝐴, 𝑅) = ∪ 𝑓 ∈ {𝑓 ∣ ∃𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))}∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) | ||
Syntax | w-bnj19 30015 | Extend wff notation with the following predicate: 𝐵 is transitive for 𝐴 and 𝑅. (New usage is discouraged.) |
wff TrFo(𝐵, 𝐴, 𝑅) | ||
Definition | df-bnj19 30016* | Define the following predicate: 𝐵 is transitive for 𝐴 and 𝑅. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ( TrFo(𝐵, 𝐴, 𝑅) ↔ ∀𝑥 ∈ 𝐵 pred(𝑥, 𝐴, 𝑅) ⊆ 𝐵) | ||
Theorem | bnj170 30017 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜓 ∧ 𝜒) ∧ 𝜑)) | ||
Theorem | bnj240 30018 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜓 → 𝜓′) & ⊢ (𝜒 → 𝜒′) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜓′ ∧ 𝜒′)) | ||
Theorem | bnj248 30019 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃)) | ||
Theorem | bnj250 30020 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃))) | ||
Theorem | bnj251 30021 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃)))) | ||
Theorem | bnj252 30022 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃))) | ||
Theorem | bnj253 30023 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) | ||
Theorem | bnj255 30024 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃))) | ||
Theorem | bnj256 30025 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃))) | ||
Theorem | bnj257 30026 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ 𝜓 ∧ 𝜃 ∧ 𝜒)) | ||
Theorem | bnj258 30027 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜓 ∧ 𝜃) ∧ 𝜒)) | ||
Theorem | bnj268 30028 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓 ∧ 𝜃)) | ||
Theorem | bnj290 30029 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ 𝜒 ∧ 𝜃 ∧ 𝜓)) | ||
Theorem | bnj291 30030 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜒 ∧ 𝜃) ∧ 𝜓)) | ||
Theorem | bnj312 30031 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒 ∧ 𝜃)) | ||
Theorem | bnj334 30032 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜒 ∧ 𝜑 ∧ 𝜓 ∧ 𝜃)) | ||
Theorem | bnj345 30033 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜃 ∧ 𝜑 ∧ 𝜓 ∧ 𝜒)) | ||
Theorem | bnj422 30034 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜒 ∧ 𝜃 ∧ 𝜑 ∧ 𝜓)) | ||
Theorem | bnj432 30035 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜒 ∧ 𝜃) ∧ (𝜑 ∧ 𝜓))) | ||
Theorem | bnj446 30036 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜑)) | ||
Theorem | bnj21 30037* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜑} ⇒ ⊢ 𝐵 ⊆ 𝐴 | ||
Theorem | bnj23 30038* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.) |
⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ⇒ ⊢ (∀𝑧 ∈ 𝐵 ¬ 𝑧𝑅𝑦 → ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑦 → [𝑤 / 𝑥]𝜑)) | ||
Theorem | bnj31 30039 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) & ⊢ (𝜓 → 𝜒) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒) | ||
Theorem | bnj62 30040* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ([𝑧 / 𝑥]𝑥 Fn 𝐴 ↔ 𝑧 Fn 𝐴) | ||
Theorem | bnj89 30041* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝑍 ∈ V ⇒ ⊢ ([𝑍 / 𝑦]∃!𝑥𝜑 ↔ ∃!𝑥[𝑍 / 𝑦]𝜑) | ||
Theorem | bnj90 30042* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.) |
⊢ 𝑌 ∈ V ⇒ ⊢ ([𝑌 / 𝑥]𝑧 Fn 𝑥 ↔ 𝑧 Fn 𝑌) | ||
Theorem | bnj101 30043 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ∃𝑥𝜑 & ⊢ (𝜑 → 𝜓) ⇒ ⊢ ∃𝑥𝜓 | ||
Theorem | bnj105 30044 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 1𝑜 ∈ V | ||
Theorem | bnj115 30045 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜂 ↔ ∀𝑛 ∈ 𝐷 (𝜏 → 𝜃)) ⇒ ⊢ (𝜂 ↔ ∀𝑛((𝑛 ∈ 𝐷 ∧ 𝜏) → 𝜃)) | ||
Theorem | bnj132 30046* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 ↔ ∃𝑥(𝜓 → 𝜒)) ⇒ ⊢ (𝜑 ↔ (𝜓 → ∃𝑥𝜒)) | ||
Theorem | bnj133 30047 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 ↔ ∃𝑥𝜓) & ⊢ (𝜒 ↔ 𝜓) ⇒ ⊢ (𝜑 ↔ ∃𝑥𝜒) | ||
Theorem | bnj142OLD 30048 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.) (Proof modification is discouraged.) Obsolete as of 29-Dec-2018. This is now incorporated into the proof of fnsnb 6337. |
⊢ (𝐹 Fn {𝐴} → (𝑢 ∈ 𝐹 → 𝑢 = 〈𝐴, (𝐹‘𝐴)〉)) | ||
Theorem | bnj145OLD 30049 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) (Proof modification is discouraged.) Obsolete as of 29-Dec-2018. This is now incorporated into the proof of fnsnb 6337. |
⊢ 𝐴 ∈ V & ⊢ (𝐹‘𝐴) ∈ V ⇒ ⊢ (𝐹 Fn {𝐴} → 𝐹 = {〈𝐴, (𝐹‘𝐴)〉}) | ||
Theorem | bnj156 30050 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜁0 ↔ (𝑓 Fn 1𝑜 ∧ 𝜑′ ∧ 𝜓′)) & ⊢ (𝜁1 ↔ [𝑔 / 𝑓]𝜁0) & ⊢ (𝜑1 ↔ [𝑔 / 𝑓]𝜑′) & ⊢ (𝜓1 ↔ [𝑔 / 𝑓]𝜓′) ⇒ ⊢ (𝜁1 ↔ (𝑔 Fn 1𝑜 ∧ 𝜑1 ∧ 𝜓1)) | ||
Theorem | bnj158 30051* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐷 = (ω ∖ {∅}) ⇒ ⊢ (𝑚 ∈ 𝐷 → ∃𝑝 ∈ ω 𝑚 = suc 𝑝) | ||
Theorem | bnj168 30052* | First-order logic and set theory. Revised to remove dependence on ax-reg 8380. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Revised by NM, 21-Dec-2016.) (New usage is discouraged.) |
⊢ 𝐷 = (ω ∖ {∅}) ⇒ ⊢ ((𝑛 ≠ 1𝑜 ∧ 𝑛 ∈ 𝐷) → ∃𝑚 ∈ 𝐷 𝑛 = suc 𝑚) | ||
Theorem | bnj206 30053 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑′ ↔ [𝑀 / 𝑛]𝜑) & ⊢ (𝜓′ ↔ [𝑀 / 𝑛]𝜓) & ⊢ (𝜒′ ↔ [𝑀 / 𝑛]𝜒) & ⊢ 𝑀 ∈ V ⇒ ⊢ ([𝑀 / 𝑛](𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑′ ∧ 𝜓′ ∧ 𝜒′)) | ||
Theorem | bnj216 30054 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 = suc 𝐵 → 𝐵 ∈ 𝐴) | ||
Theorem | bnj219 30055 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝑛 = suc 𝑚 → 𝑚 E 𝑛) | ||
Theorem | bnj226 30056* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐵 ⊆ 𝐶 ⇒ ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 | ||
Theorem | bnj228 30057 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) (New usage is discouraged.) |
⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓) | ||
Theorem | bnj519 30058 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Revised by Mario Carneiro, 6-May-2015.) (New usage is discouraged.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐵 ∈ V → Fun {〈𝐴, 𝐵〉}) | ||
Theorem | bnj521 30059 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝐴 ∩ {𝐴}) = ∅ | ||
Theorem | bnj524 30060 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ 𝐴 ∈ V ⇒ ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓) | ||
Theorem | bnj525 30061* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜑) | ||
Theorem | bnj534 30062* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜒 → (∃𝑥𝜑 ∧ 𝜓)) ⇒ ⊢ (𝜒 → ∃𝑥(𝜑 ∧ 𝜓)) | ||
Theorem | bnj538 30063* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) (Proof shortened by OpenAI, 30-Mar-2020.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ([𝐴 / 𝑦]∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝐵 [𝐴 / 𝑦]𝜑) | ||
Theorem | bnj538OLD 30064* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) Obsolete version of bnj538 30063 as of 30-Mar-2020. (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ([𝐴 / 𝑦]∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝐵 [𝐴 / 𝑦]𝜑) | ||
Theorem | bnj529 30065 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐷 = (ω ∖ {∅}) ⇒ ⊢ (𝑀 ∈ 𝐷 → ∅ ∈ 𝑀) | ||
Theorem | bnj551 30066 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝑚 = suc 𝑝 ∧ 𝑚 = suc 𝑖) → 𝑝 = 𝑖) | ||
Theorem | bnj563 30067 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜂 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝)) & ⊢ (𝜌 ↔ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 ≠ suc 𝑖)) ⇒ ⊢ ((𝜂 ∧ 𝜌) → suc 𝑖 ∈ 𝑚) | ||
Theorem | bnj564 30068 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′)) ⇒ ⊢ (𝜏 → dom 𝑓 = 𝑚) | ||
Theorem | bnj593 30069 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∃𝑥𝜓) & ⊢ (𝜓 → 𝜒) ⇒ ⊢ (𝜑 → ∃𝑥𝜒) | ||
Theorem | bnj596 30070 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → ∃𝑥𝜓) ⇒ ⊢ (𝜑 → ∃𝑥(𝜑 ∧ 𝜓)) | ||
Theorem | bnj610 30071* | Pass from equality (𝑥 = 𝐴) to substitution ([𝐴 / 𝑥]) without the distinct variable restriction ($d 𝐴 𝑥). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓′)) & ⊢ (𝑦 = 𝐴 → (𝜓′ ↔ 𝜓)) ⇒ ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜓) | ||
Theorem | bnj642 30072 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜑) | ||
Theorem | bnj643 30073 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜓) | ||
Theorem | bnj645 30074 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜃) | ||
Theorem | bnj658 30075 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → (𝜑 ∧ 𝜓 ∧ 𝜒)) | ||
Theorem | bnj667 30076 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → (𝜓 ∧ 𝜒 ∧ 𝜃)) | ||
Theorem | bnj705 30077 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | ||
Theorem | bnj706 30078 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜓 → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | ||
Theorem | bnj707 30079 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜒 → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | ||
Theorem | bnj708 30080 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜃 → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | ||
Theorem | bnj721 30081 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | ||
Theorem | bnj832 30082 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜂 ↔ (𝜑 ∧ 𝜓)) & ⊢ (𝜑 → 𝜏) ⇒ ⊢ (𝜂 → 𝜏) | ||
Theorem | bnj835 30083 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒)) & ⊢ (𝜑 → 𝜏) ⇒ ⊢ (𝜂 → 𝜏) | ||
Theorem | bnj836 30084 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒)) & ⊢ (𝜓 → 𝜏) ⇒ ⊢ (𝜂 → 𝜏) | ||
Theorem | bnj837 30085 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒)) & ⊢ (𝜒 → 𝜏) ⇒ ⊢ (𝜂 → 𝜏) | ||
Theorem | bnj769 30086 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃)) & ⊢ (𝜑 → 𝜏) ⇒ ⊢ (𝜂 → 𝜏) | ||
Theorem | bnj770 30087 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃)) & ⊢ (𝜓 → 𝜏) ⇒ ⊢ (𝜂 → 𝜏) | ||
Theorem | bnj771 30088 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃)) & ⊢ (𝜒 → 𝜏) ⇒ ⊢ (𝜂 → 𝜏) | ||
Theorem | bnj887 30089 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 ↔ 𝜑′) & ⊢ (𝜓 ↔ 𝜓′) & ⊢ (𝜒 ↔ 𝜒′) & ⊢ (𝜃 ↔ 𝜃′) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑′ ∧ 𝜓′ ∧ 𝜒′ ∧ 𝜃′)) | ||
Theorem | bnj918 30090 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐺 = (𝑓 ∪ {〈𝑛, 𝐶〉}) ⇒ ⊢ 𝐺 ∈ V | ||
Theorem | bnj919 30091* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝐹 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) & ⊢ (𝜑′ ↔ [𝑃 / 𝑛]𝜑) & ⊢ (𝜓′ ↔ [𝑃 / 𝑛]𝜓) & ⊢ (𝜒′ ↔ [𝑃 / 𝑛]𝜒) & ⊢ 𝑃 ∈ V ⇒ ⊢ (𝜒′ ↔ (𝑃 ∈ 𝐷 ∧ 𝐹 Fn 𝑃 ∧ 𝜑′ ∧ 𝜓′)) | ||
Theorem | bnj923 30092 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐷 = (ω ∖ {∅}) ⇒ ⊢ (𝑛 ∈ 𝐷 → 𝑛 ∈ ω) | ||
Theorem | bnj927 30093 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐺 = (𝑓 ∪ {〈𝑛, 𝐶〉}) & ⊢ 𝐶 ∈ V ⇒ ⊢ ((𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛) → 𝐺 Fn 𝑝) | ||
Theorem | bnj930 30094 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) ⇒ ⊢ (𝜑 → Fun 𝐹) | ||
Theorem | bnj931 30095 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐴 = (𝐵 ∪ 𝐶) ⇒ ⊢ 𝐵 ⊆ 𝐴 | ||
Theorem | bnj937 30096* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∃𝑥𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | bnj941 30097 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐺 = (𝑓 ∪ {〈𝑛, 𝐶〉}) ⇒ ⊢ (𝐶 ∈ V → ((𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛) → 𝐺 Fn 𝑝)) | ||
Theorem | bnj945 30098 | Technical lemma for bnj69 30332. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐺 = (𝑓 ∪ {〈𝑛, 𝐶〉}) ⇒ ⊢ ((𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ∧ 𝐴 ∈ 𝑛) → (𝐺‘𝐴) = (𝑓‘𝐴)) | ||
Theorem | bnj946 30099 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ (𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) | ||
Theorem | bnj951 30100 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜏 → 𝜑) & ⊢ (𝜏 → 𝜓) & ⊢ (𝜏 → 𝜒) & ⊢ (𝜏 → 𝜃) ⇒ ⊢ (𝜏 → (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |