| Metamath
Proof Explorer Theorem List (p. 362 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | btwnconn1lem14 36101 | Lemma for btwnconn1 36102. Final statement of the theorem when 𝐵 ≠ 𝐶. (Contributed by Scott Fenton, 9-Oct-2013.) |
| ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉))) → (𝐶 Btwn 〈𝐴, 𝐷〉 ∨ 𝐷 Btwn 〈𝐴, 𝐶〉)) | ||
| Theorem | btwnconn1 36102 | Connectitivy law for betweenness. Theorem 5.1 of [Schwabhauser] p. 39-41. (Contributed by Scott Fenton, 9-Oct-2013.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((𝐴 ≠ 𝐵 ∧ 𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉) → (𝐶 Btwn 〈𝐴, 𝐷〉 ∨ 𝐷 Btwn 〈𝐴, 𝐶〉))) | ||
| Theorem | btwnconn2 36103 | Another connectivity law for betweenness. Theorem 5.2 of [Schwabhauser] p. 41. (Contributed by Scott Fenton, 9-Oct-2013.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((𝐴 ≠ 𝐵 ∧ 𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉) → (𝐶 Btwn 〈𝐵, 𝐷〉 ∨ 𝐷 Btwn 〈𝐵, 𝐶〉))) | ||
| Theorem | btwnconn3 36104 | Inner connectivity law for betweenness. Theorem 5.3 of [Schwabhauser] p. 41. (Contributed by Scott Fenton, 9-Oct-2013.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn 〈𝐴, 𝐷〉 ∧ 𝐶 Btwn 〈𝐴, 𝐷〉) → (𝐵 Btwn 〈𝐴, 𝐶〉 ∨ 𝐶 Btwn 〈𝐴, 𝐵〉))) | ||
| Theorem | midofsegid 36105 | If two points fall in the same place in the middle of a segment, then they are identical. (Contributed by Scott Fenton, 16-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → ((𝐷 Btwn 〈𝐴, 𝐵〉 ∧ 𝐸 Btwn 〈𝐴, 𝐵〉 ∧ 〈𝐴, 𝐷〉Cgr〈𝐴, 𝐸〉) → 𝐷 = 𝐸)) | ||
| Theorem | segcon2 36106* | Generalization of axsegcon 28942. This time, we generate an endpoint for a segment on the ray 𝑄𝐴 congruent to 𝐵𝐶 and starting at 𝑄, as opposed to axsegcon 28942, where the segment starts at 𝐴 (Contributed by Scott Fenton, 14-Oct-2013.) Remove unneeded inequality. (Revised by Scott Fenton, 15-Oct-2013.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ∃𝑥 ∈ (𝔼‘𝑁)((𝐴 Btwn 〈𝑄, 𝑥〉 ∨ 𝑥 Btwn 〈𝑄, 𝐴〉) ∧ 〈𝑄, 𝑥〉Cgr〈𝐵, 𝐶〉)) | ||
| Syntax | csegle 36107 | Declare the constant for the segment less than or equal to relationship. |
| class Seg≤ | ||
| Definition | df-segle 36108* | Define the segment length comparison relationship. This relationship expresses that the segment 𝐴𝐵 is no longer than 𝐶𝐷. In this section, we establish various properties of this relationship showing that it is a transitive, reflexive relationship on pairs of points that is substitutive under congruence. Definition 5.4 of [Schwabhauser] p. 41. (Contributed by Scott Fenton, 11-Oct-2013.) |
| ⊢ Seg≤ = {〈𝑝, 𝑞〉 ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = 〈𝑎, 𝑏〉 ∧ 𝑞 = 〈𝑐, 𝑑〉 ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉))} | ||
| Theorem | brsegle 36109* | Binary relation form of the segment comparison relationship. (Contributed by Scott Fenton, 11-Oct-2013.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ↔ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) | ||
| Theorem | brsegle2 36110* | Alternate characterization of segment comparison. Theorem 5.5 of [Schwabhauser] p. 41-42. (Contributed by Scott Fenton, 11-Oct-2013.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ↔ ∃𝑥 ∈ (𝔼‘𝑁)(𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉))) | ||
| Theorem | seglecgr12im 36111 | Substitution law for segment comparison under congruence. Theorem 5.6 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 11-Oct-2013.) |
| ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → ((〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉 ∧ 〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉) → 〈𝐸, 𝐹〉 Seg≤ 〈𝐺, 𝐻〉)) | ||
| Theorem | seglecgr12 36112 | Substitution law for segment comparison under congruence. Biconditional version. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → ((〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉) → (〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ↔ 〈𝐸, 𝐹〉 Seg≤ 〈𝐺, 𝐻〉))) | ||
| Theorem | seglerflx 36113 | Segment comparison is reflexive. Theorem 5.7 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 11-Oct-2013.) |
| ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 〈𝐴, 𝐵〉 Seg≤ 〈𝐴, 𝐵〉) | ||
| Theorem | seglemin 36114 | Any segment is at least as long as a degenerate segment. Theorem 5.11 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 11-Oct-2013.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → 〈𝐴, 𝐴〉 Seg≤ 〈𝐵, 𝐶〉) | ||
| Theorem | segletr 36115 | Segment less than is transitive. Theorem 5.8 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 11-Oct-2013.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → ((〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ∧ 〈𝐶, 𝐷〉 Seg≤ 〈𝐸, 𝐹〉) → 〈𝐴, 𝐵〉 Seg≤ 〈𝐸, 𝐹〉)) | ||
| Theorem | segleantisym 36116 | Antisymmetry law for segment comparison. Theorem 5.9 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 14-Oct-2013.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ∧ 〈𝐶, 𝐷〉 Seg≤ 〈𝐴, 𝐵〉) → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉)) | ||
| Theorem | seglelin 36117 | Linearity law for segment comparison. Theorem 5.10 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 14-Oct-2013.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ∨ 〈𝐶, 𝐷〉 Seg≤ 〈𝐴, 𝐵〉)) | ||
| Theorem | btwnsegle 36118 | If 𝐵 falls between 𝐴 and 𝐶, then 𝐴𝐵 is no longer than 𝐴𝐶. (Contributed by Scott Fenton, 16-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐵 Btwn 〈𝐴, 𝐶〉 → 〈𝐴, 𝐵〉 Seg≤ 〈𝐴, 𝐶〉)) | ||
| Theorem | colinbtwnle 36119 | Given three colinear points 𝐴, 𝐵, and 𝐶, 𝐵 falls in the middle iff the two segments to 𝐵 are no longer than 𝐴𝐶. Theorem 5.12 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 Colinear 〈𝐵, 𝐶〉 → (𝐵 Btwn 〈𝐴, 𝐶〉 ↔ (〈𝐴, 𝐵〉 Seg≤ 〈𝐴, 𝐶〉 ∧ 〈𝐵, 𝐶〉 Seg≤ 〈𝐴, 𝐶〉)))) | ||
| Syntax | coutsideof 36120 | Declare the syntax for the outside of constant. |
| class OutsideOf | ||
| Definition | df-outsideof 36121 | The outside of relationship. This relationship expresses that 𝑃, 𝐴, and 𝐵 fall on a line, but 𝑃 is not on the segment 𝐴𝐵. This definition is taken from theorem 6.4 of [Schwabhauser] p. 43, since it requires no dummy variables. (Contributed by Scott Fenton, 17-Oct-2013.) |
| ⊢ OutsideOf = ( Colinear ∖ Btwn ) | ||
| Theorem | broutsideof 36122 | Binary relation form of OutsideOf. Theorem 6.4 of [Schwabhauser] p. 43. (Contributed by Scott Fenton, 17-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ (𝑃OutsideOf〈𝐴, 𝐵〉 ↔ (𝑃 Colinear 〈𝐴, 𝐵〉 ∧ ¬ 𝑃 Btwn 〈𝐴, 𝐵〉)) | ||
| Theorem | broutsideof2 36123 | Alternate form of OutsideOf. Definition 6.1 of [Schwabhauser] p. 43. (Contributed by Scott Fenton, 17-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf〈𝐴, 𝐵〉 ↔ (𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ (𝐴 Btwn 〈𝑃, 𝐵〉 ∨ 𝐵 Btwn 〈𝑃, 𝐴〉)))) | ||
| Theorem | outsidene1 36124 | Outsideness implies inequality. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf〈𝐴, 𝐵〉 → 𝐴 ≠ 𝑃)) | ||
| Theorem | outsidene2 36125 | Outsideness implies inequality. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf〈𝐴, 𝐵〉 → 𝐵 ≠ 𝑃)) | ||
| Theorem | btwnoutside 36126 | A principle linking outsideness to betweenness. Theorem 6.2 of [Schwabhauser] p. 43. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝑃 Btwn 〈𝐴, 𝐶〉) → (𝑃 Btwn 〈𝐵, 𝐶〉 ↔ 𝑃OutsideOf〈𝐴, 𝐵〉))) | ||
| Theorem | broutsideof3 36127* | Characterization of outsideness in terms of relationship to a fourth point. Theorem 6.3 of [Schwabhauser] p. 43. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf〈𝐴, 𝐵〉 ↔ (𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ ∃𝑐 ∈ (𝔼‘𝑁)(𝑐 ≠ 𝑃 ∧ 𝑃 Btwn 〈𝐴, 𝑐〉 ∧ 𝑃 Btwn 〈𝐵, 𝑐〉)))) | ||
| Theorem | outsideofrflx 36128 | Reflexivity of outsideness. Theorem 6.5 of [Schwabhauser] p. 44. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) → (𝐴 ≠ 𝑃 → 𝑃OutsideOf〈𝐴, 𝐴〉)) | ||
| Theorem | outsideofcom 36129 | Commutativity law for outsideness. Theorem 6.6 of [Schwabhauser] p. 44. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf〈𝐴, 𝐵〉 ↔ 𝑃OutsideOf〈𝐵, 𝐴〉)) | ||
| Theorem | outsideoftr 36130 | Transitivity law for outsideness. Theorem 6.7 of [Schwabhauser] p. 44. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → ((𝑃OutsideOf〈𝐴, 𝐵〉 ∧ 𝑃OutsideOf〈𝐵, 𝐶〉) → 𝑃OutsideOf〈𝐴, 𝐶〉)) | ||
| Theorem | outsideofeq 36131 | Uniqueness law for OutsideOf. Analogue of segconeq 36011. (Contributed by Scott Fenton, 24-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑋 ∈ (𝔼‘𝑁) ∧ 𝑌 ∈ (𝔼‘𝑁))) → (((𝐴OutsideOf〈𝑋, 𝑅〉 ∧ 〈𝐴, 𝑋〉Cgr〈𝐵, 𝐶〉) ∧ (𝐴OutsideOf〈𝑌, 𝑅〉 ∧ 〈𝐴, 𝑌〉Cgr〈𝐵, 𝐶〉)) → 𝑋 = 𝑌)) | ||
| Theorem | outsideofeu 36132* | Given a nondegenerate ray, there is a unique point congruent to the segment 𝐵𝐶 lying on the ray 𝐴𝑅. Theorem 6.11 of [Schwabhauser] p. 44. (Contributed by Scott Fenton, 23-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) → ∃!𝑥 ∈ (𝔼‘𝑁)(𝐴OutsideOf〈𝑥, 𝑅〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉))) | ||
| Theorem | outsidele 36133 | Relate OutsideOf to Seg≤. Theorem 6.13 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 24-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf〈𝐴, 𝐵〉 → (〈𝑃, 𝐴〉 Seg≤ 〈𝑃, 𝐵〉 ↔ 𝐴 Btwn 〈𝑃, 𝐵〉))) | ||
| Theorem | outsideofcol 36134 | Outside of implies colinearity. (Contributed by Scott Fenton, 26-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ (𝑃OutsideOf〈𝑄, 𝑅〉 → 𝑃 Colinear 〈𝑄, 𝑅〉) | ||
| Syntax | cline2 36135 | Declare the constant for the line function. |
| class Line | ||
| Syntax | cray 36136 | Declare the constant for the ray function. |
| class Ray | ||
| Syntax | clines2 36137 | Declare the constant for the set of all lines. |
| class LinesEE | ||
| Definition | df-line2 36138* | 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 36139* | 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 36140 | Define the set of all lines. Definition 6.14, part 2 of [Schwabhauser] p. 45. See ellines 36153 for membership. (Contributed by Scott Fenton, 28-Oct-2013.) |
| ⊢ LinesEE = ran Line | ||
| Theorem | funray 36141 | 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 36142* | 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 36143 | 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 36144 | 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 36145* | 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 36146 | 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 36147* | Alternate definition of a line. (Contributed by Scott Fenton, 25-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵)) → (𝐴Line𝐵) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear 〈𝐴, 𝐵〉}) | ||
| Theorem | lineunray 36148 | 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 36149 | 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 36150 | 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 36151 | 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 36152 | 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 36153* | 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 36154 | 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 36155* | 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 36156* | 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 36157* | 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 36158* | 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 36159 | Declare the syntax for the forward difference operator. |
| class △ | ||
| Definition | df-fwddif 36160* | 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 36161 | Declare the syntax for the nth forward difference operator. |
| class △n | ||
| Definition | df-fwddifn 36162* | 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 36163 | Calculate the value of the forward difference operator at a point. (Contributed by Scott Fenton, 18-May-2020.) |
| ⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → (𝑋 + 1) ∈ 𝐴) ⇒ ⊢ (𝜑 → (( △ ‘𝐹)‘𝑋) = ((𝐹‘(𝑋 + 1)) − (𝐹‘𝑋))) | ||
| Theorem | fwddifnval 36164* | 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 36165 | 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 36166* | 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 36167 | The rank of the union of two sets. Closed form of rankun 9896. (Contributed by Scott Fenton, 15-Jul-2015.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (rank‘(𝐴 ∪ 𝐵)) = ((rank‘𝐴) ∪ (rank‘𝐵))) | ||
| Theorem | ranksng 36168 | The rank of a singleton. Closed form of ranksn 9894. (Contributed by Scott Fenton, 15-Jul-2015.) |
| ⊢ (𝐴 ∈ 𝑉 → (rank‘{𝐴}) = suc (rank‘𝐴)) | ||
| Theorem | rankelg 36169 | The membership relation is inherited by the rank function. Closed form of rankel 9879. (Contributed by Scott Fenton, 16-Jul-2015.) |
| ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝐵) → (rank‘𝐴) ∈ (rank‘𝐵)) | ||
| Theorem | rankpwg 36170 | The rank of a power set. Closed form of rankpw 9883. (Contributed by Scott Fenton, 16-Jul-2015.) |
| ⊢ (𝐴 ∈ 𝑉 → (rank‘𝒫 𝐴) = suc (rank‘𝐴)) | ||
| Theorem | rank0 36171 | The rank of the empty set is ∅. (Contributed by Scott Fenton, 17-Jul-2015.) |
| ⊢ (rank‘∅) = ∅ | ||
| Theorem | rankeq1o 36172 | The only set with rank 1o is the singleton of the empty set. (Contributed by Scott Fenton, 17-Jul-2015.) |
| ⊢ ((rank‘𝐴) = 1o ↔ 𝐴 = {∅}) | ||
| Syntax | chf 36173 | The constant Hf is a class. |
| class Hf | ||
| Definition | df-hf 36174 | 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 36175* | Membership in the hereditarily finite sets. (Contributed by Scott Fenton, 9-Jul-2015.) |
| ⊢ (𝐴 ∈ Hf ↔ ∃𝑥 ∈ ω 𝐴 ∈ (𝑅1‘𝑥)) | ||
| Theorem | elhf2 36176 | Alternate form of membership in the hereditarily finite sets. (Contributed by Scott Fenton, 13-Jul-2015.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ Hf ↔ (rank‘𝐴) ∈ ω) | ||
| Theorem | elhf2g 36177 | Hereditarily finiteness via rank. Closed form of elhf2 36176. (Contributed by Scott Fenton, 15-Jul-2015.) |
| ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Hf ↔ (rank‘𝐴) ∈ ω)) | ||
| Theorem | 0hf 36178 | The empty set is a hereditarily finite set. (Contributed by Scott Fenton, 9-Jul-2015.) |
| ⊢ ∅ ∈ Hf | ||
| Theorem | hfun 36179 | The union of two HF sets is an HF set. (Contributed by Scott Fenton, 15-Jul-2015.) |
| ⊢ ((𝐴 ∈ Hf ∧ 𝐵 ∈ Hf ) → (𝐴 ∪ 𝐵) ∈ Hf ) | ||
| Theorem | hfsn 36180 | The singleton of an HF set is an HF set. (Contributed by Scott Fenton, 15-Jul-2015.) |
| ⊢ (𝐴 ∈ Hf → {𝐴} ∈ Hf ) | ||
| Theorem | hfadj 36181 | Adjoining one HF element to an HF set preserves HF status. (Contributed by Scott Fenton, 15-Jul-2015.) |
| ⊢ ((𝐴 ∈ Hf ∧ 𝐵 ∈ Hf ) → (𝐴 ∪ {𝐵}) ∈ Hf ) | ||
| Theorem | hfelhf 36182 | Any member of an HF set is itself an HF set. (Contributed by Scott Fenton, 16-Jul-2015.) |
| ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ Hf ) → 𝐴 ∈ Hf ) | ||
| Theorem | hftr 36183 | The class of all hereditarily finite sets is transitive. (Contributed by Scott Fenton, 16-Jul-2015.) |
| ⊢ Tr Hf | ||
| Theorem | hfext 36184* | Extensionality for HF sets depends only on comparison of HF elements. (Contributed by Scott Fenton, 16-Jul-2015.) |
| ⊢ ((𝐴 ∈ Hf ∧ 𝐵 ∈ Hf ) → (𝐴 = 𝐵 ↔ ∀𝑥 ∈ Hf (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))) | ||
| Theorem | hfuni 36185 | The union of an HF set is itself hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015.) |
| ⊢ (𝐴 ∈ Hf → ∪ 𝐴 ∈ Hf ) | ||
| Theorem | hfpw 36186 | The power class of an HF set is hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015.) |
| ⊢ (𝐴 ∈ Hf → 𝒫 𝐴 ∈ Hf ) | ||
| Theorem | hfninf 36187 | ω is not hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015.) |
| ⊢ ¬ ω ∈ Hf | ||
| Theorem | rmoeqi 36188 | Equality inference for restricted at-most-one quantifier. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐵 𝜓) | ||
| Theorem | rmoeqbii 36189 | Equality inference for restricted at-most-one quantifier. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 & ⊢ (𝜓 ↔ 𝜒) ⇒ ⊢ (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐵 𝜒) | ||
| Theorem | reueqi 36190 | Equality inference for restricted existential uniqueness quantifier. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐵 𝜓) | ||
| Theorem | reueqbii 36191 | Equality inference for restricted existential uniqueness quantifier. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 & ⊢ (𝜓 ↔ 𝜒) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐵 𝜒) | ||
| Theorem | sbceqbii 36192 | Formula-building inference for class substitution. General version of sbcbii 3846. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 & ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐵 / 𝑥]𝜓) | ||
| Theorem | disjeq1i 36193 | Equality theorem for disjoint collection. Inference version. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐶) | ||
| Theorem | disjeq12i 36194 | Equality theorem for disjoint collection. Inference version. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐷) | ||
| Theorem | rabeqbii 36195 | Equality theorem for restricted class abstractions. Inference version. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 & ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜓} | ||
| Theorem | iuneq12i 36196 | Equality theorem for indexed union. Inference version. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷 | ||
| Theorem | iineq1i 36197 | Equality theorem for indexed intersection. Inference version. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐶 | ||
| Theorem | iineq12i 36198 | Equality theorem for indexed intersection. Inference version. General version of iineq1i 36197. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐷 | ||
| Theorem | riotaeqbii 36199 | Equivalent wff's and equal domains yield equal restricted iotas. Inference version. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 & ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥 ∈ 𝐵 𝜓) | ||
| Theorem | riotaeqi 36200 | Equal domains yield equal restricted iotas. Inference version. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥 ∈ 𝐵 𝜑) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |