![]() |
Metamath
Proof Explorer Theorem List (p. 334 of 473) | < 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: | ![]() (1-29860) |
![]() (29861-31383) |
![]() (31384-47242) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-bnj14 33301* | 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 33302 | Extend wff notation with the following predicate: 𝑅 is set-like on 𝐴. (New usage is discouraged.) |
wff 𝑅 Se 𝐴 | ||
Definition | df-bnj13 33303* | 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 33304 | Extend wff notation with the following predicate: 𝑅 is both well-founded and set-like on 𝐴. (New usage is discouraged.) |
wff 𝑅 FrSe 𝐴 | ||
Definition | df-bnj15 33305 | 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 33306 | Extend class notation with the function giving: the transitive closure of 𝑋 in 𝐴 by 𝑅. (New usage is discouraged.) |
class trCl(𝑋, 𝐴, 𝑅) | ||
Definition | df-bnj18 33307* | 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 33538. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ trCl(𝑋, 𝐴, 𝑅) = ∪ 𝑓 ∈ {𝑓 ∣ ∃𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))}∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) | ||
Syntax | w-bnj19 33308 | Extend wff notation with the following predicate: 𝐵 is transitive for 𝐴 and 𝑅. (New usage is discouraged.) |
wff TrFo(𝐵, 𝐴, 𝑅) | ||
Definition | df-bnj19 33309* | Define the following predicate: 𝐵 is transitive for 𝐴 and 𝑅. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ( TrFo(𝐵, 𝐴, 𝑅) ↔ ∀𝑥 ∈ 𝐵 pred(𝑥, 𝐴, 𝑅) ⊆ 𝐵) | ||
Theorem | bnj170 33310 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜓 ∧ 𝜒) ∧ 𝜑)) | ||
Theorem | bnj240 33311 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜓 → 𝜓′) & ⊢ (𝜒 → 𝜒′) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜓′ ∧ 𝜒′)) | ||
Theorem | bnj248 33312 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃)) | ||
Theorem | bnj250 33313 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃))) | ||
Theorem | bnj251 33314 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃)))) | ||
Theorem | bnj252 33315 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃))) | ||
Theorem | bnj253 33316 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) | ||
Theorem | bnj255 33317 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃))) | ||
Theorem | bnj256 33318 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃))) | ||
Theorem | bnj257 33319 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ 𝜓 ∧ 𝜃 ∧ 𝜒)) | ||
Theorem | bnj258 33320 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜓 ∧ 𝜃) ∧ 𝜒)) | ||
Theorem | bnj268 33321 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓 ∧ 𝜃)) | ||
Theorem | bnj290 33322 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ 𝜒 ∧ 𝜃 ∧ 𝜓)) | ||
Theorem | bnj291 33323 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜒 ∧ 𝜃) ∧ 𝜓)) | ||
Theorem | bnj312 33324 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒 ∧ 𝜃)) | ||
Theorem | bnj334 33325 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜒 ∧ 𝜑 ∧ 𝜓 ∧ 𝜃)) | ||
Theorem | bnj345 33326 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜃 ∧ 𝜑 ∧ 𝜓 ∧ 𝜒)) | ||
Theorem | bnj422 33327 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜒 ∧ 𝜃 ∧ 𝜑 ∧ 𝜓)) | ||
Theorem | bnj432 33328 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜒 ∧ 𝜃) ∧ (𝜑 ∧ 𝜓))) | ||
Theorem | bnj446 33329 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜑)) | ||
Theorem | bnj23 33330* | 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 33331 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) & ⊢ (𝜓 → 𝜒) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒) | ||
Theorem | bnj62 33332* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ([𝑧 / 𝑥]𝑥 Fn 𝐴 ↔ 𝑧 Fn 𝐴) | ||
Theorem | bnj89 33333* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝑍 ∈ V ⇒ ⊢ ([𝑍 / 𝑦]∃!𝑥𝜑 ↔ ∃!𝑥[𝑍 / 𝑦]𝜑) | ||
Theorem | bnj90 33334* | 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 33335 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ∃𝑥𝜑 & ⊢ (𝜑 → 𝜓) ⇒ ⊢ ∃𝑥𝜓 | ||
Theorem | bnj105 33336 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 1o ∈ V | ||
Theorem | bnj115 33337 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜂 ↔ ∀𝑛 ∈ 𝐷 (𝜏 → 𝜃)) ⇒ ⊢ (𝜂 ↔ ∀𝑛((𝑛 ∈ 𝐷 ∧ 𝜏) → 𝜃)) | ||
Theorem | bnj132 33338* | 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 33339 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 ↔ ∃𝑥𝜓) & ⊢ (𝜒 ↔ 𝜓) ⇒ ⊢ (𝜑 ↔ ∃𝑥𝜒) | ||
Theorem | bnj156 33340 | 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 33341* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐷 = (ω ∖ {∅}) ⇒ ⊢ (𝑚 ∈ 𝐷 → ∃𝑝 ∈ ω 𝑚 = suc 𝑝) | ||
Theorem | bnj168 33342* | First-order logic and set theory. Revised to remove dependence on ax-reg 9528. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Revised by NM, 21-Dec-2016.) (New usage is discouraged.) |
⊢ 𝐷 = (ω ∖ {∅}) ⇒ ⊢ ((𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷) → ∃𝑚 ∈ 𝐷 𝑛 = suc 𝑚) | ||
Theorem | bnj206 33343 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑′ ↔ [𝑀 / 𝑛]𝜑) & ⊢ (𝜓′ ↔ [𝑀 / 𝑛]𝜓) & ⊢ (𝜒′ ↔ [𝑀 / 𝑛]𝜒) & ⊢ 𝑀 ∈ V ⇒ ⊢ ([𝑀 / 𝑛](𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑′ ∧ 𝜓′ ∧ 𝜒′)) | ||
Theorem | bnj216 33344 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 = suc 𝐵 → 𝐵 ∈ 𝐴) | ||
Theorem | bnj219 33345 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝑛 = suc 𝑚 → 𝑚 E 𝑛) | ||
Theorem | bnj226 33346* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐵 ⊆ 𝐶 ⇒ ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 | ||
Theorem | bnj228 33347 | 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 33348 | 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 33349 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ 𝐴 ∈ V ⇒ ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓) | ||
Theorem | bnj525 33350* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜑) | ||
Theorem | bnj534 33351* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜒 → (∃𝑥𝜑 ∧ 𝜓)) ⇒ ⊢ (𝜒 → ∃𝑥(𝜑 ∧ 𝜓)) | ||
Theorem | bnj538 33352* | 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 33353 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐷 = (ω ∖ {∅}) ⇒ ⊢ (𝑀 ∈ 𝐷 → ∅ ∈ 𝑀) | ||
Theorem | bnj551 33354 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝑚 = suc 𝑝 ∧ 𝑚 = suc 𝑖) → 𝑝 = 𝑖) | ||
Theorem | bnj563 33355 | 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 33356 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′)) ⇒ ⊢ (𝜏 → dom 𝑓 = 𝑚) | ||
Theorem | bnj593 33357 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∃𝑥𝜓) & ⊢ (𝜓 → 𝜒) ⇒ ⊢ (𝜑 → ∃𝑥𝜒) | ||
Theorem | bnj596 33358 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → ∃𝑥𝜓) ⇒ ⊢ (𝜑 → ∃𝑥(𝜑 ∧ 𝜓)) | ||
Theorem | bnj610 33359* | 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 33360 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜑) | ||
Theorem | bnj643 33361 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜓) | ||
Theorem | bnj645 33362 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜃) | ||
Theorem | bnj658 33363 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → (𝜑 ∧ 𝜓 ∧ 𝜒)) | ||
Theorem | bnj667 33364 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → (𝜓 ∧ 𝜒 ∧ 𝜃)) | ||
Theorem | bnj705 33365 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | ||
Theorem | bnj706 33366 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜓 → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | ||
Theorem | bnj707 33367 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜒 → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | ||
Theorem | bnj708 33368 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜃 → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | ||
Theorem | bnj721 33369 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | ||
Theorem | bnj832 33370 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜂 ↔ (𝜑 ∧ 𝜓)) & ⊢ (𝜑 → 𝜏) ⇒ ⊢ (𝜂 → 𝜏) | ||
Theorem | bnj835 33371 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒)) & ⊢ (𝜑 → 𝜏) ⇒ ⊢ (𝜂 → 𝜏) | ||
Theorem | bnj836 33372 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒)) & ⊢ (𝜓 → 𝜏) ⇒ ⊢ (𝜂 → 𝜏) | ||
Theorem | bnj837 33373 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒)) & ⊢ (𝜒 → 𝜏) ⇒ ⊢ (𝜂 → 𝜏) | ||
Theorem | bnj769 33374 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃)) & ⊢ (𝜑 → 𝜏) ⇒ ⊢ (𝜂 → 𝜏) | ||
Theorem | bnj770 33375 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃)) & ⊢ (𝜓 → 𝜏) ⇒ ⊢ (𝜂 → 𝜏) | ||
Theorem | bnj771 33376 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃)) & ⊢ (𝜒 → 𝜏) ⇒ ⊢ (𝜂 → 𝜏) | ||
Theorem | bnj887 33377 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 ↔ 𝜑′) & ⊢ (𝜓 ↔ 𝜓′) & ⊢ (𝜒 ↔ 𝜒′) & ⊢ (𝜃 ↔ 𝜃′) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑′ ∧ 𝜓′ ∧ 𝜒′ ∧ 𝜃′)) | ||
Theorem | bnj918 33378 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐺 = (𝑓 ∪ {〈𝑛, 𝐶〉}) ⇒ ⊢ 𝐺 ∈ V | ||
Theorem | bnj919 33379* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝐹 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) & ⊢ (𝜑′ ↔ [𝑃 / 𝑛]𝜑) & ⊢ (𝜓′ ↔ [𝑃 / 𝑛]𝜓) & ⊢ (𝜒′ ↔ [𝑃 / 𝑛]𝜒) & ⊢ 𝑃 ∈ V ⇒ ⊢ (𝜒′ ↔ (𝑃 ∈ 𝐷 ∧ 𝐹 Fn 𝑃 ∧ 𝜑′ ∧ 𝜓′)) | ||
Theorem | bnj923 33380 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐷 = (ω ∖ {∅}) ⇒ ⊢ (𝑛 ∈ 𝐷 → 𝑛 ∈ ω) | ||
Theorem | bnj927 33381 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐺 = (𝑓 ∪ {〈𝑛, 𝐶〉}) & ⊢ 𝐶 ∈ V ⇒ ⊢ ((𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛) → 𝐺 Fn 𝑝) | ||
Theorem | bnj931 33382 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐴 = (𝐵 ∪ 𝐶) ⇒ ⊢ 𝐵 ⊆ 𝐴 | ||
Theorem | bnj937 33383* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∃𝑥𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | bnj941 33384 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐺 = (𝑓 ∪ {〈𝑛, 𝐶〉}) ⇒ ⊢ (𝐶 ∈ V → ((𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛) → 𝐺 Fn 𝑝)) | ||
Theorem | bnj945 33385 | Technical lemma for bnj69 33622. 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 33386 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ (𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) | ||
Theorem | bnj951 33387 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜏 → 𝜑) & ⊢ (𝜏 → 𝜓) & ⊢ (𝜏 → 𝜒) & ⊢ (𝜏 → 𝜃) ⇒ ⊢ (𝜏 → (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃)) | ||
Theorem | bnj956 33388 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝐴 = 𝐵 → ∀𝑥 𝐴 = 𝐵) ⇒ ⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶) | ||
Theorem | bnj976 33389* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜒 ↔ (𝑁 ∈ 𝐷 ∧ 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓)) & ⊢ (𝜑′ ↔ [𝐺 / 𝑓]𝜑) & ⊢ (𝜓′ ↔ [𝐺 / 𝑓]𝜓) & ⊢ (𝜒′ ↔ [𝐺 / 𝑓]𝜒) & ⊢ 𝐺 ∈ V ⇒ ⊢ (𝜒′ ↔ (𝑁 ∈ 𝐷 ∧ 𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′)) | ||
Theorem | bnj982 33390 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝜒 → ∀𝑥𝜒) & ⊢ (𝜃 → ∀𝑥𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → ∀𝑥(𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃)) | ||
Theorem | bnj1019 33391* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (∃𝑝(𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂) ↔ (𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃𝑝𝜏)) | ||
Theorem | bnj1023 33392 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ∃𝑥(𝜑 → 𝜓) & ⊢ (𝜓 → 𝜒) ⇒ ⊢ ∃𝑥(𝜑 → 𝜒) | ||
Theorem | bnj1095 33393 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ (𝜑 → ∀𝑥𝜑) | ||
Theorem | bnj1096 33394* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜓 ↔ (𝜒 ∧ 𝜃 ∧ 𝜏 ∧ 𝜑)) ⇒ ⊢ (𝜓 → ∀𝑥𝜓) | ||
Theorem | bnj1098 33395* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐷 = (ω ∖ {∅}) ⇒ ⊢ ∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) → (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗)) | ||
Theorem | bnj1101 33396 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ∃𝑥(𝜑 → 𝜓) & ⊢ (𝜒 → 𝜑) ⇒ ⊢ ∃𝑥(𝜒 → 𝜓) | ||
Theorem | bnj1113 33397* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝐴 = 𝐵 → 𝐶 = 𝐷) ⇒ ⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐶 𝐸 = ∪ 𝑥 ∈ 𝐷 𝐸) | ||
Theorem | bnj1109 33398 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ∃𝑥((𝐴 ≠ 𝐵 ∧ 𝜑) → 𝜓) & ⊢ ((𝐴 = 𝐵 ∧ 𝜑) → 𝜓) ⇒ ⊢ ∃𝑥(𝜑 → 𝜓) | ||
Theorem | bnj1131 33399 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ ∃𝑥𝜑 ⇒ ⊢ 𝜑 | ||
Theorem | bnj1138 33400 | 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 > |