HomeTheorem List (p. 355 of 485)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 355 of 485) | < 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-30800) |
Hilbert Space Explorer
(30801-32323) |
Users' Mathboxes
(32324-48424) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | problem2 35401 | Practice problem 2. Clues: oveq12i 7431 adddiri 11259 add4i 11470 mulcli 11253 recni 11260 2re 12319 3eqtri 2757 10re 12729 5re 12332 1re 11246 4re 12329 eqcomi 2734 5p4e9 12403 oveq1i 7429 df-3 12309. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Revised by AV, 9-Sep-2021.) (Proof modification is discouraged.) |
| ⊢ (((2 · ;10) + 5) + ((1 · ;10) + 4)) = ((3 · ;10) + 9) | ||
| Theorem | problem3 35402 | Practice problem 3. Clues: eqcomi 2734 eqtri 2753 subaddrii 11581 recni 11260 4re 12329 3re 12325 1re 11246 df-4 12310 addcomi 11437. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ (𝐴 + 3) = 4 ⇒ ⊢ 𝐴 = 1 | ||
| Theorem | problem4 35403 | Practice problem 4. Clues: pm3.2i 469 eqcomi 2734 eqtri 2753 subaddrii 11581 recni 11260 7re 12338 6re 12335 ax-1cn 11198 df-7 12313 ax-mp 5 oveq1i 7429 3cn 12326 2cn 12320 df-3 12309 mullidi 11251 subdiri 11696 mp3an 1457 mulcli 11253 subadd23 11504 oveq2i 7430 oveq12i 7431 3t2e6 12411 mulcomi 11254 subcli 11568 biimpri 227 subadd2i 11580. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ (𝐴 + 𝐵) = 3 & ⊢ ((3 · 𝐴) + (2 · 𝐵)) = 7 ⇒ ⊢ (𝐴 = 1 ∧ 𝐵 = 2) | ||
| Theorem | problem5 35404 | Practice problem 5. Clues: 3brtr3i 5178 mpbi 229 breqtri 5174 ltaddsubi 11807 remulcli 11262 2re 12319 3re 12325 9re 12344 eqcomi 2734 mvlladdi 11510 3cn 6cn 12336 eqtr3i 2755 6p3e9 12405 addcomi 11437 ltdiv1ii 12176 6re 12335 nngt0i 12284 2nn 12318 divcan3i 11993 recni 11260 2cn 12320 2ne0 12349 mpbir 230 eqtri 2753 mulcomi 11254 3t2e6 12411 divmuli 12001. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ ((2 · 𝐴) + 3) < 9 ⇒ ⊢ 𝐴 < 3 | ||
| Theorem | quad3 35405 | Variant of quadratic equation with discriminant expanded. (Contributed by Filip Cernatescu, 19-Oct-2019.) |
| ⊢ 𝑋 ∈ ℂ & ⊢ 𝐴 ∈ ℂ & ⊢ 𝐴 ≠ 0 & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0 ⇒ ⊢ (𝑋 = ((-𝐵 + (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)) ∨ 𝑋 = ((-𝐵 − (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴))) | ||
| Theorem | climuzcnv 35406* | Utility lemma to convert between 𝑚 ≤ 𝑘 and 𝑘 ∈ (ℤ≥‘𝑚) in limit theorems. (Contributed by Paul Chapman, 10-Nov-2012.) |
| ⊢ (𝑚 ∈ ℕ → ((𝑘 ∈ (ℤ≥‘𝑚) → 𝜑) ↔ (𝑘 ∈ ℕ → (𝑚 ≤ 𝑘 → 𝜑)))) | ||
| Theorem | sinccvglem 35407* | ((sin‘𝑥) / 𝑥) ⇝ 1 as (real) 𝑥 ⇝ 0. (Contributed by Paul Chapman, 10-Nov-2012.) (Revised by Mario Carneiro, 21-May-2014.) |
| ⊢ (𝜑 → 𝐹:ℕ⟶(ℝ ∖ {0})) & ⊢ (𝜑 → 𝐹 ⇝ 0) & ⊢ 𝐺 = (𝑥 ∈ (ℝ ∖ {0}) ↦ ((sin‘𝑥) / 𝑥)) & ⊢ 𝐻 = (𝑥 ∈ ℂ ↦ (1 − ((𝑥↑2) / 3))) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (abs‘(𝐹‘𝑘)) < 1) ⇒ ⊢ (𝜑 → (𝐺 ∘ 𝐹) ⇝ 1) | ||
| Theorem | sinccvg 35408* | ((sin‘𝑥) / 𝑥) ⇝ 1 as (real) 𝑥 ⇝ 0. (Contributed by Paul Chapman, 10-Nov-2012.) (Proof shortened by Mario Carneiro, 21-May-2014.) |
| ⊢ ((𝐹:ℕ⟶(ℝ ∖ {0}) ∧ 𝐹 ⇝ 0) → ((𝑥 ∈ (ℝ ∖ {0}) ↦ ((sin‘𝑥) / 𝑥)) ∘ 𝐹) ⇝ 1) | ||
| Theorem | circum 35409* | The circumference of a circle of radius 𝑅, defined as the limit as 𝑛 ⇝ +∞ of the perimeter of an inscribed n-sided isogons, is ((2 · π) · 𝑅). (Contributed by Paul Chapman, 10-Nov-2012.) (Proof shortened by Mario Carneiro, 21-May-2014.) |
| ⊢ 𝐴 = ((2 · π) / 𝑛) & ⊢ 𝑃 = (𝑛 ∈ ℕ ↦ ((2 · 𝑛) · (𝑅 · (sin‘(𝐴 / 2))))) & ⊢ 𝑅 ∈ ℝ ⇒ ⊢ 𝑃 ⇝ ((2 · π) · 𝑅) | ||
| Theorem | elfzm12 35410 | Membership in a curtailed finite sequence of integers. (Contributed by Paul Chapman, 17-Nov-2012.) |
| ⊢ (𝑁 ∈ ℕ → (𝑀 ∈ (1...(𝑁 − 1)) → 𝑀 ∈ (1...𝑁))) | ||
| Theorem | nn0seqcvg 35411* | A strictly-decreasing nonnegative integer sequence with initial term 𝑁 reaches zero by the 𝑁 th term. Inference version. (Contributed by Paul Chapman, 31-Mar-2011.) |
| ⊢ 𝐹:ℕ0⟶ℕ0 & ⊢ 𝑁 = (𝐹‘0) & ⊢ (𝑘 ∈ ℕ0 → ((𝐹‘(𝑘 + 1)) ≠ 0 → (𝐹‘(𝑘 + 1)) < (𝐹‘𝑘))) ⇒ ⊢ (𝐹‘𝑁) = 0 | ||
| Theorem | lediv2aALT 35412 | Division of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Paul Chapman, 7-Sep-2007.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ (((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵) ∧ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)) → (𝐴 ≤ 𝐵 → (𝐶 / 𝐵) ≤ (𝐶 / 𝐴))) | ||
| Theorem | abs2sqlei 35413 | The absolute values of two numbers compare as their squares. (Contributed by Paul Chapman, 7-Sep-2007.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((abs‘𝐴) ≤ (abs‘𝐵) ↔ ((abs‘𝐴)↑2) ≤ ((abs‘𝐵)↑2)) | ||
| Theorem | abs2sqlti 35414 | The absolute values of two numbers compare as their squares. (Contributed by Paul Chapman, 7-Sep-2007.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((abs‘𝐴) < (abs‘𝐵) ↔ ((abs‘𝐴)↑2) < ((abs‘𝐵)↑2)) | ||
| Theorem | abs2sqle 35415 | The absolute values of two numbers compare as their squares. (Contributed by Paul Chapman, 7-Sep-2007.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((abs‘𝐴) ≤ (abs‘𝐵) ↔ ((abs‘𝐴)↑2) ≤ ((abs‘𝐵)↑2))) | ||
| Theorem | abs2sqlt 35416 | The absolute values of two numbers compare as their squares. (Contributed by Paul Chapman, 7-Sep-2007.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((abs‘𝐴) < (abs‘𝐵) ↔ ((abs‘𝐴)↑2) < ((abs‘𝐵)↑2))) | ||
| Theorem | abs2difi 35417 | Difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((abs‘𝐴) − (abs‘𝐵)) ≤ (abs‘(𝐴 − 𝐵)) | ||
| Theorem | abs2difabsi 35418 | Absolute value of difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (abs‘((abs‘𝐴) − (abs‘𝐵))) ≤ (abs‘(𝐴 − 𝐵)) | ||
| Theorem | currybi 35419 | Biconditional version of Curry's paradox. If some proposition 𝜑 amounts to the self-referential statement "This very statement is equivalent to 𝜓", then 𝜓 is true. See bj-currypara 36166 in BJ's mathbox for the classical version. (Contributed by Adrian Ducourtial, 18-Mar-2025.) |
| ⊢ ((𝜑 ↔ (𝜑 ↔ 𝜓)) → 𝜓) | ||
| Syntax | ccloneop 35420 | Syntax for the function of the class of operations on a set. |
| class CloneOp | ||
| Definition | df-cloneop 35421* | Define the function that sends a set to the class of clone-theoretic operations on the set. For convenience, we take an operation on 𝑎 to be a function on finite sequences of elements of 𝑎 (rather than tuples) with values in 𝑎. Following line 6 of [Szendrei] p. 11, the arity 𝑛 of an operation (here, the length of the sequences at which the operation is defined) is always finite and non-zero, whence 𝑛 is taken to be a non-zero finite ordinal. (Contributed by Adrian Ducourtial, 3-Apr-2025.) |
| ⊢ CloneOp = (𝑎 ∈ V ↦ {𝑥 ∣ ∃𝑛 ∈ (ω ∖ 1o)𝑥 ∈ (𝑎 ↑m (𝑎 ↑m 𝑛))}) | ||
| Syntax | cprj 35422 | Syntax for the function of projections on sets. |
| class prj | ||
| Definition | df-prj 35423* | Define the function that, for a set 𝑎, arity 𝑛, and index 𝑖, returns the 𝑖-th 𝑛-ary projection on 𝑎. This is the 𝑛-ary operation on 𝑎 that, for any sequence of 𝑛 elements of 𝑎, returns the element having index 𝑖. (Contributed by Adrian Ducourtial, 3-Apr-2025.) |
| ⊢ prj = (𝑎 ∈ V ↦ (𝑛 ∈ (ω ∖ 1o), 𝑖 ∈ 𝑛 ↦ (𝑥 ∈ (𝑎 ↑m 𝑛) ↦ (𝑥‘𝑖)))) | ||
| Syntax | csuppos 35424 | Syntax for the function of superpositions. |
| class suppos | ||
| Definition | df-suppos 35425* | Define the function that, when given an 𝑛-ary operation 𝑓 and 𝑛 many 𝑚-ary operations (𝑔‘∅), ..., (𝑔‘∪ 𝑛), returns the superposition of 𝑓 with the (𝑔‘𝑖), itself another 𝑚-ary operation on 𝑎. Given 𝑥 (a sequence of 𝑚 arguments in 𝑎), the superposition effectively applies each of the (𝑔‘𝑖) to 𝑥, then applies 𝑓 to the resulting sequence of 𝑛 function values. This can be seen as a generalized version of function composition; see paragraph 3 of [Szendrei] p. 11. (Contributed by Adrian Ducourtial, 3-Apr-2025.) |
| ⊢ suppos = (𝑎 ∈ V ↦ (𝑛 ∈ (ω ∖ 1o), 𝑚 ∈ (ω ∖ 1o) ↦ (𝑓 ∈ (𝑎 ↑m (𝑎 ↑m 𝑛)), 𝑔 ∈ ((𝑎 ↑m (𝑎 ↑m 𝑚)) ↑m 𝑛) ↦ (𝑥 ∈ (𝑎 ↑m 𝑚) ↦ (𝑓‘(𝑖 ∈ 𝑛 ↦ ((𝑔‘𝑖)‘𝑥))))))) | ||
| Theorem | axextprim 35426 | ax-ext 2696 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.) |
| ⊢ ¬ ∀𝑥 ¬ ((𝑥 ∈ 𝑦 → 𝑥 ∈ 𝑧) → ((𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦) → 𝑦 = 𝑧)) | ||
| Theorem | axrepprim 35427 | ax-rep 5286 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.) |
| ⊢ ¬ ∀𝑥 ¬ (¬ ∀𝑦 ¬ ∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧 ¬ ((∀𝑦 𝑧 ∈ 𝑥 → ¬ ∀𝑥(∀𝑧 𝑥 ∈ 𝑦 → ¬ ∀𝑦𝜑)) → ¬ (¬ ∀𝑥(∀𝑧 𝑥 ∈ 𝑦 → ¬ ∀𝑦𝜑) → ∀𝑦 𝑧 ∈ 𝑥))) | ||
| Theorem | axunprim 35428 | ax-un 7741 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.) |
| ⊢ ¬ ∀𝑥 ¬ ∀𝑦(¬ ∀𝑥(𝑦 ∈ 𝑥 → ¬ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥) | ||
| Theorem | axpowprim 35429 | ax-pow 5365 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.) |
| ⊢ (∀𝑥 ¬ ∀𝑦(∀𝑥(¬ ∀𝑧 ¬ 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥) → 𝑥 = 𝑦) | ||
| Theorem | axregprim 35430 | ax-reg 9617 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.) |
| ⊢ (𝑥 ∈ 𝑦 → ¬ ∀𝑥(𝑥 ∈ 𝑦 → ¬ ∀𝑧(𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦))) | ||
| Theorem | axinfprim 35431 | ax-inf 9663 without distinct variable conditions or defined symbols. (New usage is discouraged.) (Contributed by Scott Fenton, 13-Oct-2010.) |
| ⊢ ¬ ∀𝑥 ¬ (𝑦 ∈ 𝑧 → ¬ (𝑦 ∈ 𝑥 → ¬ ∀𝑦(𝑦 ∈ 𝑥 → ¬ ∀𝑧(𝑦 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑥)))) | ||
| Theorem | axacprim 35432 | ax-ac 10484 without distinct variable conditions or defined symbols. (New usage is discouraged.) (Contributed by Scott Fenton, 26-Oct-2010.) |
| ⊢ ¬ ∀𝑥 ¬ ∀𝑦∀𝑧(∀𝑥 ¬ (𝑦 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑤) → ¬ ∀𝑤 ¬ ∀𝑦 ¬ ((¬ ∀𝑤(𝑦 ∈ 𝑧 → (𝑧 ∈ 𝑤 → (𝑦 ∈ 𝑤 → ¬ 𝑤 ∈ 𝑥))) → 𝑦 = 𝑤) → ¬ (𝑦 = 𝑤 → ¬ ∀𝑤(𝑦 ∈ 𝑧 → (𝑧 ∈ 𝑤 → (𝑦 ∈ 𝑤 → ¬ 𝑤 ∈ 𝑥)))))) | ||
| Theorem | untelirr 35433* | We call a class "untanged" if all its members are not members of themselves. The term originates from Isbell (see citation in dfon2 35519). Using this concept, we can avoid a lot of the uses of the Axiom of Regularity. Here, we prove a series of properties of untanged classes. First, we prove that an untangled class is not a member of itself. (Contributed by Scott Fenton, 28-Feb-2011.) |
| ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝑥 → ¬ 𝐴 ∈ 𝐴) | ||
| Theorem | untuni 35434* | The union of a class is untangled iff all its members are untangled. (Contributed by Scott Fenton, 28-Feb-2011.) |
| ⊢ (∀𝑥 ∈ ∪ 𝐴 ¬ 𝑥 ∈ 𝑥 ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝑦 ¬ 𝑥 ∈ 𝑥) | ||
| Theorem | untsucf 35435* | If a class is untangled, then so is its successor. (Contributed by Scott Fenton, 28-Feb-2011.) (Revised by Mario Carneiro, 11-Dec-2016.) |
| ⊢ Ⅎ𝑦𝐴 ⇒ ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝑥 → ∀𝑦 ∈ suc 𝐴 ¬ 𝑦 ∈ 𝑦) | ||
| Theorem | unt0 35436 | The null set is untangled. (Contributed by Scott Fenton, 10-Mar-2011.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
| ⊢ ∀𝑥 ∈ ∅ ¬ 𝑥 ∈ 𝑥 | ||
| Theorem | untint 35437* | If there is an untangled element of a class, then the intersection of the class is untangled. (Contributed by Scott Fenton, 1-Mar-2011.) |
| ⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑦 → ∀𝑦 ∈ ∩ 𝐴 ¬ 𝑦 ∈ 𝑦) | ||
| Theorem | efrunt 35438* | If 𝐴 is well-founded by E, then it is untangled. (Contributed by Scott Fenton, 1-Mar-2011.) |
| ⊢ ( E Fr 𝐴 → ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝑥) | ||
| Theorem | untangtr 35439* | A transitive class is untangled iff its elements are. (Contributed by Scott Fenton, 7-Mar-2011.) |
| ⊢ (Tr 𝐴 → (∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝑥 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑦)) | ||
| Theorem | 3jaodd 35440 | Double deduction form of 3jaoi 1424. (Contributed by Scott Fenton, 20-Apr-2011.) |
| ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) & ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜂))) & ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜓 → ((𝜒 ∨ 𝜃 ∨ 𝜏) → 𝜂))) | ||
| Theorem | 3orit 35441 | Closed form of 3ori 1421. (Contributed by Scott Fenton, 20-Apr-2011.) |
| ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((¬ 𝜑 ∧ ¬ 𝜓) → 𝜒)) | ||
| Theorem | biimpexp 35442 | A biconditional in the antecedent is the same as two implications. (Contributed by Scott Fenton, 12-Dec-2010.) |
| ⊢ (((𝜑 ↔ 𝜓) → 𝜒) ↔ ((𝜑 → 𝜓) → ((𝜓 → 𝜑) → 𝜒))) | ||
| Theorem | nepss 35443 | Two classes are unequal iff their intersection is a proper subset of one of them. (Contributed by Scott Fenton, 23-Feb-2011.) |
| ⊢ (𝐴 ≠ 𝐵 ↔ ((𝐴 ∩ 𝐵) ⊊ 𝐴 ∨ (𝐴 ∩ 𝐵) ⊊ 𝐵)) | ||
| Theorem | 3ccased 35444 | Triple disjunction form of ccased 1036. (Contributed by Scott Fenton, 27-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ (𝜑 → ((𝜒 ∧ 𝜂) → 𝜓)) & ⊢ (𝜑 → ((𝜒 ∧ 𝜁) → 𝜓)) & ⊢ (𝜑 → ((𝜒 ∧ 𝜎) → 𝜓)) & ⊢ (𝜑 → ((𝜃 ∧ 𝜂) → 𝜓)) & ⊢ (𝜑 → ((𝜃 ∧ 𝜁) → 𝜓)) & ⊢ (𝜑 → ((𝜃 ∧ 𝜎) → 𝜓)) & ⊢ (𝜑 → ((𝜏 ∧ 𝜂) → 𝜓)) & ⊢ (𝜑 → ((𝜏 ∧ 𝜁) → 𝜓)) & ⊢ (𝜑 → ((𝜏 ∧ 𝜎) → 𝜓)) ⇒ ⊢ (𝜑 → (((𝜒 ∨ 𝜃 ∨ 𝜏) ∧ (𝜂 ∨ 𝜁 ∨ 𝜎)) → 𝜓)) | ||
| Theorem | dfso3 35445* | Expansion of the definition of a strict order. (Contributed by Scott Fenton, 6-Jun-2016.) |
| ⊢ (𝑅 Or 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ∧ (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) | ||
| Theorem | brtpid1 35446 | A binary relation involving unordered triples. (Contributed by Scott Fenton, 7-Jun-2016.) |
| ⊢ 𝐴{⟨𝐴, 𝐵⟩, 𝐶, 𝐷}𝐵 | ||
| Theorem | brtpid2 35447 | A binary relation involving unordered triples. (Contributed by Scott Fenton, 7-Jun-2016.) |
| ⊢ 𝐴{𝐶, ⟨𝐴, 𝐵⟩, 𝐷}𝐵 | ||
| Theorem | brtpid3 35448 | A binary relation involving unordered triples. (Contributed by Scott Fenton, 7-Jun-2016.) |
| ⊢ 𝐴{𝐶, 𝐷, ⟨𝐴, 𝐵⟩}𝐵 | ||
| Theorem | iota5f 35449* | A method for computing iota. (Contributed by Scott Fenton, 13-Dec-2017.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → (𝜓 ↔ 𝑥 = 𝐴)) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → (℩𝑥𝜓) = 𝐴) | ||
| Theorem | jath 35450 | Closed form of ja 186. Proved using the completeness script. (Proof modification is discouraged.) (Contributed by Scott Fenton, 13-Dec-2021.) |
| ⊢ ((¬ 𝜑 → 𝜒) → ((𝜓 → 𝜒) → ((𝜑 → 𝜓) → 𝜒))) | ||
| Theorem | xpab 35451* | Cartesian product of two class abstractions. (Contributed by Scott Fenton, 19-Aug-2024.) |
| ⊢ ({𝑥 ∣ 𝜑} × {𝑦 ∣ 𝜓}) = {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∧ 𝜓)} | ||
| Theorem | nnuni 35452 | The union of a finite ordinal is a finite ordinal. (Contributed by Scott Fenton, 17-Oct-2024.) |
| ⊢ (𝐴 ∈ ω → ∪ 𝐴 ∈ ω) | ||
| Theorem | sqdivzi 35453 | Distribution of square over division. (Contributed by Scott Fenton, 7-Jun-2013.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐵 ≠ 0 → ((𝐴 / 𝐵)↑2) = ((𝐴↑2) / (𝐵↑2))) | ||
| Theorem | supfz 35454 | The supremum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) |
| ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → sup((𝑀...𝑁), ℤ, < ) = 𝑁) | ||
| Theorem | inffz 35455 | The infimum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by AV, 10-Oct-2021.) |
| ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → inf((𝑀...𝑁), ℤ, < ) = 𝑀) | ||
| Theorem | fz0n 35456 | The sequence (0...(𝑁 − 1)) is empty iff 𝑁 is zero. (Contributed by Scott Fenton, 16-May-2014.) |
| ⊢ (𝑁 ∈ ℕ0 → ((0...(𝑁 − 1)) = ∅ ↔ 𝑁 = 0)) | ||
| Theorem | shftvalg 35457 | Value of a sequence shifted by 𝐴. (Contributed by Scott Fenton, 16-Dec-2017.) |
| ⊢ ((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴)‘𝐵) = (𝐹‘(𝐵 − 𝐴))) | ||
| Theorem | divcnvlin 35458* | Limit of the ratio of two linear functions. (Contributed by Scott Fenton, 17-Dec-2017.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = ((𝑘 + 𝐴) / (𝑘 + 𝐵))) ⇒ ⊢ (𝜑 → 𝐹 ⇝ 1) | ||
| Theorem | climlec3 35459* | Comparison of a constant to the limit of a sequence. (Contributed by Scott Fenton, 5-Jan-2018.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ≤ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐵) | ||
| Theorem | iexpire 35460 | i raised to itself is real. (Contributed by Scott Fenton, 13-Apr-2020.) |
| ⊢ (i↑𝑐i) ∈ ℝ | ||
| Theorem | bcneg1 35461 | The binomial coefficient over negative one is zero. (Contributed by Scott Fenton, 29-May-2020.) |
| ⊢ (𝑁 ∈ ℕ0 → (𝑁C-1) = 0) | ||
| Theorem | bcm1nt 35462 | The proportion of one binomial coefficient to another with 𝑁 decreased by 1. (Contributed by Scott Fenton, 23-Jun-2020.) |
| ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...(𝑁 − 1))) → (𝑁C𝐾) = (((𝑁 − 1)C𝐾) · (𝑁 / (𝑁 − 𝐾)))) | ||
| Theorem | bcprod 35463* | A product identity for binomial coefficients. (Contributed by Scott Fenton, 23-Jun-2020.) |
| ⊢ (𝑁 ∈ ℕ → ∏𝑘 ∈ (1...(𝑁 − 1))((𝑁 − 1)C𝑘) = ∏𝑘 ∈ (1...(𝑁 − 1))(𝑘↑((2 · 𝑘) − 𝑁))) | ||
| Theorem | bccolsum 35464* | A column-sum rule for binomial coefficients. (Contributed by Scott Fenton, 24-Jun-2020.) |
| ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0) → Σ𝑘 ∈ (0...𝑁)(𝑘C𝐶) = ((𝑁 + 1)C(𝐶 + 1))) | ||
| Theorem | iprodefisumlem 35465 | Lemma for iprodefisum 35466. (Contributed by Scott Fenton, 11-Feb-2018.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶ℂ) ⇒ ⊢ (𝜑 → seq𝑀( · , (exp ∘ 𝐹)) = (exp ∘ seq𝑀( + , 𝐹))) | ||
| Theorem | iprodefisum 35466* | Applying the exponential function to an infinite sum yields an infinite product. (Contributed by Scott Fenton, 11-Feb-2018.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝑍 (exp‘𝐵) = (exp‘Σ𝑘 ∈ 𝑍 𝐵)) | ||
| Theorem | iprodgam 35467* | An infinite product version of Euler's gamma function. (Contributed by Scott Fenton, 12-Feb-2018.) |
| ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) ⇒ ⊢ (𝜑 → (Γ‘𝐴) = (∏𝑘 ∈ ℕ (((1 + (1 / 𝑘))↑𝑐𝐴) / (1 + (𝐴 / 𝑘))) / 𝐴)) | ||
| Theorem | faclimlem1 35468* | Lemma for faclim 35471. Closed form for a particular sequence. (Contributed by Scott Fenton, 15-Dec-2017.) |
| ⊢ (𝑀 ∈ ℕ0 → seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) = (𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1)))))) | ||
| Theorem | faclimlem2 35469* | Lemma for faclim 35471. Show a limit for the inductive step. (Contributed by Scott Fenton, 15-Dec-2017.) |
| ⊢ (𝑀 ∈ ℕ0 → seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) ⇝ (𝑀 + 1)) | ||
| Theorem | faclimlem3 35470 | Lemma for faclim 35471. Algebraic manipulation for the final induction. (Contributed by Scott Fenton, 15-Dec-2017.) |
| ⊢ ((𝑀 ∈ ℕ0 ∧ 𝐵 ∈ ℕ) → (((1 + (1 / 𝐵))↑(𝑀 + 1)) / (1 + ((𝑀 + 1) / 𝐵))) = ((((1 + (1 / 𝐵))↑𝑀) / (1 + (𝑀 / 𝐵))) · (((1 + (𝑀 / 𝐵)) · (1 + (1 / 𝐵))) / (1 + ((𝑀 + 1) / 𝐵))))) | ||
| Theorem | faclim 35471* | An infinite product expression relating to factorials. Originally due to Euler. (Contributed by Scott Fenton, 22-Nov-2017.) |
| ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (((1 + (1 / 𝑛))↑𝐴) / (1 + (𝐴 / 𝑛)))) ⇒ ⊢ (𝐴 ∈ ℕ0 → seq1( · , 𝐹) ⇝ (!‘𝐴)) | ||
| Theorem | iprodfac 35472* | An infinite product expression for factorial. (Contributed by Scott Fenton, 15-Dec-2017.) |
| ⊢ (𝐴 ∈ ℕ0 → (!‘𝐴) = ∏𝑘 ∈ ℕ (((1 + (1 / 𝑘))↑𝐴) / (1 + (𝐴 / 𝑘)))) | ||
| Theorem | faclim2 35473* | Another factorial limit due to Euler. (Contributed by Scott Fenton, 17-Dec-2017.) |
| ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (((!‘𝑛) · ((𝑛 + 1)↑𝑀)) / (!‘(𝑛 + 𝑀)))) ⇒ ⊢ (𝑀 ∈ ℕ0 → 𝐹 ⇝ 1) | ||
| Theorem | gcd32 35474 | Swap the second and third arguments of a gcd. (Contributed by Scott Fenton, 8-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → ((𝐴 gcd 𝐵) gcd 𝐶) = ((𝐴 gcd 𝐶) gcd 𝐵)) | ||
| Theorem | gcdabsorb 35475 | Absorption law for gcd. (Contributed by Scott Fenton, 8-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) gcd 𝐵) = (𝐴 gcd 𝐵)) | ||
| Theorem | dftr6 35476 | A potential definition of transitivity for sets. (Contributed by Scott Fenton, 18-Mar-2012.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ (Tr 𝐴 ↔ 𝐴 ∈ (V ∖ ran (( E ∘ E ) ∖ E ))) | ||
| Theorem | coep 35477* | Composition with the membership relation. (Contributed by Scott Fenton, 18-Feb-2013.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴( E ∘ 𝑅)𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴𝑅𝑥) | ||
| Theorem | coepr 35478* | Composition with the converse membership relation. (Contributed by Scott Fenton, 18-Feb-2013.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴(𝑅 ∘ ◡ E )𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑥𝑅𝐵) | ||
| Theorem | dffr5 35479 | A quantifier-free definition of a well-founded relationship. (Contributed by Scott Fenton, 11-Apr-2011.) |
| ⊢ (𝑅 Fr 𝐴 ↔ (𝒫 𝐴 ∖ {∅}) ⊆ ran ( E ∖ ( E ∘ ◡𝑅))) | ||
| Theorem | dfso2 35480 | Quantifier-free definition of a strict order. (Contributed by Scott Fenton, 22-Feb-2013.) |
| ⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ (𝐴 × 𝐴) ⊆ (𝑅 ∪ ( I ∪ ◡𝑅)))) | ||
| Theorem | br8 35481* | Substitution for an eight-place predicate. (Contributed by Scott Fenton, 26-Sep-2013.) (Revised by Mario Carneiro, 3-May-2015.) |
| ⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑏 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑐 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ (𝑑 = 𝐷 → (𝜃 ↔ 𝜏)) & ⊢ (𝑒 = 𝐸 → (𝜏 ↔ 𝜂)) & ⊢ (𝑓 = 𝐹 → (𝜂 ↔ 𝜁)) & ⊢ (𝑔 = 𝐺 → (𝜁 ↔ 𝜎)) & ⊢ (ℎ = 𝐻 → (𝜎 ↔ 𝜌)) & ⊢ (𝑥 = 𝑋 → 𝑃 = 𝑄) & ⊢ 𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑)} ⇒ ⊢ (((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩𝑅⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ 𝜌)) | ||
| Theorem | br6 35482* | Substitution for a six-place predicate. (Contributed by Scott Fenton, 4-Oct-2013.) (Revised by Mario Carneiro, 3-May-2015.) |
| ⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑏 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑐 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ (𝑑 = 𝐷 → (𝜃 ↔ 𝜏)) & ⊢ (𝑒 = 𝐸 → (𝜏 ↔ 𝜂)) & ⊢ (𝑓 = 𝐹 → (𝜂 ↔ 𝜁)) & ⊢ (𝑥 = 𝑋 → 𝑃 = 𝑄) & ⊢ 𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑)} ⇒ ⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) → (⟨𝐴, ⟨𝐵, 𝐶⟩⟩𝑅⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ↔ 𝜁)) | ||
| Theorem | br4 35483* | Substitution for a four-place predicate. (Contributed by Scott Fenton, 9-Oct-2013.) (Revised by Mario Carneiro, 14-Oct-2013.) |
| ⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑏 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑐 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ (𝑑 = 𝐷 → (𝜃 ↔ 𝜏)) & ⊢ (𝑥 = 𝑋 → 𝑃 = 𝑄) & ⊢ 𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑)} ⇒ ⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) → (⟨𝐴, 𝐵⟩𝑅⟨𝐶, 𝐷⟩ ↔ 𝜏)) | ||
| Theorem | cnvco1 35484 | Another distributive law of converse over class composition. (Contributed by Scott Fenton, 3-May-2014.) |
| ⊢ ◡(◡𝐴 ∘ 𝐵) = (◡𝐵 ∘ 𝐴) | ||
| Theorem | cnvco2 35485 | Another distributive law of converse over class composition. (Contributed by Scott Fenton, 3-May-2014.) |
| ⊢ ◡(𝐴 ∘ ◡𝐵) = (𝐵 ∘ ◡𝐴) | ||
| Theorem | eldm3 35486 | Quantifier-free definition of membership in a domain. (Contributed by Scott Fenton, 21-Jan-2017.) |
| ⊢ (𝐴 ∈ dom 𝐵 ↔ (𝐵 ↾ {𝐴}) ≠ ∅) | ||
| Theorem | elrn3 35487 | Quantifier-free definition of membership in a range. (Contributed by Scott Fenton, 21-Jan-2017.) |
| ⊢ (𝐴 ∈ ran 𝐵 ↔ (𝐵 ∩ (V × {𝐴})) ≠ ∅) | ||
| Theorem | pocnv 35488 | The converse of a partial ordering is still a partial ordering. (Contributed by Scott Fenton, 13-Jun-2018.) |
| ⊢ (𝑅 Po 𝐴 → ◡𝑅 Po 𝐴) | ||
| Theorem | socnv 35489 | The converse of a strict ordering is still a strict ordering. (Contributed by Scott Fenton, 13-Jun-2018.) |
| ⊢ (𝑅 Or 𝐴 → ◡𝑅 Or 𝐴) | ||
| Theorem | sotrd 35490 | Transitivity law for strict orderings, deduction form. (Contributed by Scott Fenton, 24-Nov-2021.) |
| ⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ (𝜑 → 𝑍 ∈ 𝐴) & ⊢ (𝜑 → 𝑋𝑅𝑌) & ⊢ (𝜑 → 𝑌𝑅𝑍) ⇒ ⊢ (𝜑 → 𝑋𝑅𝑍) | ||
| Theorem | elintfv 35491* | Membership in an intersection of function values. (Contributed by Scott Fenton, 9-Dec-2021.) |
| ⊢ 𝑋 ∈ V ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝑋 ∈ ∩ (𝐹 “ 𝐵) ↔ ∀𝑦 ∈ 𝐵 𝑋 ∈ (𝐹‘𝑦))) | ||
| Theorem | funpsstri 35492 | A condition for subset trichotomy for functions. (Contributed by Scott Fenton, 19-Apr-2011.) |
| ⊢ ((Fun 𝐻 ∧ (𝐹 ⊆ 𝐻 ∧ 𝐺 ⊆ 𝐻) ∧ (dom 𝐹 ⊆ dom 𝐺 ∨ dom 𝐺 ⊆ dom 𝐹)) → (𝐹 ⊊ 𝐺 ∨ 𝐹 = 𝐺 ∨ 𝐺 ⊊ 𝐹)) | ||
| Theorem | fundmpss 35493 | If a class 𝐹 is a proper subset of a function 𝐺, then dom 𝐹 ⊊ dom 𝐺. (Contributed by Scott Fenton, 20-Apr-2011.) |
| ⊢ (Fun 𝐺 → (𝐹 ⊊ 𝐺 → dom 𝐹 ⊊ dom 𝐺)) | ||
| Theorem | funsseq 35494 | Given two functions with equal domains, equality only requires one direction of the subset relationship. (Contributed by Scott Fenton, 24-Apr-2012.) (Proof shortened by Mario Carneiro, 3-May-2015.) |
| ⊢ ((Fun 𝐹 ∧ Fun 𝐺 ∧ dom 𝐹 = dom 𝐺) → (𝐹 = 𝐺 ↔ 𝐹 ⊆ 𝐺)) | ||
| Theorem | fununiq 35495 | The uniqueness condition of functions. (Contributed by Scott Fenton, 18-Feb-2013.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (Fun 𝐹 → ((𝐴𝐹𝐵 ∧ 𝐴𝐹𝐶) → 𝐵 = 𝐶)) | ||
| Theorem | funbreq 35496 | An equality condition for functions. (Contributed by Scott Fenton, 18-Feb-2013.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ ((Fun 𝐹 ∧ 𝐴𝐹𝐵) → (𝐴𝐹𝐶 ↔ 𝐵 = 𝐶)) | ||
| Theorem | br1steq 35497 | Uniqueness condition for the binary relation 1st. (Contributed by Scott Fenton, 11-Apr-2014.) (Proof shortened by Mario Carneiro, 3-May-2015.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (⟨𝐴, 𝐵⟩1st 𝐶 ↔ 𝐶 = 𝐴) | ||
| Theorem | br2ndeq 35498 | Uniqueness condition for the binary relation 2nd. (Contributed by Scott Fenton, 11-Apr-2014.) (Proof shortened by Mario Carneiro, 3-May-2015.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (⟨𝐴, 𝐵⟩2nd 𝐶 ↔ 𝐶 = 𝐵) | ||
| Theorem | dfdm5 35499 | Definition of domain in terms of 1st and image. (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
| ⊢ dom 𝐴 = ((1st ↾ (V × V)) “ 𝐴) | ||
| Theorem | dfrn5 35500 | Definition of range in terms of 2nd and image. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
| ⊢ ran 𝐴 = ((2nd ↾ (V × V)) “ 𝐴) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |