![]() |
Metamath
Proof Explorer Theorem List (p. 362 of 489) | < 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-30950) |
![]() (30951-32473) |
![]() (32474-48899) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-line2 36101* | Define the Line function. This function generates the line passing through the distinct points 𝑎 and 𝑏. Adapted from definition 6.14 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 25-Oct-2013.) |
⊢ Line = {〈〈𝑎, 𝑏〉, 𝑙〉 ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [〈𝑎, 𝑏〉]◡ Colinear )} | ||
Definition | df-ray 36102* | Define the Ray function. This function generates the set of all points that lie on the ray starting at 𝑝 and passing through 𝑎. Definition 6.8 of [Schwabhauser] p. 44. (Contributed by Scott Fenton, 21-Oct-2013.) |
⊢ Ray = {〈〈𝑝, 𝑎〉, 𝑟〉 ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉})} | ||
Definition | df-lines2 36103 | Define the set of all lines. Definition 6.14, part 2 of [Schwabhauser] p. 45. See ellines 36116 for membership. (Contributed by Scott Fenton, 28-Oct-2013.) |
⊢ LinesEE = ran Line | ||
Theorem | funray 36104 | Show that the Ray relationship is a function. (Contributed by Scott Fenton, 21-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ Fun Ray | ||
Theorem | fvray 36105* | Calculate the value of the Ray function. (Contributed by Scott Fenton, 21-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝐴)) → (𝑃Ray𝐴) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉}) | ||
Theorem | funline 36106 | Show that the Line relationship is a function. (Contributed by Scott Fenton, 25-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ Fun Line | ||
Theorem | linedegen 36107 | When Line is applied with the same argument, the result is the empty set. (Contributed by Scott Fenton, 29-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (𝐴Line𝐴) = ∅ | ||
Theorem | fvline 36108* | Calculate the value of the Line function. (Contributed by Scott Fenton, 25-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵)) → (𝐴Line𝐵) = {𝑥 ∣ 𝑥 Colinear 〈𝐴, 𝐵〉}) | ||
Theorem | liness 36109 | A line is a subset of the space its two points lie in. (Contributed by Scott Fenton, 25-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵)) → (𝐴Line𝐵) ⊆ (𝔼‘𝑁)) | ||
Theorem | fvline2 36110* | Alternate definition of a line. (Contributed by Scott Fenton, 25-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵)) → (𝐴Line𝐵) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear 〈𝐴, 𝐵〉}) | ||
Theorem | lineunray 36111 | A line is composed of a point and the two rays emerging from it. Theorem 6.15 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 26-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → (𝑃 Btwn 〈𝑄, 𝑅〉 → (𝑃Line𝑄) = (((𝑃Ray𝑄) ∪ {𝑃}) ∪ (𝑃Ray𝑅)))) | ||
Theorem | lineelsb2 36112 | If 𝑆 lies on 𝑃𝑄, then 𝑃𝑄 = 𝑃𝑆. Theorem 6.16 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 27-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) → (𝑆 ∈ (𝑃Line𝑄) → (𝑃Line𝑄) = (𝑃Line𝑆))) | ||
Theorem | linerflx1 36113 | Reflexivity law for line membership. Part of theorem 6.17 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 28-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄)) → 𝑃 ∈ (𝑃Line𝑄)) | ||
Theorem | linecom 36114 | Commutativity law for lines. Part of theorem 6.17 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 28-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄)) → (𝑃Line𝑄) = (𝑄Line𝑃)) | ||
Theorem | linerflx2 36115 | Reflexivity law for line membership. Part of theorem 6.17 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 28-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄)) → 𝑄 ∈ (𝑃Line𝑄)) | ||
Theorem | ellines 36116* | Membership in the set of all lines. (Contributed by Scott Fenton, 28-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (𝐴 ∈ LinesEE ↔ ∃𝑛 ∈ ℕ ∃𝑝 ∈ (𝔼‘𝑛)∃𝑞 ∈ (𝔼‘𝑛)(𝑝 ≠ 𝑞 ∧ 𝐴 = (𝑝Line𝑞))) | ||
Theorem | linethru 36117 | If 𝐴 is a line containing two distinct points 𝑃 and 𝑄, then 𝐴 is the line through 𝑃 and 𝑄. Theorem 6.18 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 28-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝐴 ∈ LinesEE ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → 𝐴 = (𝑃Line𝑄)) | ||
Theorem | hilbert1.1 36118* | There is a line through any two distinct points. Hilbert's axiom I.1 for geometry. (Contributed by Scott Fenton, 29-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄)) → ∃𝑥 ∈ LinesEE (𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥)) | ||
Theorem | hilbert1.2 36119* | There is at most one line through any two distinct points. Hilbert's axiom I.2 for geometry. (Contributed by Scott Fenton, 29-Oct-2013.) (Revised by NM, 17-Jun-2017.) |
⊢ (𝑃 ≠ 𝑄 → ∃*𝑥 ∈ LinesEE (𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥)) | ||
Theorem | linethrueu 36120* | There is a unique line going through any two distinct points. Theorem 6.19 of [Schwabhauser] p. 46. (Contributed by Scott Fenton, 29-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄)) → ∃!𝑥 ∈ LinesEE (𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥)) | ||
Theorem | lineintmo 36121* | Two distinct lines intersect in at most one point. Theorem 6.21 of [Schwabhauser] p. 46. (Contributed by Scott Fenton, 29-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝐴 ∈ LinesEE ∧ 𝐵 ∈ LinesEE ∧ 𝐴 ≠ 𝐵) → ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) | ||
Syntax | cfwddif 36122 | Declare the syntax for the forward difference operator. |
class △ | ||
Definition | df-fwddif 36123* | Define the forward difference operator. This is a discrete analogue of the derivative operator. Definition 2.42 of [GramKnuthPat], p. 47. (Contributed by Scott Fenton, 18-May-2020.) |
⊢ △ = (𝑓 ∈ (ℂ ↑pm ℂ) ↦ (𝑥 ∈ {𝑦 ∈ dom 𝑓 ∣ (𝑦 + 1) ∈ dom 𝑓} ↦ ((𝑓‘(𝑥 + 1)) − (𝑓‘𝑥)))) | ||
Syntax | cfwddifn 36124 | Declare the syntax for the nth forward difference operator. |
class △n | ||
Definition | df-fwddifn 36125* | Define the nth forward difference operator. This works out to be the forward difference operator iterated 𝑛 times. (Contributed by Scott Fenton, 28-May-2020.) |
⊢ △n = (𝑛 ∈ ℕ0, 𝑓 ∈ (ℂ ↑pm ℂ) ↦ (𝑥 ∈ {𝑦 ∈ ℂ ∣ ∀𝑘 ∈ (0...𝑛)(𝑦 + 𝑘) ∈ dom 𝑓} ↦ Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((-1↑(𝑛 − 𝑘)) · (𝑓‘(𝑥 + 𝑘)))))) | ||
Theorem | fwddifval 36126 | Calculate the value of the forward difference operator at a point. (Contributed by Scott Fenton, 18-May-2020.) |
⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → (𝑋 + 1) ∈ 𝐴) ⇒ ⊢ (𝜑 → (( △ ‘𝐹)‘𝑋) = ((𝐹‘(𝑋 + 1)) − (𝐹‘𝑋))) | ||
Theorem | fwddifnval 36127* | The value of the forward difference operator at a point. (Contributed by Scott Fenton, 28-May-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑋 + 𝑘) ∈ 𝐴) ⇒ ⊢ (𝜑 → ((𝑁 △n 𝐹)‘𝑋) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘))))) | ||
Theorem | fwddifn0 36128 | The value of the n-iterated forward difference operator at zero is just the function value. (Contributed by Scott Fenton, 28-May-2020.) |
⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) ⇒ ⊢ (𝜑 → ((0 △n 𝐹)‘𝑋) = (𝐹‘𝑋)) | ||
Theorem | fwddifnp1 36129* | The value of the n-iterated forward difference at a successor. (Contributed by Scott Fenton, 28-May-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑋 + 𝑘) ∈ 𝐴) ⇒ ⊢ (𝜑 → (((𝑁 + 1) △n 𝐹)‘𝑋) = (((𝑁 △n 𝐹)‘(𝑋 + 1)) − ((𝑁 △n 𝐹)‘𝑋))) | ||
Theorem | rankung 36130 | The rank of the union of two sets. Closed form of rankun 9925. (Contributed by Scott Fenton, 15-Jul-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (rank‘(𝐴 ∪ 𝐵)) = ((rank‘𝐴) ∪ (rank‘𝐵))) | ||
Theorem | ranksng 36131 | The rank of a singleton. Closed form of ranksn 9923. (Contributed by Scott Fenton, 15-Jul-2015.) |
⊢ (𝐴 ∈ 𝑉 → (rank‘{𝐴}) = suc (rank‘𝐴)) | ||
Theorem | rankelg 36132 | The membership relation is inherited by the rank function. Closed form of rankel 9908. (Contributed by Scott Fenton, 16-Jul-2015.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝐵) → (rank‘𝐴) ∈ (rank‘𝐵)) | ||
Theorem | rankpwg 36133 | The rank of a power set. Closed form of rankpw 9912. (Contributed by Scott Fenton, 16-Jul-2015.) |
⊢ (𝐴 ∈ 𝑉 → (rank‘𝒫 𝐴) = suc (rank‘𝐴)) | ||
Theorem | rank0 36134 | The rank of the empty set is ∅. (Contributed by Scott Fenton, 17-Jul-2015.) |
⊢ (rank‘∅) = ∅ | ||
Theorem | rankeq1o 36135 | The only set with rank 1o is the singleton of the empty set. (Contributed by Scott Fenton, 17-Jul-2015.) |
⊢ ((rank‘𝐴) = 1o ↔ 𝐴 = {∅}) | ||
Syntax | chf 36136 | The constant Hf is a class. |
class Hf | ||
Definition | df-hf 36137 | Define the hereditarily finite sets. These are the finite sets whose elements are finite, and so forth. (Contributed by Scott Fenton, 9-Jul-2015.) |
⊢ Hf = ∪ (𝑅1 “ ω) | ||
Theorem | elhf 36138* | Membership in the hereditarily finite sets. (Contributed by Scott Fenton, 9-Jul-2015.) |
⊢ (𝐴 ∈ Hf ↔ ∃𝑥 ∈ ω 𝐴 ∈ (𝑅1‘𝑥)) | ||
Theorem | elhf2 36139 | Alternate form of membership in the hereditarily finite sets. (Contributed by Scott Fenton, 13-Jul-2015.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ Hf ↔ (rank‘𝐴) ∈ ω) | ||
Theorem | elhf2g 36140 | Hereditarily finiteness via rank. Closed form of elhf2 36139. (Contributed by Scott Fenton, 15-Jul-2015.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Hf ↔ (rank‘𝐴) ∈ ω)) | ||
Theorem | 0hf 36141 | The empty set is a hereditarily finite set. (Contributed by Scott Fenton, 9-Jul-2015.) |
⊢ ∅ ∈ Hf | ||
Theorem | hfun 36142 | The union of two HF sets is an HF set. (Contributed by Scott Fenton, 15-Jul-2015.) |
⊢ ((𝐴 ∈ Hf ∧ 𝐵 ∈ Hf ) → (𝐴 ∪ 𝐵) ∈ Hf ) | ||
Theorem | hfsn 36143 | The singleton of an HF set is an HF set. (Contributed by Scott Fenton, 15-Jul-2015.) |
⊢ (𝐴 ∈ Hf → {𝐴} ∈ Hf ) | ||
Theorem | hfadj 36144 | Adjoining one HF element to an HF set preserves HF status. (Contributed by Scott Fenton, 15-Jul-2015.) |
⊢ ((𝐴 ∈ Hf ∧ 𝐵 ∈ Hf ) → (𝐴 ∪ {𝐵}) ∈ Hf ) | ||
Theorem | hfelhf 36145 | Any member of an HF set is itself an HF set. (Contributed by Scott Fenton, 16-Jul-2015.) |
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ Hf ) → 𝐴 ∈ Hf ) | ||
Theorem | hftr 36146 | The class of all hereditarily finite sets is transitive. (Contributed by Scott Fenton, 16-Jul-2015.) |
⊢ Tr Hf | ||
Theorem | hfext 36147* | Extensionality for HF sets depends only on comparison of HF elements. (Contributed by Scott Fenton, 16-Jul-2015.) |
⊢ ((𝐴 ∈ Hf ∧ 𝐵 ∈ Hf ) → (𝐴 = 𝐵 ↔ ∀𝑥 ∈ Hf (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))) | ||
Theorem | hfuni 36148 | The union of an HF set is itself hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015.) |
⊢ (𝐴 ∈ Hf → ∪ 𝐴 ∈ Hf ) | ||
Theorem | hfpw 36149 | The power class of an HF set is hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015.) |
⊢ (𝐴 ∈ Hf → 𝒫 𝐴 ∈ Hf ) | ||
Theorem | hfninf 36150 | ω is not hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015.) |
⊢ ¬ ω ∈ Hf | ||
Theorem | rmoeqi 36151 | Equality inference for restricted at-most-one quantifier. (Contributed by GG, 1-Sep-2025.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐵 𝜓) | ||
Theorem | rmoeqbii 36152 | Equality inference for restricted at-most-one quantifier. (Contributed by GG, 1-Sep-2025.) |
⊢ 𝐴 = 𝐵 & ⊢ (𝜓 ↔ 𝜒) ⇒ ⊢ (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐵 𝜒) | ||
Theorem | reueqi 36153 | Equality inference for restricted existential uniqueness quantifier. (Contributed by GG, 1-Sep-2025.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐵 𝜓) | ||
Theorem | reueqbii 36154 | Equality inference for restricted existential uniqueness quantifier. (Contributed by GG, 1-Sep-2025.) |
⊢ 𝐴 = 𝐵 & ⊢ (𝜓 ↔ 𝜒) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐵 𝜒) | ||
Theorem | sbceqbii 36155 | Formula-building inference for class substitution. General version of sbcbii 3865. (Contributed by GG, 1-Sep-2025.) |
⊢ 𝐴 = 𝐵 & ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐵 / 𝑥]𝜓) | ||
Theorem | disjeq1i 36156 | Equality theorem for disjoint collection. Inference version. (Contributed by GG, 1-Sep-2025.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐶) | ||
Theorem | disjeq12i 36157 | Equality theorem for disjoint collection. Inference version. (Contributed by GG, 1-Sep-2025.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐷) | ||
Theorem | rabeqbii 36158 | Equality theorem for restricted class abstractions. Inference version. (Contributed by GG, 1-Sep-2025.) |
⊢ 𝐴 = 𝐵 & ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜓} | ||
Theorem | iuneq12i 36159 | Equality theorem for indexed union. Inference version. (Contributed by GG, 1-Sep-2025.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷 | ||
Theorem | iineq1i 36160 | Equality theorem for indexed intersection. Inference version. (Contributed by GG, 1-Sep-2025.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐶 | ||
Theorem | iineq12i 36161 | Equality theorem for indexed intersection. Inference version. General version of iineq1i 36160. (Contributed by GG, 1-Sep-2025.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐷 | ||
Theorem | riotaeqbii 36162 | Equivalent wff's and equal domains yield equal restricted iotas. Inference version. (Contributed by GG, 1-Sep-2025.) |
⊢ 𝐴 = 𝐵 & ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥 ∈ 𝐵 𝜓) | ||
Theorem | riotaeqi 36163 | Equal domains yield equal restricted iotas. Inference version. (Contributed by GG, 1-Sep-2025.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥 ∈ 𝐵 𝜑) | ||
Theorem | ixpeq1i 36164 | Equality inference for infinite Cartesian product. (Contributed by GG, 1-Sep-2025.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐶 | ||
Theorem | ixpeq12i 36165 | Equality inference for infinite Cartesian product. (Contributed by GG, 1-Sep-2025.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐷 | ||
Theorem | sumeq2si 36166 | Equality inference for sum. (Contributed by GG, 1-Sep-2025.) |
⊢ 𝐵 = 𝐶 ⇒ ⊢ Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶 | ||
Theorem | sumeq12si 36167 | Equality inference for sum. General version of sumeq2si 36166. (Contributed by GG, 1-Sep-2025.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ Σ𝑥 ∈ 𝐴 𝐶 = Σ𝑥 ∈ 𝐵 𝐷 | ||
Theorem | prodeq2si 36168 | Equality inference for product. (Contributed by GG, 1-Sep-2025.) |
⊢ 𝐵 = 𝐶 ⇒ ⊢ ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶 | ||
Theorem | prodeq12si 36169 | Equality inference for product. General version of prodeq2si 36168. (Contributed by GG, 1-Sep-2025.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ ∏𝑥 ∈ 𝐴 𝐶 = ∏𝑥 ∈ 𝐵 𝐷 | ||
Theorem | itgeq12i 36170 | Equality inference for an integral. General version of itgeq1i 36171 and itgeq2i 36172. (Contributed by GG, 1-Sep-2025.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ ∫𝐴𝐶 d𝑥 = ∫𝐵𝐷 d𝑥 | ||
Theorem | itgeq1i 36171 | Equality inference for an integral. (Contributed by GG, 1-Sep-2025.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ ∫𝐴𝐶 d𝑥 = ∫𝐵𝐶 d𝑥 | ||
Theorem | itgeq2i 36172 | Equality inference for an integral. (Contributed by GG, 1-Sep-2025.) |
⊢ 𝐵 = 𝐶 ⇒ ⊢ ∫𝐴𝐵 d𝑥 = ∫𝐴𝐶 d𝑥 | ||
Theorem | ditgeq123i 36173 | Equality inference for the directed integral. General version of ditgeq12i 36174 and ditgeq3i 36175. (Contributed by GG, 1-Sep-2025.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 & ⊢ 𝐸 = 𝐹 ⇒ ⊢ ⨜[𝐴 → 𝐶]𝐸 d𝑥 = ⨜[𝐵 → 𝐷]𝐹 d𝑥 | ||
Theorem | ditgeq12i 36174 | Equality inference for the directed integral. (Contributed by GG, 1-Sep-2025.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ ⨜[𝐴 → 𝐶]𝐸 d𝑥 = ⨜[𝐵 → 𝐷]𝐸 d𝑥 | ||
Theorem | ditgeq3i 36175 | Equality inference for the directed integral. (Contributed by GG, 1-Sep-2025.) |
⊢ 𝐶 = 𝐷 ⇒ ⊢ ⨜[𝐴 → 𝐵]𝐶 d𝑥 = ⨜[𝐴 → 𝐵]𝐷 d𝑥 | ||
Theorem | rmoeqdv 36176* | Formula-building rule for restricted at-most-one quantifier. Deduction form. (Contributed by GG, 1-Sep-2025.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | rmoeqbidv 36177* | Formula-building rule for restricted at-most-one quantifier. Deduction form. General version of rmobidv 3405. (Contributed by GG, 1-Sep-2025.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐵 𝜒)) | ||
Theorem | reueqdv 36178* | Formula-building rule for restricted existential uniqueness quantifier. Deduction form. (Contributed by GG, 1-Sep-2025.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | reueqbidv 36179* | Formula-building rule for restricted existential uniqueness quantifier. Deduction form. General version of reubidv 3406. (Contributed by GG, 1-Sep-2025.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐵 𝜒)) | ||
Theorem | sbequbidv 36180* | Deduction substituting both sides of a biconditional. (Contributed by GG, 1-Sep-2025.) |
⊢ (𝜑 → 𝑢 = 𝑣) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝑢 / 𝑥]𝜓 ↔ [𝑣 / 𝑥]𝜒)) | ||
Theorem | disjeq12dv 36181* | Equality theorem for disjoint collection. Deduction version. (Contributed by GG, 1-Sep-2025.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐷)) | ||
Theorem | ixpeq12dv 36182* | Equality theorem for infinite Cartesian product. Deduction version. (Contributed by GG, 1-Sep-2025.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐷) | ||
Theorem | sumeq12sdv 36183* | Equality deduction for sum. General version of sumeq2sdv 15751. (Contributed by GG, 1-Sep-2025.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐷) | ||
Theorem | prodeq12sdv 36184* | Equality deduction for product. General version of prodeq2sdv 15971. (Contributed by GG, 1-Sep-2025.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐷) | ||
Theorem | itgeq12sdv 36185* | Equality theorem for an integral. Deduction form. General version of itgeq1d 45878 and itgeq2sdv 36186. (Contributed by GG, 1-Sep-2025.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∫𝐴𝐶 d𝑥 = ∫𝐵𝐷 d𝑥) | ||
Theorem | itgeq2sdv 36186* | Equality theorem for an integral. Deduction form. (Contributed by GG, 1-Sep-2025.) |
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = ∫𝐴𝐶 d𝑥) | ||
Theorem | ditgeq123dv 36187* | Equality theorem for the directed integral. Deduction form. General version of ditgeq3sdv 36189. (Contributed by GG, 1-Sep-2025.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) & ⊢ (𝜑 → 𝐸 = 𝐹) ⇒ ⊢ (𝜑 → ⨜[𝐴 → 𝐶]𝐸 d𝑥 = ⨜[𝐵 → 𝐷]𝐹 d𝑥) | ||
Theorem | ditgeq12d 36188* | Equality theorem for the directed integral. Deduction form. (Contributed by GG, 1-Sep-2025.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ⨜[𝐴 → 𝐶]𝐸 d𝑥 = ⨜[𝐵 → 𝐷]𝐸 d𝑥) | ||
Theorem | ditgeq3sdv 36189* | Equality theorem for the directed integral. Deduction form. (Contributed by GG, 1-Sep-2025.) |
⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ⨜[𝐴 → 𝐵]𝐶 d𝑥 = ⨜[𝐴 → 𝐵]𝐷 d𝑥) | ||
Theorem | in-ax8 36190 | A proof of ax-8 2110 that does not rely on ax-8 2110. It employs df-in 3983 to perform alpha-renaming and eliminates disjoint variable conditions using ax-9 2118. Since the nature of this result is unclear, usage of this theorem is discouraged, and this method should not be applied to eliminate axiom dependencies. (Contributed by GG, 1-Aug-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧)) | ||
Theorem | ss-ax8 36191 | A proof of ax-8 2110 that does not rely on ax-8 2110. It employs df-ss 3993 to perform alpha-renaming and eliminates disjoint variable conditions using ax-9 2118. Contrary to in-ax8 36190, this proof does not rely on df-cleq 2732, therefore using fewer axioms . This method should not be applied to eliminate axiom dependencies. (Contributed by GG, 30-Aug-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧)) | ||
Theorem | cbvralvw2 36192* | Change bound variable and domain in the restricted universal quantifier, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓) | ||
Theorem | cbvrexvw2 36193* | Change bound variable and domain in the restricted existential quantifier, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜓) | ||
Theorem | cbvrmovw2 36194* | Change bound variable and domain in the restricted at-most-one quantifier, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑦 ∈ 𝐵 𝜓) | ||
Theorem | cbvreuvw2 36195* | Change bound variable and domain in the restricted existential uniqueness quantifier, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐵 𝜓) | ||
Theorem | cbvsbcvw2 36196* | Change bound variable of a class substitution using implicit substitution. General version of cbvsbcvw 3839. (Contributed by GG, 1-Sep-2025.) |
⊢ 𝐴 = 𝐵 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐵 / 𝑦]𝜓) | ||
Theorem | cbvcsbvw2 36197* | Change bound variable of a proper substitution into a class using implicit substitution. General version of cbvcsbv 3933. (Contributed by GG, 1-Sep-2025.) |
⊢ 𝐴 = 𝐵 & ⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷) ⇒ ⊢ ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑦⦌𝐷 | ||
Theorem | cbviunvw2 36198* | Change bound variable and domain in indexed unions, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷) & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) ⇒ ⊢ ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑦 ∈ 𝐵 𝐷 | ||
Theorem | cbviinvw2 36199* | Change bound variable and domain in an indexed intersection, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷) & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) ⇒ ⊢ ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑦 ∈ 𝐵 𝐷 | ||
Theorem | cbvmptvw2 36200* | Change bound variable and domain in a maps-to function, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷) & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑦 ∈ 𝐵 ↦ 𝐷) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |