HomeTheorem List (p. 351 of 505)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 351 of 505) | < 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-31179) |
Hilbert Space Explorer
(31180-32702) |
Users' Mathboxes
(32703-50434) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Definition | df-bnj18 35001* | 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 35231. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ trCl(𝑋, 𝐴, 𝑅) = ∪ 𝑓 ∈ {𝑓 ∣ ∃𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))}∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) | ||
| Syntax | w-bnj19 35002 | Extend wff notation with the following predicate: 𝐵 is transitive for 𝐴 and 𝑅. (New usage is discouraged.) |
| wff TrFo(𝐵, 𝐴, 𝑅) | ||
| Definition | df-bnj19 35003* | Define the following predicate: 𝐵 is transitive for 𝐴 and 𝑅. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ( TrFo(𝐵, 𝐴, 𝑅) ↔ ∀𝑥 ∈ 𝐵 pred(𝑥, 𝐴, 𝑅) ⊆ 𝐵) | ||
| Theorem | bnj170 35004 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜓 ∧ 𝜒) ∧ 𝜑)) | ||
| Theorem | bnj240 35005 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜓 → 𝜓′) & ⊢ (𝜒 → 𝜒′) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜓′ ∧ 𝜒′)) | ||
| Theorem | bnj248 35006 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃)) | ||
| Theorem | bnj250 35007 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃))) | ||
| Theorem | bnj251 35008 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃)))) | ||
| Theorem | bnj252 35009 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃))) | ||
| Theorem | bnj253 35010 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) | ||
| Theorem | bnj255 35011 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃))) | ||
| Theorem | bnj256 35012 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃))) | ||
| Theorem | bnj257 35013 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ 𝜓 ∧ 𝜃 ∧ 𝜒)) | ||
| Theorem | bnj258 35014 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜓 ∧ 𝜃) ∧ 𝜒)) | ||
| Theorem | bnj268 35015 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓 ∧ 𝜃)) | ||
| Theorem | bnj290 35016 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ 𝜒 ∧ 𝜃 ∧ 𝜓)) | ||
| Theorem | bnj291 35017 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜒 ∧ 𝜃) ∧ 𝜓)) | ||
| Theorem | bnj312 35018 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒 ∧ 𝜃)) | ||
| Theorem | bnj334 35019 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜒 ∧ 𝜑 ∧ 𝜓 ∧ 𝜃)) | ||
| Theorem | bnj345 35020 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜃 ∧ 𝜑 ∧ 𝜓 ∧ 𝜒)) | ||
| Theorem | bnj422 35021 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜒 ∧ 𝜃 ∧ 𝜑 ∧ 𝜓)) | ||
| Theorem | bnj432 35022 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜒 ∧ 𝜃) ∧ (𝜑 ∧ 𝜓))) | ||
| Theorem | bnj446 35023 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜑)) | ||
| Theorem | bnj23 35024* | 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 35025 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) & ⊢ (𝜓 → 𝜒) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒) | ||
| Theorem | bnj62 35026* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ([𝑧 / 𝑥]𝑥 Fn 𝐴 ↔ 𝑧 Fn 𝐴) | ||
| Theorem | bnj89 35027* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ 𝑍 ∈ V ⇒ ⊢ ([𝑍 / 𝑦]∃!𝑥𝜑 ↔ ∃!𝑥[𝑍 / 𝑦]𝜑) | ||
| Theorem | bnj90 35028* | 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 35029 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ∃𝑥𝜑 & ⊢ (𝜑 → 𝜓) ⇒ ⊢ ∃𝑥𝜓 | ||
| Theorem | bnj105 35030 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ 1o ∈ V | ||
| Theorem | bnj115 35031 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜂 ↔ ∀𝑛 ∈ 𝐷 (𝜏 → 𝜃)) ⇒ ⊢ (𝜂 ↔ ∀𝑛((𝑛 ∈ 𝐷 ∧ 𝜏) → 𝜃)) | ||
| Theorem | bnj132 35032* | 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 35033 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜑 ↔ ∃𝑥𝜓) & ⊢ (𝜒 ↔ 𝜓) ⇒ ⊢ (𝜑 ↔ ∃𝑥𝜒) | ||
| Theorem | bnj156 35034 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜁0 ↔ (𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′)) & ⊢ (𝜁1 ↔ [𝑔 / 𝑓]𝜁0) & ⊢ (𝜑1 ↔ [𝑔 / 𝑓]𝜑′) & ⊢ (𝜓1 ↔ [𝑔 / 𝑓]𝜓′) ⇒ ⊢ (𝜁1 ↔ (𝑔 Fn 1o ∧ 𝜑1 ∧ 𝜓1)) | ||
| Theorem | bnj158 35035* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ 𝐷 = (ω ∖ {∅}) ⇒ ⊢ (𝑚 ∈ 𝐷 → ∃𝑝 ∈ ω 𝑚 = suc 𝑝) | ||
| Theorem | bnj168 35036* | First-order logic and set theory. Revised to remove dependence on ax-reg 9542. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Revised by NM, 21-Dec-2016.) (New usage is discouraged.) |
| ⊢ 𝐷 = (ω ∖ {∅}) ⇒ ⊢ ((𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷) → ∃𝑚 ∈ 𝐷 𝑛 = suc 𝑚) | ||
| Theorem | bnj206 35037 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜑′ ↔ [𝑀 / 𝑛]𝜑) & ⊢ (𝜓′ ↔ [𝑀 / 𝑛]𝜓) & ⊢ (𝜒′ ↔ [𝑀 / 𝑛]𝜒) & ⊢ 𝑀 ∈ V ⇒ ⊢ ([𝑀 / 𝑛](𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑′ ∧ 𝜓′ ∧ 𝜒′)) | ||
| Theorem | bnj216 35038 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 = suc 𝐵 → 𝐵 ∈ 𝐴) | ||
| Theorem | bnj219 35039 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝑛 = suc 𝑚 → 𝑚 E 𝑛) | ||
| Theorem | bnj226 35040* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ 𝐵 ⊆ 𝐶 ⇒ ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 | ||
| Theorem | bnj228 35041 | 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 35042 | 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 | bnj524 35043 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜑 ↔ 𝜓) & ⊢ 𝐴 ∈ V ⇒ ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓) | ||
| Theorem | bnj525 35044* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜑) | ||
| Theorem | bnj534 35045* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜒 → (∃𝑥𝜑 ∧ 𝜓)) ⇒ ⊢ (𝜒 → ∃𝑥(𝜑 ∧ 𝜓)) | ||
| Theorem | bnj538 35046* | 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 | bnj529 35047 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ 𝐷 = (ω ∖ {∅}) ⇒ ⊢ (𝑀 ∈ 𝐷 → ∅ ∈ 𝑀) | ||
| Theorem | bnj551 35048 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝑚 = suc 𝑝 ∧ 𝑚 = suc 𝑖) → 𝑝 = 𝑖) | ||
| Theorem | bnj563 35049 | 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 35050 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′)) ⇒ ⊢ (𝜏 → dom 𝑓 = 𝑚) | ||
| Theorem | bnj593 35051 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜑 → ∃𝑥𝜓) & ⊢ (𝜓 → 𝜒) ⇒ ⊢ (𝜑 → ∃𝑥𝜒) | ||
| Theorem | bnj596 35052 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → ∃𝑥𝜓) ⇒ ⊢ (𝜑 → ∃𝑥(𝜑 ∧ 𝜓)) | ||
| Theorem | bnj610 35053* | Pass from equality (𝑥 = 𝐴) to substitution ([𝐴 / 𝑥]) without the distinct variable condition on 𝐴, 𝑥. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓′)) & ⊢ (𝑦 = 𝐴 → (𝜓′ ↔ 𝜓)) ⇒ ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜓) | ||
| Theorem | bnj642 35054 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜑) | ||
| Theorem | bnj643 35055 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜓) | ||
| Theorem | bnj645 35056 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜃) | ||
| Theorem | bnj658 35057 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → (𝜑 ∧ 𝜓 ∧ 𝜒)) | ||
| Theorem | bnj667 35058 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → (𝜓 ∧ 𝜒 ∧ 𝜃)) | ||
| Theorem | bnj705 35059 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | ||
| Theorem | bnj706 35060 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜓 → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | ||
| Theorem | bnj707 35061 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜒 → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | ||
| Theorem | bnj708 35062 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜃 → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | ||
| Theorem | bnj721 35063 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | ||
| Theorem | bnj832 35064 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜂 ↔ (𝜑 ∧ 𝜓)) & ⊢ (𝜑 → 𝜏) ⇒ ⊢ (𝜂 → 𝜏) | ||
| Theorem | bnj835 35065 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒)) & ⊢ (𝜑 → 𝜏) ⇒ ⊢ (𝜂 → 𝜏) | ||
| Theorem | bnj836 35066 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒)) & ⊢ (𝜓 → 𝜏) ⇒ ⊢ (𝜂 → 𝜏) | ||
| Theorem | bnj837 35067 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒)) & ⊢ (𝜒 → 𝜏) ⇒ ⊢ (𝜂 → 𝜏) | ||
| Theorem | bnj769 35068 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃)) & ⊢ (𝜑 → 𝜏) ⇒ ⊢ (𝜂 → 𝜏) | ||
| Theorem | bnj770 35069 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃)) & ⊢ (𝜓 → 𝜏) ⇒ ⊢ (𝜂 → 𝜏) | ||
| Theorem | bnj771 35070 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃)) & ⊢ (𝜒 → 𝜏) ⇒ ⊢ (𝜂 → 𝜏) | ||
| Theorem | bnj887 35071 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜑 ↔ 𝜑′) & ⊢ (𝜓 ↔ 𝜓′) & ⊢ (𝜒 ↔ 𝜒′) & ⊢ (𝜃 ↔ 𝜃′) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑′ ∧ 𝜓′ ∧ 𝜒′ ∧ 𝜃′)) | ||
| Theorem | bnj918 35072 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ 𝐺 = (𝑓 ∪ {⟨𝑛, 𝐶⟩}) ⇒ ⊢ 𝐺 ∈ V | ||
| Theorem | bnj919 35073* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝐹 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) & ⊢ (𝜑′ ↔ [𝑃 / 𝑛]𝜑) & ⊢ (𝜓′ ↔ [𝑃 / 𝑛]𝜓) & ⊢ (𝜒′ ↔ [𝑃 / 𝑛]𝜒) & ⊢ 𝑃 ∈ V ⇒ ⊢ (𝜒′ ↔ (𝑃 ∈ 𝐷 ∧ 𝐹 Fn 𝑃 ∧ 𝜑′ ∧ 𝜓′)) | ||
| Theorem | bnj923 35074 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ 𝐷 = (ω ∖ {∅}) ⇒ ⊢ (𝑛 ∈ 𝐷 → 𝑛 ∈ ω) | ||
| Theorem | bnj927 35075 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ 𝐺 = (𝑓 ∪ {⟨𝑛, 𝐶⟩}) & ⊢ 𝐶 ∈ V ⇒ ⊢ ((𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛) → 𝐺 Fn 𝑝) | ||
| Theorem | bnj931 35076 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ 𝐴 = (𝐵 ∪ 𝐶) ⇒ ⊢ 𝐵 ⊆ 𝐴 | ||
| Theorem | bnj937 35077* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜑 → ∃𝑥𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
| Theorem | bnj941 35078 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ 𝐺 = (𝑓 ∪ {⟨𝑛, 𝐶⟩}) ⇒ ⊢ (𝐶 ∈ V → ((𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛) → 𝐺 Fn 𝑝)) | ||
| Theorem | bnj945 35079 | Technical lemma for bnj69 35315. 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 35080 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ (𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) | ||
| Theorem | bnj951 35081 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜏 → 𝜑) & ⊢ (𝜏 → 𝜓) & ⊢ (𝜏 → 𝜒) & ⊢ (𝜏 → 𝜃) ⇒ ⊢ (𝜏 → (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃)) | ||
| Theorem | bnj956 35082 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝐴 = 𝐵 → ∀𝑥 𝐴 = 𝐵) ⇒ ⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶) | ||
| Theorem | bnj976 35083* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜒 ↔ (𝑁 ∈ 𝐷 ∧ 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓)) & ⊢ (𝜑′ ↔ [𝐺 / 𝑓]𝜑) & ⊢ (𝜓′ ↔ [𝐺 / 𝑓]𝜓) & ⊢ (𝜒′ ↔ [𝐺 / 𝑓]𝜒) & ⊢ 𝐺 ∈ V ⇒ ⊢ (𝜒′ ↔ (𝑁 ∈ 𝐷 ∧ 𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′)) | ||
| Theorem | bnj982 35084 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝜒 → ∀𝑥𝜒) & ⊢ (𝜃 → ∀𝑥𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → ∀𝑥(𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃)) | ||
| Theorem | bnj1019 35085* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (∃𝑝(𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂) ↔ (𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃𝑝𝜏)) | ||
| Theorem | bnj1023 35086 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ∃𝑥(𝜑 → 𝜓) & ⊢ (𝜓 → 𝜒) ⇒ ⊢ ∃𝑥(𝜑 → 𝜒) | ||
| Theorem | bnj1095 35087 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ (𝜑 → ∀𝑥𝜑) | ||
| Theorem | bnj1096 35088* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜓 ↔ (𝜒 ∧ 𝜃 ∧ 𝜏 ∧ 𝜑)) ⇒ ⊢ (𝜓 → ∀𝑥𝜓) | ||
| Theorem | bnj1098 35089* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ 𝐷 = (ω ∖ {∅}) ⇒ ⊢ ∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) → (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗)) | ||
| Theorem | bnj1101 35090 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ∃𝑥(𝜑 → 𝜓) & ⊢ (𝜒 → 𝜑) ⇒ ⊢ ∃𝑥(𝜒 → 𝜓) | ||
| Theorem | bnj1113 35091* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝐴 = 𝐵 → 𝐶 = 𝐷) ⇒ ⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐶 𝐸 = ∪ 𝑥 ∈ 𝐷 𝐸) | ||
| Theorem | bnj1109 35092 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ∃𝑥((𝐴 ≠ 𝐵 ∧ 𝜑) → 𝜓) & ⊢ ((𝐴 = 𝐵 ∧ 𝜑) → 𝜓) ⇒ ⊢ ∃𝑥(𝜑 → 𝜓) | ||
| Theorem | bnj1131 35093 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜑 → ∀𝑥𝜑) & ⊢ ∃𝑥𝜑 ⇒ ⊢ 𝜑 | ||
| Theorem | bnj1138 35094 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ 𝐴 = (𝐵 ∪ 𝐶) ⇒ ⊢ (𝑋 ∈ 𝐴 ↔ (𝑋 ∈ 𝐵 ∨ 𝑋 ∈ 𝐶)) | ||
| Theorem | bnj1143 35095* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐵 | ||
| Theorem | bnj1146 35096* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) ⇒ ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐵 | ||
| Theorem | bnj1149 35097 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) ⇒ ⊢ (𝜑 → (𝐴 ∪ 𝐵) ∈ V) | ||
| Theorem | bnj1185 35098* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜑 → ∃𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 ¬ 𝑤𝑅𝑧) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥) | ||
| Theorem | bnj1196 35099 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ (𝜑 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) | ||
| Theorem | bnj1198 35100 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜑 → ∃𝑥𝜓) & ⊢ (𝜓′ ↔ 𝜓) ⇒ ⊢ (𝜑 → ∃𝑥𝜓′) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |