Home | Metamath
Proof Explorer Theorem List (p. 309 of 426) | < 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-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | bnj219 30801 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝑛 = suc 𝑚 → 𝑚 E 𝑛) | ||
Theorem | bnj226 30802* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐵 ⊆ 𝐶 ⇒ ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 | ||
Theorem | bnj228 30803 | 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 30804 | 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 30805 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝐴 ∩ {𝐴}) = ∅ | ||
Theorem | bnj524 30806 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ 𝐴 ∈ V ⇒ ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓) | ||
Theorem | bnj525 30807* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜑) | ||
Theorem | bnj534 30808* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜒 → (∃𝑥𝜑 ∧ 𝜓)) ⇒ ⊢ (𝜒 → ∃𝑥(𝜑 ∧ 𝜓)) | ||
Theorem | bnj538 30809* | 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 30810* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) Obsolete version of bnj538 30809 as of 30-Mar-2020. (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ([𝐴 / 𝑦]∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝐵 [𝐴 / 𝑦]𝜑) | ||
Theorem | bnj529 30811 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐷 = (ω ∖ {∅}) ⇒ ⊢ (𝑀 ∈ 𝐷 → ∅ ∈ 𝑀) | ||
Theorem | bnj551 30812 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝑚 = suc 𝑝 ∧ 𝑚 = suc 𝑖) → 𝑝 = 𝑖) | ||
Theorem | bnj563 30813 | 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 30814 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′)) ⇒ ⊢ (𝜏 → dom 𝑓 = 𝑚) | ||
Theorem | bnj593 30815 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∃𝑥𝜓) & ⊢ (𝜓 → 𝜒) ⇒ ⊢ (𝜑 → ∃𝑥𝜒) | ||
Theorem | bnj596 30816 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → ∃𝑥𝜓) ⇒ ⊢ (𝜑 → ∃𝑥(𝜑 ∧ 𝜓)) | ||
Theorem | bnj610 30817* | 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 30818 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜑) | ||
Theorem | bnj643 30819 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜓) | ||
Theorem | bnj645 30820 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜃) | ||
Theorem | bnj658 30821 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → (𝜑 ∧ 𝜓 ∧ 𝜒)) | ||
Theorem | bnj667 30822 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → (𝜓 ∧ 𝜒 ∧ 𝜃)) | ||
Theorem | bnj705 30823 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | ||
Theorem | bnj706 30824 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜓 → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | ||
Theorem | bnj707 30825 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜒 → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | ||
Theorem | bnj708 30826 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜃 → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | ||
Theorem | bnj721 30827 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | ||
Theorem | bnj832 30828 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜂 ↔ (𝜑 ∧ 𝜓)) & ⊢ (𝜑 → 𝜏) ⇒ ⊢ (𝜂 → 𝜏) | ||
Theorem | bnj835 30829 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒)) & ⊢ (𝜑 → 𝜏) ⇒ ⊢ (𝜂 → 𝜏) | ||
Theorem | bnj836 30830 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒)) & ⊢ (𝜓 → 𝜏) ⇒ ⊢ (𝜂 → 𝜏) | ||
Theorem | bnj837 30831 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒)) & ⊢ (𝜒 → 𝜏) ⇒ ⊢ (𝜂 → 𝜏) | ||
Theorem | bnj769 30832 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃)) & ⊢ (𝜑 → 𝜏) ⇒ ⊢ (𝜂 → 𝜏) | ||
Theorem | bnj770 30833 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃)) & ⊢ (𝜓 → 𝜏) ⇒ ⊢ (𝜂 → 𝜏) | ||
Theorem | bnj771 30834 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃)) & ⊢ (𝜒 → 𝜏) ⇒ ⊢ (𝜂 → 𝜏) | ||
Theorem | bnj887 30835 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 ↔ 𝜑′) & ⊢ (𝜓 ↔ 𝜓′) & ⊢ (𝜒 ↔ 𝜒′) & ⊢ (𝜃 ↔ 𝜃′) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑′ ∧ 𝜓′ ∧ 𝜒′ ∧ 𝜃′)) | ||
Theorem | bnj918 30836 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐺 = (𝑓 ∪ {〈𝑛, 𝐶〉}) ⇒ ⊢ 𝐺 ∈ V | ||
Theorem | bnj919 30837* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝐹 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) & ⊢ (𝜑′ ↔ [𝑃 / 𝑛]𝜑) & ⊢ (𝜓′ ↔ [𝑃 / 𝑛]𝜓) & ⊢ (𝜒′ ↔ [𝑃 / 𝑛]𝜒) & ⊢ 𝑃 ∈ V ⇒ ⊢ (𝜒′ ↔ (𝑃 ∈ 𝐷 ∧ 𝐹 Fn 𝑃 ∧ 𝜑′ ∧ 𝜓′)) | ||
Theorem | bnj923 30838 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐷 = (ω ∖ {∅}) ⇒ ⊢ (𝑛 ∈ 𝐷 → 𝑛 ∈ ω) | ||
Theorem | bnj927 30839 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐺 = (𝑓 ∪ {〈𝑛, 𝐶〉}) & ⊢ 𝐶 ∈ V ⇒ ⊢ ((𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛) → 𝐺 Fn 𝑝) | ||
Theorem | bnj930 30840 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) ⇒ ⊢ (𝜑 → Fun 𝐹) | ||
Theorem | bnj931 30841 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐴 = (𝐵 ∪ 𝐶) ⇒ ⊢ 𝐵 ⊆ 𝐴 | ||
Theorem | bnj937 30842* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∃𝑥𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | bnj941 30843 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐺 = (𝑓 ∪ {〈𝑛, 𝐶〉}) ⇒ ⊢ (𝐶 ∈ V → ((𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛) → 𝐺 Fn 𝑝)) | ||
Theorem | bnj945 30844 | Technical lemma for bnj69 31078. 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 30845 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ (𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) | ||
Theorem | bnj951 30846 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜏 → 𝜑) & ⊢ (𝜏 → 𝜓) & ⊢ (𝜏 → 𝜒) & ⊢ (𝜏 → 𝜃) ⇒ ⊢ (𝜏 → (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃)) | ||
Theorem | bnj956 30847 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝐴 = 𝐵 → ∀𝑥 𝐴 = 𝐵) ⇒ ⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶) | ||
Theorem | bnj976 30848* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜒 ↔ (𝑁 ∈ 𝐷 ∧ 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓)) & ⊢ (𝜑′ ↔ [𝐺 / 𝑓]𝜑) & ⊢ (𝜓′ ↔ [𝐺 / 𝑓]𝜓) & ⊢ (𝜒′ ↔ [𝐺 / 𝑓]𝜒) & ⊢ 𝐺 ∈ V ⇒ ⊢ (𝜒′ ↔ (𝑁 ∈ 𝐷 ∧ 𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′)) | ||
Theorem | bnj982 30849 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝜒 → ∀𝑥𝜒) & ⊢ (𝜃 → ∀𝑥𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) → ∀𝑥(𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃)) | ||
Theorem | bnj1019 30850* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (∃𝑝(𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂) ↔ (𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃𝑝𝜏)) | ||
Theorem | bnj1023 30851 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ∃𝑥(𝜑 → 𝜓) & ⊢ (𝜓 → 𝜒) ⇒ ⊢ ∃𝑥(𝜑 → 𝜒) | ||
Theorem | bnj1095 30852 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ (𝜑 → ∀𝑥𝜑) | ||
Theorem | bnj1096 30853* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜓 ↔ (𝜒 ∧ 𝜃 ∧ 𝜏 ∧ 𝜑)) ⇒ ⊢ (𝜓 → ∀𝑥𝜓) | ||
Theorem | bnj1098 30854* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐷 = (ω ∖ {∅}) ⇒ ⊢ ∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) → (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗)) | ||
Theorem | bnj1101 30855 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ∃𝑥(𝜑 → 𝜓) & ⊢ (𝜒 → 𝜑) ⇒ ⊢ ∃𝑥(𝜒 → 𝜓) | ||
Theorem | bnj1113 30856* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝐴 = 𝐵 → 𝐶 = 𝐷) ⇒ ⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐶 𝐸 = ∪ 𝑥 ∈ 𝐷 𝐸) | ||
Theorem | bnj1109 30857 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ∃𝑥((𝐴 ≠ 𝐵 ∧ 𝜑) → 𝜓) & ⊢ ((𝐴 = 𝐵 ∧ 𝜑) → 𝜓) ⇒ ⊢ ∃𝑥(𝜑 → 𝜓) | ||
Theorem | bnj1131 30858 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ ∃𝑥𝜑 ⇒ ⊢ 𝜑 | ||
Theorem | bnj1138 30859 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐴 = (𝐵 ∪ 𝐶) ⇒ ⊢ (𝑋 ∈ 𝐴 ↔ (𝑋 ∈ 𝐵 ∨ 𝑋 ∈ 𝐶)) | ||
Theorem | bnj1142 30860 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) | ||
Theorem | bnj1143 30861* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐵 | ||
Theorem | bnj1146 30862* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) ⇒ ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐵 | ||
Theorem | bnj1149 30863 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) ⇒ ⊢ (𝜑 → (𝐴 ∪ 𝐵) ∈ V) | ||
Theorem | bnj1185 30864* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∃𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 ¬ 𝑤𝑅𝑧) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥) | ||
Theorem | bnj1196 30865 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ (𝜑 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) | ||
Theorem | bnj1198 30866 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∃𝑥𝜓) & ⊢ (𝜓′ ↔ 𝜓) ⇒ ⊢ (𝜑 → ∃𝑥𝜓′) | ||
Theorem | bnj1209 30867* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜒 → ∃𝑥 ∈ 𝐵 𝜑) & ⊢ (𝜃 ↔ (𝜒 ∧ 𝑥 ∈ 𝐵 ∧ 𝜑)) ⇒ ⊢ (𝜒 → ∃𝑥𝜃) | ||
Theorem | bnj1211 30868 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) | ||
Theorem | bnj1213 30869 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐴 ⊆ 𝐵 & ⊢ (𝜃 → 𝑥 ∈ 𝐴) ⇒ ⊢ (𝜃 → 𝑥 ∈ 𝐵) | ||
Theorem | bnj1212 30870* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜑} & ⊢ (𝜃 ↔ (𝜒 ∧ 𝑥 ∈ 𝐵 ∧ 𝜏)) ⇒ ⊢ (𝜃 → 𝑥 ∈ 𝐴) | ||
Theorem | bnj1219 30871 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜒 ↔ (𝜑 ∧ 𝜓 ∧ 𝜁)) & ⊢ (𝜃 ↔ (𝜒 ∧ 𝜏 ∧ 𝜂)) ⇒ ⊢ (𝜃 → 𝜓) | ||
Theorem | bnj1224 30872 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ¬ (𝜃 ∧ 𝜏 ∧ 𝜂) ⇒ ⊢ ((𝜃 ∧ 𝜏) → ¬ 𝜂) | ||
Theorem | bnj1230 30873* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜑} ⇒ ⊢ (𝑦 ∈ 𝐵 → ∀𝑥 𝑦 ∈ 𝐵) | ||
Theorem | bnj1232 30874 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃 ∧ 𝜏)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | bnj1235 30875 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃 ∧ 𝜏)) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | bnj1239 30876 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜒) → ∃𝑥 ∈ 𝐴 𝜓) | ||
Theorem | bnj1238 30877 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) | ||
Theorem | bnj1241 30878 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜓 → 𝐶 = 𝐴) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝐶 ⊆ 𝐵) | ||
Theorem | bnj1247 30879 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃 ∧ 𝜏)) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | bnj1254 30880 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃 ∧ 𝜏)) ⇒ ⊢ (𝜑 → 𝜏) | ||
Theorem | bnj1262 30881 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐴 ⊆ 𝐵 & ⊢ (𝜑 → 𝐶 = 𝐴) ⇒ ⊢ (𝜑 → 𝐶 ⊆ 𝐵) | ||
Theorem | bnj1266 30882 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜒 → ∃𝑥(𝜑 ∧ 𝜓)) ⇒ ⊢ (𝜒 → ∃𝑥𝜓) | ||
Theorem | bnj1265 30883* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | bnj1275 30884 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∃𝑥(𝜓 ∧ 𝜒)) & ⊢ (𝜑 → ∀𝑥𝜑) ⇒ ⊢ (𝜑 → ∃𝑥(𝜑 ∧ 𝜓 ∧ 𝜒)) | ||
Theorem | bnj1276 30885 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝜒 → ∀𝑥𝜒) & ⊢ (𝜃 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜃 → ∀𝑥𝜃) | ||
Theorem | bnj1292 30886 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐴 = (𝐵 ∩ 𝐶) ⇒ ⊢ 𝐴 ⊆ 𝐵 | ||
Theorem | bnj1293 30887 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐴 = (𝐵 ∩ 𝐶) ⇒ ⊢ 𝐴 ⊆ 𝐶 | ||
Theorem | bnj1294 30888 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) & ⊢ (𝜑 → 𝑥 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | bnj1299 30889 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) | ||
Theorem | bnj1304 30890 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∃𝑥𝜓) & ⊢ (𝜓 → 𝜒) & ⊢ (𝜓 → ¬ 𝜒) ⇒ ⊢ ¬ 𝜑 | ||
Theorem | bnj1316 30891* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) & ⊢ (𝑦 ∈ 𝐵 → ∀𝑥 𝑦 ∈ 𝐵) ⇒ ⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶) | ||
Theorem | bnj1317 30892* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐴 = {𝑥 ∣ 𝜑} ⇒ ⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) | ||
Theorem | bnj1322 30893 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐵) = 𝐴) | ||
Theorem | bnj1340 30894 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜓 → ∃𝑥𝜃) & ⊢ (𝜒 ↔ (𝜓 ∧ 𝜃)) & ⊢ (𝜓 → ∀𝑥𝜓) ⇒ ⊢ (𝜓 → ∃𝑥𝜒) | ||
Theorem | bnj1345 30895 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∃𝑥(𝜓 ∧ 𝜒)) & ⊢ (𝜃 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒)) & ⊢ (𝜑 → ∀𝑥𝜑) ⇒ ⊢ (𝜑 → ∃𝑥𝜃) | ||
Theorem | bnj1350 30896* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜒 → ∀𝑥𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → ∀𝑥(𝜑 ∧ 𝜓 ∧ 𝜒)) | ||
Theorem | bnj1351 30897* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥𝜑) ⇒ ⊢ ((𝜑 ∧ 𝜓) → ∀𝑥(𝜑 ∧ 𝜓)) | ||
Theorem | bnj1352 30898* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜓 → ∀𝑥𝜓) ⇒ ⊢ ((𝜑 ∧ 𝜓) → ∀𝑥(𝜑 ∧ 𝜓)) | ||
Theorem | bnj1361 30899* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | ||
Theorem | bnj1366 30900* | 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 ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦𝜑 ∧ 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑})) ⇒ ⊢ (𝜓 → 𝐵 ∈ V) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |