HomeTheorem List (p. 338 of 479)
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. 338 of 479) | < 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-30166) |
Hilbert Space Explorer
(30167-31689) |
Users' Mathboxes
(31690-47842) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Definition | df-bnj18 33701* | 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 33932. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ trCl(𝑋, 𝐴, 𝑅) = ∪ 𝑓 ∈ {𝑓 ∣ ∃𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))}∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) | ||
| Syntax | w-bnj19 33702 | Extend wff notation with the following predicate: 𝐵 is transitive for 𝐴 and 𝑅. (New usage is discouraged.) |
| wff TrFo(𝐵, 𝐴, 𝑅) | ||
| Definition | df-bnj19 33703* | Define the following predicate: 𝐵 is transitive for 𝐴 and 𝑅. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ( TrFo(𝐵, 𝐴, 𝑅) ↔ ∀𝑥 ∈ 𝐵 pred(𝑥, 𝐴, 𝑅) ⊆ 𝐵) | ||
| Theorem | bnj170 33704 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜓 ∧ 𝜒) ∧ 𝜑)) | ||
| Theorem | bnj240 33705 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜓 → 𝜓′) & ⊢ (𝜒 → 𝜒′) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜓′ ∧ 𝜒′)) | ||
| Theorem | bnj248 33706 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃)) | ||
| Theorem | bnj250 33707 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃))) | ||
| Theorem | bnj251 33708 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃)))) | ||
| Theorem | bnj252 33709 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃))) | ||
| Theorem | bnj253 33710 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) | ||
| Theorem | bnj255 33711 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃))) | ||
| Theorem | bnj256 33712 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃))) | ||
| Theorem | bnj257 33713 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ 𝜓 ∧ 𝜃 ∧ 𝜒)) | ||
| Theorem | bnj258 33714 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜓 ∧ 𝜃) ∧ 𝜒)) | ||
| Theorem | bnj268 33715 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓 ∧ 𝜃)) | ||
| Theorem | bnj290 33716 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ 𝜒 ∧ 𝜃 ∧ 𝜓)) | ||
| Theorem | bnj291 33717 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜒 ∧ 𝜃) ∧ 𝜓)) | ||
| Theorem | bnj312 33718 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒 ∧ 𝜃)) | ||
| Theorem | bnj334 33719 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜒 ∧ 𝜑 ∧ 𝜓 ∧ 𝜃)) | ||
| Theorem | bnj345 33720 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜃 ∧ 𝜑 ∧ 𝜓 ∧ 𝜒)) | ||
| Theorem | bnj422 33721 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜒 ∧ 𝜃 ∧ 𝜑 ∧ 𝜓)) | ||
| Theorem | bnj432 33722 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜒 ∧ 𝜃) ∧ (𝜑 ∧ 𝜓))) | ||
| Theorem | bnj446 33723 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜑)) | ||
| Theorem | bnj23 33724* | 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 33725 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) & ⊢ (𝜓 → 𝜒) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒) | ||
| Theorem | bnj62 33726* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ([𝑧 / 𝑥]𝑥 Fn 𝐴 ↔ 𝑧 Fn 𝐴) | ||
| Theorem | bnj89 33727* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ 𝑍 ∈ V ⇒ ⊢ ([𝑍 / 𝑦]∃!𝑥𝜑 ↔ ∃!𝑥[𝑍 / 𝑦]𝜑) | ||
| Theorem | bnj90 33728* | 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 33729 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ∃𝑥𝜑 & ⊢ (𝜑 → 𝜓) ⇒ ⊢ ∃𝑥𝜓 | ||
| Theorem | bnj105 33730 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ 1o ∈ V | ||
| Theorem | bnj115 33731 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜂 ↔ ∀𝑛 ∈ 𝐷 (𝜏 → 𝜃)) ⇒ ⊢ (𝜂 ↔ ∀𝑛((𝑛 ∈ 𝐷 ∧ 𝜏) → 𝜃)) | ||
| Theorem | bnj132 33732* | 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 33733 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜑 ↔ ∃𝑥𝜓) & ⊢ (𝜒 ↔ 𝜓) ⇒ ⊢ (𝜑 ↔ ∃𝑥𝜒) | ||
| Theorem | bnj156 33734 | 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 33735* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ 𝐷 = (ω ∖ {∅}) ⇒ ⊢ (𝑚 ∈ 𝐷 → ∃𝑝 ∈ ω 𝑚 = suc 𝑝) | ||
| Theorem | bnj168 33736* | First-order logic and set theory. Revised to remove dependence on ax-reg 9586. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Revised by NM, 21-Dec-2016.) (New usage is discouraged.) |
| ⊢ 𝐷 = (ω ∖ {∅}) ⇒ ⊢ ((𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷) → ∃𝑚 ∈ 𝐷 𝑛 = suc 𝑚) | ||
| Theorem | bnj206 33737 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜑′ ↔ [𝑀 / 𝑛]𝜑) & ⊢ (𝜓′ ↔ [𝑀 / 𝑛]𝜓) & ⊢ (𝜒′ ↔ [𝑀 / 𝑛]𝜒) & ⊢ 𝑀 ∈ V ⇒ ⊢ ([𝑀 / 𝑛](𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑′ ∧ 𝜓′ ∧ 𝜒′)) | ||
| Theorem | bnj216 33738 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 = suc 𝐵 → 𝐵 ∈ 𝐴) | ||
| Theorem | bnj219 33739 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝑛 = suc 𝑚 → 𝑚 E 𝑛) | ||
| Theorem | bnj226 33740* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ 𝐵 ⊆ 𝐶 ⇒ ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 | ||
| Theorem | bnj228 33741 | 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 33742 | 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 33743 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜑 ↔ 𝜓) & ⊢ 𝐴 ∈ V ⇒ ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓) | ||
| Theorem | bnj525 33744* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜑) | ||
| Theorem | bnj534 33745* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜒 → (∃𝑥𝜑 ∧ 𝜓)) ⇒ ⊢ (𝜒 → ∃𝑥(𝜑 ∧ 𝜓)) | ||
| Theorem | bnj538 33746* | 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 33747 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ 𝐷 = (ω ∖ {∅}) ⇒ ⊢ (𝑀 ∈ 𝐷 → ∅ ∈ 𝑀) | ||
| Theorem | bnj551 33748 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝑚 = suc 𝑝 ∧ 𝑚 = suc 𝑖) → 𝑝 = 𝑖) | ||
| Theorem | bnj563 33749 | 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 33750 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′)) ⇒ ⊢ (𝜏 → dom 𝑓 = 𝑚) | ||
| Theorem | bnj593 33751 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜑 → ∃𝑥𝜓) & ⊢ (𝜓 → 𝜒) ⇒ ⊢ (𝜑 → ∃𝑥𝜒) | ||
| Theorem | bnj596 33752 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → ∃𝑥𝜓) ⇒ ⊢ (𝜑 → ∃𝑥(𝜑 ∧ 𝜓)) | ||
| Theorem | bnj610 33753* | 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 33754 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜑) | ||
| Theorem | bnj643 33755 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜓) | ||
| Theorem | bnj645 33756 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜃) | ||
| Theorem | bnj658 33757 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → (𝜑 ∧ 𝜓 ∧ 𝜒)) | ||
| Theorem | bnj667 33758 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → (𝜓 ∧ 𝜒 ∧ 𝜃)) | ||
| Theorem | bnj705 33759 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | ||
| Theorem | bnj706 33760 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜓 → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | ||
| Theorem | bnj707 33761 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜒 → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | ||
| Theorem | bnj708 33762 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜃 → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | ||
| Theorem | bnj721 33763 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | ||
| Theorem | bnj832 33764 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜂 ↔ (𝜑 ∧ 𝜓)) & ⊢ (𝜑 → 𝜏) ⇒ ⊢ (𝜂 → 𝜏) | ||
| Theorem | bnj835 33765 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒)) & ⊢ (𝜑 → 𝜏) ⇒ ⊢ (𝜂 → 𝜏) | ||
| Theorem | bnj836 33766 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒)) & ⊢ (𝜓 → 𝜏) ⇒ ⊢ (𝜂 → 𝜏) | ||
| Theorem | bnj837 33767 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒)) & ⊢ (𝜒 → 𝜏) ⇒ ⊢ (𝜂 → 𝜏) | ||
| Theorem | bnj769 33768 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃)) & ⊢ (𝜑 → 𝜏) ⇒ ⊢ (𝜂 → 𝜏) | ||
| Theorem | bnj770 33769 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃)) & ⊢ (𝜓 → 𝜏) ⇒ ⊢ (𝜂 → 𝜏) | ||
| Theorem | bnj771 33770 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃)) & ⊢ (𝜒 → 𝜏) ⇒ ⊢ (𝜂 → 𝜏) | ||
| Theorem | bnj887 33771 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜑 ↔ 𝜑′) & ⊢ (𝜓 ↔ 𝜓′) & ⊢ (𝜒 ↔ 𝜒′) & ⊢ (𝜃 ↔ 𝜃′) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑′ ∧ 𝜓′ ∧ 𝜒′ ∧ 𝜃′)) | ||
| Theorem | bnj918 33772 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ 𝐺 = (𝑓 ∪ {⟨𝑛, 𝐶⟩}) ⇒ ⊢ 𝐺 ∈ V | ||
| Theorem | bnj919 33773* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝐹 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) & ⊢ (𝜑′ ↔ [𝑃 / 𝑛]𝜑) & ⊢ (𝜓′ ↔ [𝑃 / 𝑛]𝜓) & ⊢ (𝜒′ ↔ [𝑃 / 𝑛]𝜒) & ⊢ 𝑃 ∈ V ⇒ ⊢ (𝜒′ ↔ (𝑃 ∈ 𝐷 ∧ 𝐹 Fn 𝑃 ∧ 𝜑′ ∧ 𝜓′)) | ||
| Theorem | bnj923 33774 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ 𝐷 = (ω ∖ {∅}) ⇒ ⊢ (𝑛 ∈ 𝐷 → 𝑛 ∈ ω) | ||
| Theorem | bnj927 33775 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ 𝐺 = (𝑓 ∪ {⟨𝑛, 𝐶⟩}) & ⊢ 𝐶 ∈ V ⇒ ⊢ ((𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛) → 𝐺 Fn 𝑝) | ||
| Theorem | bnj931 33776 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ 𝐴 = (𝐵 ∪ 𝐶) ⇒ ⊢ 𝐵 ⊆ 𝐴 | ||
| Theorem | bnj937 33777* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜑 → ∃𝑥𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
| Theorem | bnj941 33778 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ 𝐺 = (𝑓 ∪ {⟨𝑛, 𝐶⟩}) ⇒ ⊢ (𝐶 ∈ V → ((𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛) → 𝐺 Fn 𝑝)) | ||
| Theorem | bnj945 33779 | Technical lemma for bnj69 34016. 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 33780 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ (𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) | ||
| Theorem | bnj951 33781 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜏 → 𝜑) & ⊢ (𝜏 → 𝜓) & ⊢ (𝜏 → 𝜒) & ⊢ (𝜏 → 𝜃) ⇒ ⊢ (𝜏 → (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃)) | ||
| Theorem | bnj956 33782 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝐴 = 𝐵 → ∀𝑥 𝐴 = 𝐵) ⇒ ⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶) | ||
| Theorem | bnj976 33783* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜒 ↔ (𝑁 ∈ 𝐷 ∧ 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓)) & ⊢ (𝜑′ ↔ [𝐺 / 𝑓]𝜑) & ⊢ (𝜓′ ↔ [𝐺 / 𝑓]𝜓) & ⊢ (𝜒′ ↔ [𝐺 / 𝑓]𝜒) & ⊢ 𝐺 ∈ V ⇒ ⊢ (𝜒′ ↔ (𝑁 ∈ 𝐷 ∧ 𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′)) | ||
| Theorem | bnj982 33784 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝜒 → ∀𝑥𝜒) & ⊢ (𝜃 → ∀𝑥𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → ∀𝑥(𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃)) | ||
| Theorem | bnj1019 33785* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (∃𝑝(𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂) ↔ (𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃𝑝𝜏)) | ||
| Theorem | bnj1023 33786 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ∃𝑥(𝜑 → 𝜓) & ⊢ (𝜓 → 𝜒) ⇒ ⊢ ∃𝑥(𝜑 → 𝜒) | ||
| Theorem | bnj1095 33787 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ (𝜑 → ∀𝑥𝜑) | ||
| Theorem | bnj1096 33788* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜓 ↔ (𝜒 ∧ 𝜃 ∧ 𝜏 ∧ 𝜑)) ⇒ ⊢ (𝜓 → ∀𝑥𝜓) | ||
| Theorem | bnj1098 33789* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ 𝐷 = (ω ∖ {∅}) ⇒ ⊢ ∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) → (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗)) | ||
| Theorem | bnj1101 33790 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ∃𝑥(𝜑 → 𝜓) & ⊢ (𝜒 → 𝜑) ⇒ ⊢ ∃𝑥(𝜒 → 𝜓) | ||
| Theorem | bnj1113 33791* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝐴 = 𝐵 → 𝐶 = 𝐷) ⇒ ⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐶 𝐸 = ∪ 𝑥 ∈ 𝐷 𝐸) | ||
| Theorem | bnj1109 33792 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ∃𝑥((𝐴 ≠ 𝐵 ∧ 𝜑) → 𝜓) & ⊢ ((𝐴 = 𝐵 ∧ 𝜑) → 𝜓) ⇒ ⊢ ∃𝑥(𝜑 → 𝜓) | ||
| Theorem | bnj1131 33793 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜑 → ∀𝑥𝜑) & ⊢ ∃𝑥𝜑 ⇒ ⊢ 𝜑 | ||
| Theorem | bnj1138 33794 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ 𝐴 = (𝐵 ∪ 𝐶) ⇒ ⊢ (𝑋 ∈ 𝐴 ↔ (𝑋 ∈ 𝐵 ∨ 𝑋 ∈ 𝐶)) | ||
| Theorem | bnj1142 33795 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) | ||
| Theorem | bnj1143 33796* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐵 | ||
| Theorem | bnj1146 33797* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) ⇒ ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐵 | ||
| Theorem | bnj1149 33798 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) ⇒ ⊢ (𝜑 → (𝐴 ∪ 𝐵) ∈ V) | ||
| Theorem | bnj1185 33799* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ⊢ (𝜑 → ∃𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 ¬ 𝑤𝑅𝑧) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥) | ||
| Theorem | bnj1196 33800 | 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 > |