![]() |
Metamath
Proof Explorer Theorem List (p. 339 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: | ![]() (1-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | bnj1143 33801* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐵 | ||
Theorem | bnj1146 33802* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) ⇒ ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐵 | ||
Theorem | bnj1149 33803 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) ⇒ ⊢ (𝜑 → (𝐴 ∪ 𝐵) ∈ V) | ||
Theorem | bnj1185 33804* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∃𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 ¬ 𝑤𝑅𝑧) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥) | ||
Theorem | bnj1196 33805 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ (𝜑 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) | ||
Theorem | bnj1198 33806 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∃𝑥𝜓) & ⊢ (𝜓′ ↔ 𝜓) ⇒ ⊢ (𝜑 → ∃𝑥𝜓′) | ||
Theorem | bnj1209 33807* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜒 → ∃𝑥 ∈ 𝐵 𝜑) & ⊢ (𝜃 ↔ (𝜒 ∧ 𝑥 ∈ 𝐵 ∧ 𝜑)) ⇒ ⊢ (𝜒 → ∃𝑥𝜃) | ||
Theorem | bnj1211 33808 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) | ||
Theorem | bnj1213 33809 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐴 ⊆ 𝐵 & ⊢ (𝜃 → 𝑥 ∈ 𝐴) ⇒ ⊢ (𝜃 → 𝑥 ∈ 𝐵) | ||
Theorem | bnj1212 33810* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜑} & ⊢ (𝜃 ↔ (𝜒 ∧ 𝑥 ∈ 𝐵 ∧ 𝜏)) ⇒ ⊢ (𝜃 → 𝑥 ∈ 𝐴) | ||
Theorem | bnj1219 33811 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜒 ↔ (𝜑 ∧ 𝜓 ∧ 𝜁)) & ⊢ (𝜃 ↔ (𝜒 ∧ 𝜏 ∧ 𝜂)) ⇒ ⊢ (𝜃 → 𝜓) | ||
Theorem | bnj1224 33812 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ¬ (𝜃 ∧ 𝜏 ∧ 𝜂) ⇒ ⊢ ((𝜃 ∧ 𝜏) → ¬ 𝜂) | ||
Theorem | bnj1230 33813* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜑} ⇒ ⊢ (𝑦 ∈ 𝐵 → ∀𝑥 𝑦 ∈ 𝐵) | ||
Theorem | bnj1232 33814 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃 ∧ 𝜏)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | bnj1235 33815 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃 ∧ 𝜏)) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | bnj1239 33816 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜒) → ∃𝑥 ∈ 𝐴 𝜓) | ||
Theorem | bnj1238 33817 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) | ||
Theorem | bnj1241 33818 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜓 → 𝐶 = 𝐴) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝐶 ⊆ 𝐵) | ||
Theorem | bnj1247 33819 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃 ∧ 𝜏)) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | bnj1254 33820 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃 ∧ 𝜏)) ⇒ ⊢ (𝜑 → 𝜏) | ||
Theorem | bnj1262 33821 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐴 ⊆ 𝐵 & ⊢ (𝜑 → 𝐶 = 𝐴) ⇒ ⊢ (𝜑 → 𝐶 ⊆ 𝐵) | ||
Theorem | bnj1266 33822 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜒 → ∃𝑥(𝜑 ∧ 𝜓)) ⇒ ⊢ (𝜒 → ∃𝑥𝜓) | ||
Theorem | bnj1265 33823* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | bnj1275 33824 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∃𝑥(𝜓 ∧ 𝜒)) & ⊢ (𝜑 → ∀𝑥𝜑) ⇒ ⊢ (𝜑 → ∃𝑥(𝜑 ∧ 𝜓 ∧ 𝜒)) | ||
Theorem | bnj1276 33825 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝜒 → ∀𝑥𝜒) & ⊢ (𝜃 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜃 → ∀𝑥𝜃) | ||
Theorem | bnj1292 33826 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐴 = (𝐵 ∩ 𝐶) ⇒ ⊢ 𝐴 ⊆ 𝐵 | ||
Theorem | bnj1293 33827 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐴 = (𝐵 ∩ 𝐶) ⇒ ⊢ 𝐴 ⊆ 𝐶 | ||
Theorem | bnj1294 33828 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) & ⊢ (𝜑 → 𝑥 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | bnj1299 33829 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) | ||
Theorem | bnj1304 33830 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∃𝑥𝜓) & ⊢ (𝜓 → 𝜒) & ⊢ (𝜓 → ¬ 𝜒) ⇒ ⊢ ¬ 𝜑 | ||
Theorem | bnj1316 33831* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) & ⊢ (𝑦 ∈ 𝐵 → ∀𝑥 𝑦 ∈ 𝐵) ⇒ ⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶) | ||
Theorem | bnj1317 33832* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐴 = {𝑥 ∣ 𝜑} ⇒ ⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) | ||
Theorem | bnj1322 33833 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐵) = 𝐴) | ||
Theorem | bnj1340 33834 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜓 → ∃𝑥𝜃) & ⊢ (𝜒 ↔ (𝜓 ∧ 𝜃)) & ⊢ (𝜓 → ∀𝑥𝜓) ⇒ ⊢ (𝜓 → ∃𝑥𝜒) | ||
Theorem | bnj1345 33835 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∃𝑥(𝜓 ∧ 𝜒)) & ⊢ (𝜃 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒)) & ⊢ (𝜑 → ∀𝑥𝜑) ⇒ ⊢ (𝜑 → ∃𝑥𝜃) | ||
Theorem | bnj1350 33836* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜒 → ∀𝑥𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → ∀𝑥(𝜑 ∧ 𝜓 ∧ 𝜒)) | ||
Theorem | bnj1351 33837* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥𝜑) ⇒ ⊢ ((𝜑 ∧ 𝜓) → ∀𝑥(𝜑 ∧ 𝜓)) | ||
Theorem | bnj1352 33838* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜓 → ∀𝑥𝜓) ⇒ ⊢ ((𝜑 ∧ 𝜓) → ∀𝑥(𝜑 ∧ 𝜓)) | ||
Theorem | bnj1361 33839* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | ||
Theorem | bnj1366 33840* | 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) | ||
Theorem | bnj1379 33841* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 ↔ ∀𝑓 ∈ 𝐴 Fun 𝑓) & ⊢ 𝐷 = (dom 𝑓 ∩ dom 𝑔) & ⊢ (𝜓 ↔ (𝜑 ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))) & ⊢ (𝜒 ↔ (𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴)) & ⊢ (𝜃 ↔ (𝜒 ∧ 𝑓 ∈ 𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓)) & ⊢ (𝜏 ↔ (𝜃 ∧ 𝑔 ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑔)) ⇒ ⊢ (𝜓 → Fun ∪ 𝐴) | ||
Theorem | bnj1383 33842* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 ↔ ∀𝑓 ∈ 𝐴 Fun 𝑓) & ⊢ 𝐷 = (dom 𝑓 ∩ dom 𝑔) & ⊢ (𝜓 ↔ (𝜑 ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))) ⇒ ⊢ (𝜓 → Fun ∪ 𝐴) | ||
Theorem | bnj1385 33843* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 ↔ ∀𝑓 ∈ 𝐴 Fun 𝑓) & ⊢ 𝐷 = (dom 𝑓 ∩ dom 𝑔) & ⊢ (𝜓 ↔ (𝜑 ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))) & ⊢ (𝑥 ∈ 𝐴 → ∀𝑓 𝑥 ∈ 𝐴) & ⊢ (𝜑′ ↔ ∀ℎ ∈ 𝐴 Fun ℎ) & ⊢ 𝐸 = (dom ℎ ∩ dom 𝑔) & ⊢ (𝜓′ ↔ (𝜑′ ∧ ∀ℎ ∈ 𝐴 ∀𝑔 ∈ 𝐴 (ℎ ↾ 𝐸) = (𝑔 ↾ 𝐸))) ⇒ ⊢ (𝜓 → Fun ∪ 𝐴) | ||
Theorem | bnj1386 33844* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 ↔ ∀𝑓 ∈ 𝐴 Fun 𝑓) & ⊢ 𝐷 = (dom 𝑓 ∩ dom 𝑔) & ⊢ (𝜓 ↔ (𝜑 ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))) & ⊢ (𝑥 ∈ 𝐴 → ∀𝑓 𝑥 ∈ 𝐴) ⇒ ⊢ (𝜓 → Fun ∪ 𝐴) | ||
Theorem | bnj1397 33845 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∃𝑥𝜓) & ⊢ (𝜓 → ∀𝑥𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | bnj1400 33846* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) ⇒ ⊢ dom ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 dom 𝑥 | ||
Theorem | bnj1405 33847* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → 𝑋 ∈ ∪ 𝑦 ∈ 𝐴 𝐵) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ 𝐴 𝑋 ∈ 𝐵) | ||
Theorem | bnj1422 33848 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → Fun 𝐴) & ⊢ (𝜑 → dom 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴 Fn 𝐵) | ||
Theorem | bnj1424 33849 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐴 = (𝐵 ∪ 𝐶) ⇒ ⊢ (𝐷 ∈ 𝐴 → (𝐷 ∈ 𝐵 ∨ 𝐷 ∈ 𝐶)) | ||
Theorem | bnj1436 33850 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐴 = {𝑥 ∣ 𝜑} ⇒ ⊢ (𝑥 ∈ 𝐴 → 𝜑) | ||
Theorem | bnj1441 33851* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) Add disjoint variable condition to avoid ax-13 2372. See bnj1441g 33852 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024.) (New usage is discouraged.) |
⊢ (𝑥 ∈ 𝐴 → ∀𝑦 𝑥 ∈ 𝐴) & ⊢ (𝜑 → ∀𝑦𝜑) ⇒ ⊢ (𝑧 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} → ∀𝑦 𝑧 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑}) | ||
Theorem | bnj1441g 33852* | First-order logic and set theory. See bnj1441 33851 for a version with more disjoint variable conditions, but not requiring ax-13 2372. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝑥 ∈ 𝐴 → ∀𝑦 𝑥 ∈ 𝐴) & ⊢ (𝜑 → ∀𝑦𝜑) ⇒ ⊢ (𝑧 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} → ∀𝑦 𝑧 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑}) | ||
Theorem | bnj1454 33853 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐴 = {𝑥 ∣ 𝜑} ⇒ ⊢ (𝐵 ∈ V → (𝐵 ∈ 𝐴 ↔ [𝐵 / 𝑥]𝜑)) | ||
Theorem | bnj1459 33854* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜓 ↔ (𝜑 ∧ 𝑥 ∈ 𝐴)) & ⊢ (𝜓 → 𝜒) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜒) | ||
Theorem | bnj1464 33855* | Conversion of implicit substitution to explicit class substitution. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓)) | ||
Theorem | bnj1465 33856* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝜒 → 𝜓) ⇒ ⊢ ((𝜒 ∧ 𝐴 ∈ 𝑉) → ∃𝑥𝜑) | ||
Theorem | bnj1468 33857* | Conversion of implicit substitution to explicit class substitution. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) ⇒ ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓)) | ||
Theorem | bnj1476 33858 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} & ⊢ (𝜓 → 𝐷 = ∅) ⇒ ⊢ (𝜓 → ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | bnj1502 33859 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → Fun 𝐹) & ⊢ (𝜑 → 𝐺 ⊆ 𝐹) & ⊢ (𝜑 → 𝐴 ∈ dom 𝐺) ⇒ ⊢ (𝜑 → (𝐹‘𝐴) = (𝐺‘𝐴)) | ||
Theorem | bnj1503 33860 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → Fun 𝐹) & ⊢ (𝜑 → 𝐺 ⊆ 𝐹) & ⊢ (𝜑 → 𝐴 ⊆ dom 𝐺) ⇒ ⊢ (𝜑 → (𝐹 ↾ 𝐴) = (𝐺 ↾ 𝐴)) | ||
Theorem | bnj1517 33861 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐴 = {𝑥 ∣ (𝜑 ∧ 𝜓)} ⇒ ⊢ (𝑥 ∈ 𝐴 → 𝜓) | ||
Theorem | bnj1521 33862 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜒 → ∃𝑥 ∈ 𝐵 𝜑) & ⊢ (𝜃 ↔ (𝜒 ∧ 𝑥 ∈ 𝐵 ∧ 𝜑)) & ⊢ (𝜒 → ∀𝑥𝜒) ⇒ ⊢ (𝜒 → ∃𝑥𝜃) | ||
Theorem | bnj1533 33863 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜃 → ∀𝑧 ∈ 𝐵 ¬ 𝑧 ∈ 𝐷) & ⊢ 𝐵 ⊆ 𝐴 & ⊢ 𝐷 = {𝑧 ∈ 𝐴 ∣ 𝐶 ≠ 𝐸} ⇒ ⊢ (𝜃 → ∀𝑧 ∈ 𝐵 𝐶 = 𝐸) | ||
Theorem | bnj1534 33864* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ≠ (𝐻‘𝑥)} & ⊢ (𝑤 ∈ 𝐹 → ∀𝑥 𝑤 ∈ 𝐹) ⇒ ⊢ 𝐷 = {𝑧 ∈ 𝐴 ∣ (𝐹‘𝑧) ≠ (𝐻‘𝑧)} | ||
Theorem | bnj1536 33865* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐴) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 (𝐹‘𝑥) = (𝐺‘𝑥)) ⇒ ⊢ (𝜑 → (𝐹 ↾ 𝐵) = (𝐺 ↾ 𝐵)) | ||
Theorem | bnj1538 33866 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐴 = {𝑥 ∈ 𝐵 ∣ 𝜑} ⇒ ⊢ (𝑥 ∈ 𝐴 → 𝜑) | ||
Theorem | bnj1541 33867 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝐴 ≠ 𝐵)) & ⊢ ¬ 𝜑 ⇒ ⊢ (𝜓 → 𝐴 = 𝐵) | ||
Theorem | bnj1542 33868* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐴) & ⊢ (𝜑 → 𝐹 ≠ 𝐺) & ⊢ (𝑤 ∈ 𝐹 → ∀𝑥 𝑤 ∈ 𝐹) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) ≠ (𝐺‘𝑥)) | ||
Theorem | bnj110 33869* | Well-founded induction restricted to a set (𝐴 ∈ V). The proof has been taken from Chapter 4 of Don Monk's notes on Set Theory. See http://euclid.colorado.edu/~monkd/setth.pdf. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ 𝐴 ∈ V & ⊢ (𝜓 ↔ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)) ⇒ ⊢ ((𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑)) → ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | bnj157 33870* | Well-founded induction restricted to a set (𝐴 ∈ V). The proof has been taken from Chapter 4 of Don Monk's notes on Set Theory. See http://euclid.colorado.edu/~monkd/setth.pdf. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜓 ↔ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)) & ⊢ 𝐴 ∈ V & ⊢ 𝑅 Fr 𝐴 ⇒ ⊢ (∀𝑥 ∈ 𝐴 (𝜓 → 𝜑) → ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | bnj66 33871* | Technical lemma for bnj60 34073. 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.) |
⊢ 𝐵 = {𝑑 ∣ (𝑑 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝑑 pred(𝑥, 𝐴, 𝑅) ⊆ 𝑑)} & ⊢ 𝑌 = ⟨𝑥, (𝑓 ↾ pred(𝑥, 𝐴, 𝑅))⟩ & ⊢ 𝐶 = {𝑓 ∣ ∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} ⇒ ⊢ (𝑔 ∈ 𝐶 → Rel 𝑔) | ||
Theorem | bnj91 33872* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅)) & ⊢ 𝑍 ∈ V ⇒ ⊢ ([𝑍 / 𝑦]𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅)) | ||
Theorem | bnj92 33873* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) & ⊢ 𝑍 ∈ V ⇒ ⊢ ([𝑍 / 𝑛]𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑍 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) | ||
Theorem | bnj93 33874* | Technical lemma for bnj97 33877. 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.) |
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → pred(𝑥, 𝐴, 𝑅) ∈ V) | ||
Theorem | bnj95 33875 | Technical lemma for bnj124 33882. 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.) |
⊢ 𝐹 = {⟨∅, pred(𝑥, 𝐴, 𝑅)⟩} ⇒ ⊢ 𝐹 ∈ V | ||
Theorem | bnj96 33876* | Technical lemma for bnj150 33887. 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.) (Revised by Mario Carneiro, 6-May-2015.) (New usage is discouraged.) |
⊢ 𝐹 = {⟨∅, pred(𝑥, 𝐴, 𝑅)⟩} ⇒ ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → dom 𝐹 = 1o) | ||
Theorem | bnj97 33877* | Technical lemma for bnj150 33887. 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.) |
⊢ 𝐹 = {⟨∅, pred(𝑥, 𝐴, 𝑅)⟩} ⇒ ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐹‘∅) = pred(𝑥, 𝐴, 𝑅)) | ||
Theorem | bnj98 33878 | Technical lemma for bnj150 33887. 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.) |
⊢ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅)) | ||
Theorem | bnj106 33879* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) & ⊢ 𝐹 ∈ V ⇒ ⊢ ([𝐹 / 𝑓][1o / 𝑛]𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅))) | ||
Theorem | bnj118 33880* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅)) & ⊢ (𝜑′ ↔ [1o / 𝑛]𝜑) ⇒ ⊢ (𝜑′ ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅)) | ||
Theorem | bnj121 33881* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜁 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) & ⊢ (𝜁′ ↔ [1o / 𝑛]𝜁) & ⊢ (𝜑′ ↔ [1o / 𝑛]𝜑) & ⊢ (𝜓′ ↔ [1o / 𝑛]𝜓) ⇒ ⊢ (𝜁′ ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′))) | ||
Theorem | bnj124 33882* | Technical lemma for bnj150 33887. 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.) (Proof shortened by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.) |
⊢ 𝐹 = {⟨∅, pred(𝑥, 𝐴, 𝑅)⟩} & ⊢ (𝜑″ ↔ [𝐹 / 𝑓]𝜑′) & ⊢ (𝜓″ ↔ [𝐹 / 𝑓]𝜓′) & ⊢ (𝜁″ ↔ [𝐹 / 𝑓]𝜁′) & ⊢ (𝜁′ ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′))) ⇒ ⊢ (𝜁″ ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐹 Fn 1o ∧ 𝜑″ ∧ 𝜓″))) | ||
Theorem | bnj125 33883* | Technical lemma for bnj150 33887. 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.) |
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅)) & ⊢ (𝜑′ ↔ [1o / 𝑛]𝜑) & ⊢ (𝜑″ ↔ [𝐹 / 𝑓]𝜑′) & ⊢ 𝐹 = {⟨∅, pred(𝑥, 𝐴, 𝑅)⟩} ⇒ ⊢ (𝜑″ ↔ (𝐹‘∅) = pred(𝑥, 𝐴, 𝑅)) | ||
Theorem | bnj126 33884* | Technical lemma for bnj150 33887. 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.) |
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) & ⊢ (𝜓′ ↔ [1o / 𝑛]𝜓) & ⊢ (𝜓″ ↔ [𝐹 / 𝑓]𝜓′) & ⊢ 𝐹 = {⟨∅, pred(𝑥, 𝐴, 𝑅)⟩} ⇒ ⊢ (𝜓″ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅))) | ||
Theorem | bnj130 33885* | Technical lemma for bnj151 33888. 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.) |
⊢ (𝜃 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) & ⊢ (𝜑′ ↔ [1o / 𝑛]𝜑) & ⊢ (𝜓′ ↔ [1o / 𝑛]𝜓) & ⊢ (𝜃′ ↔ [1o / 𝑛]𝜃) ⇒ ⊢ (𝜃′ ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′))) | ||
Theorem | bnj149 33886* | Technical lemma for bnj151 33888. 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.) (Proof shortened by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.) |
⊢ (𝜃1 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃*𝑓(𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′))) & ⊢ (𝜁0 ↔ (𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′)) & ⊢ (𝜁1 ↔ [𝑔 / 𝑓]𝜁0) & ⊢ (𝜑1 ↔ [𝑔 / 𝑓]𝜑′) & ⊢ (𝜓1 ↔ [𝑔 / 𝑓]𝜓′) & ⊢ (𝜑′ ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅)) ⇒ ⊢ 𝜃1 | ||
Theorem | bnj150 33887* | Technical lemma for bnj151 33888. 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.) |
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅)) & ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) & ⊢ (𝜁 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) & ⊢ (𝜑′ ↔ [1o / 𝑛]𝜑) & ⊢ (𝜓′ ↔ [1o / 𝑛]𝜓) & ⊢ (𝜃0 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃𝑓(𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′))) & ⊢ (𝜁′ ↔ [1o / 𝑛]𝜁) & ⊢ 𝐹 = {⟨∅, pred(𝑥, 𝐴, 𝑅)⟩} & ⊢ (𝜑″ ↔ [𝐹 / 𝑓]𝜑′) & ⊢ (𝜓″ ↔ [𝐹 / 𝑓]𝜓′) & ⊢ (𝜁″ ↔ [𝐹 / 𝑓]𝜁′) ⇒ ⊢ 𝜃0 | ||
Theorem | bnj151 33888* | Technical lemma for bnj153 33891. 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.) |
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅)) & ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) & ⊢ 𝐷 = (ω ∖ {∅}) & ⊢ (𝜃 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) & ⊢ (𝜏 ↔ ∀𝑚 ∈ 𝐷 (𝑚 E 𝑛 → [𝑚 / 𝑛]𝜃)) & ⊢ (𝜁 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) & ⊢ (𝜑′ ↔ [1o / 𝑛]𝜑) & ⊢ (𝜓′ ↔ [1o / 𝑛]𝜓) & ⊢ (𝜃′ ↔ [1o / 𝑛]𝜃) & ⊢ (𝜃0 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃𝑓(𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′))) & ⊢ (𝜃1 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃*𝑓(𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′))) & ⊢ (𝜁′ ↔ [1o / 𝑛]𝜁) & ⊢ 𝐹 = {⟨∅, pred(𝑥, 𝐴, 𝑅)⟩} & ⊢ (𝜑″ ↔ [𝐹 / 𝑓]𝜑′) & ⊢ (𝜓″ ↔ [𝐹 / 𝑓]𝜓′) & ⊢ (𝜁″ ↔ [𝐹 / 𝑓]𝜁′) & ⊢ (𝜁0 ↔ (𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′)) & ⊢ (𝜁1 ↔ [𝑔 / 𝑓]𝜁0) & ⊢ (𝜑1 ↔ [𝑔 / 𝑓]𝜑′) & ⊢ (𝜓1 ↔ [𝑔 / 𝑓]𝜓′) ⇒ ⊢ (𝑛 = 1o → ((𝑛 ∈ 𝐷 ∧ 𝜏) → 𝜃)) | ||
Theorem | bnj154 33889* | Technical lemma for bnj153 33891. 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.) |
⊢ (𝜑1 ↔ [𝑔 / 𝑓]𝜑′) & ⊢ (𝜑′ ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅)) ⇒ ⊢ (𝜑1 ↔ (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅)) | ||
Theorem | bnj155 33890* | Technical lemma for bnj153 33891. 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.) |
⊢ (𝜓1 ↔ [𝑔 / 𝑓]𝜓′) & ⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) ⇒ ⊢ (𝜓1 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝑔‘suc 𝑖) = ∪ 𝑦 ∈ (𝑔‘𝑖) pred(𝑦, 𝐴, 𝑅))) | ||
Theorem | bnj153 33891* | Technical lemma for bnj852 33932. 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.) |
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅)) & ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) & ⊢ 𝐷 = (ω ∖ {∅}) & ⊢ (𝜃 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) & ⊢ (𝜏 ↔ ∀𝑚 ∈ 𝐷 (𝑚 E 𝑛 → [𝑚 / 𝑛]𝜃)) ⇒ ⊢ (𝑛 = 1o → ((𝑛 ∈ 𝐷 ∧ 𝜏) → 𝜃)) | ||
Theorem | bnj207 33892* | Technical lemma for bnj852 33932. 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.) |
⊢ (𝜒 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) & ⊢ (𝜑′ ↔ [𝑀 / 𝑛]𝜑) & ⊢ (𝜓′ ↔ [𝑀 / 𝑛]𝜓) & ⊢ (𝜒′ ↔ [𝑀 / 𝑛]𝜒) & ⊢ 𝑀 ∈ V ⇒ ⊢ (𝜒′ ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑀 ∧ 𝜑′ ∧ 𝜓′))) | ||
Theorem | bnj213 33893 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐴 | ||
Theorem | bnj222 33894* | Technical lemma for bnj229 33895. 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.) |
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅))) ⇒ ⊢ (𝜓 ↔ ∀𝑚 ∈ ω (suc 𝑚 ∈ 𝑁 → (𝐹‘suc 𝑚) = ∪ 𝑦 ∈ (𝐹‘𝑚) pred(𝑦, 𝐴, 𝑅))) | ||
Theorem | bnj229 33895* | Technical lemma for bnj517 33896. 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.) |
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅))) ⇒ ⊢ ((𝑛 ∈ 𝑁 ∧ (suc 𝑚 = 𝑛 ∧ 𝑚 ∈ ω ∧ 𝜓)) → (𝐹‘𝑛) ⊆ 𝐴) | ||
Theorem | bnj517 33896* | Technical lemma for bnj518 33897. 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.) (Proof shortened by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.) |
⊢ (𝜑 ↔ (𝐹‘∅) = pred(𝑋, 𝐴, 𝑅)) & ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅))) ⇒ ⊢ ((𝑁 ∈ ω ∧ 𝜑 ∧ 𝜓) → ∀𝑛 ∈ 𝑁 (𝐹‘𝑛) ⊆ 𝐴) | ||
Theorem | bnj518 33897* | Technical lemma for bnj852 33932. 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.) |
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅)) & ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) & ⊢ (𝜏 ↔ (𝜑 ∧ 𝜓 ∧ 𝑛 ∈ ω ∧ 𝑝 ∈ 𝑛)) ⇒ ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏) → ∀𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅) ∈ V) | ||
Theorem | bnj523 33898* | Technical lemma for bnj852 33932. 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.) |
⊢ (𝜑 ↔ (𝐹‘∅) = pred(𝑋, 𝐴, 𝑅)) & ⊢ (𝜑′ ↔ [𝑀 / 𝑛]𝜑) & ⊢ 𝑀 ∈ V ⇒ ⊢ (𝜑′ ↔ (𝐹‘∅) = pred(𝑋, 𝐴, 𝑅)) | ||
Theorem | bnj526 33899* | Technical lemma for bnj852 33932. 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.) |
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅)) & ⊢ (𝜑″ ↔ [𝐺 / 𝑓]𝜑) & ⊢ 𝐺 ∈ V ⇒ ⊢ (𝜑″ ↔ (𝐺‘∅) = pred(𝑋, 𝐴, 𝑅)) | ||
Theorem | bnj528 33900 | Technical lemma for bnj852 33932. 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.) |
⊢ 𝐺 = (𝑓 ∪ {⟨𝑚, ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)⟩}) ⇒ ⊢ 𝐺 ∈ V |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |