| Metamath
Proof Explorer Theorem List (p. 71 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 | fvun2 7001 | The value of a union when the argument is in the second domain. (Contributed by Scott Fenton, 29-Jun-2013.) |
| ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐵)) → ((𝐹 ∪ 𝐺)‘𝑋) = (𝐺‘𝑋)) | ||
| Theorem | fvun1d 7002 | The value of a union when the argument is in the first domain, a deduction version. (Contributed by metakunt, 28-May-2024.) |
| ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) ⇒ ⊢ (𝜑 → ((𝐹 ∪ 𝐺)‘𝑋) = (𝐹‘𝑋)) | ||
| Theorem | fvun2d 7003 | The value of a union when the argument is in the second domain, a deduction version. (Contributed by metakunt, 28-May-2024.) |
| ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝐹 ∪ 𝐺)‘𝑋) = (𝐺‘𝑋)) | ||
| Theorem | dffv2 7004 | Alternate definition of function value df-fv 6569 that doesn't require dummy variables. (Contributed by NM, 4-Aug-2010.) |
| ⊢ (𝐹‘𝐴) = ∪ ((𝐹 “ {𝐴}) ∖ ∪ ∪ (((𝐹 ↾ {𝐴}) ∘ ◡(𝐹 ↾ {𝐴})) ∖ I )) | ||
| Theorem | dmfco 7005 | Domains of a function composition. (Contributed by NM, 27-Jan-1997.) |
| ⊢ ((Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺) → (𝐴 ∈ dom (𝐹 ∘ 𝐺) ↔ (𝐺‘𝐴) ∈ dom 𝐹)) | ||
| Theorem | fvco2 7006 | Value of a function composition. Similar to second part of Theorem 3H of [Enderton] p. 47. (Contributed by NM, 9-Oct-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) (Revised by Stefan O'Rear, 16-Oct-2014.) |
| ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘ 𝐺)‘𝑋) = (𝐹‘(𝐺‘𝑋))) | ||
| Theorem | fvco 7007 | Value of a function composition. Similar to Exercise 5 of [TakeutiZaring] p. 28. (Contributed by NM, 22-Apr-2006.) (Proof shortened by Mario Carneiro, 26-Dec-2014.) |
| ⊢ ((Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺) → ((𝐹 ∘ 𝐺)‘𝐴) = (𝐹‘(𝐺‘𝐴))) | ||
| Theorem | fvco3 7008 | Value of a function composition. (Contributed by NM, 3-Jan-2004.) (Revised by Mario Carneiro, 26-Dec-2014.) |
| ⊢ ((𝐺:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → ((𝐹 ∘ 𝐺)‘𝐶) = (𝐹‘(𝐺‘𝐶))) | ||
| Theorem | fvco3d 7009 | Value of a function composition. Deduction form of fvco3 7008. (Contributed by Stanislas Polu, 9-Mar-2020.) |
| ⊢ (𝜑 → 𝐺:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) ⇒ ⊢ (𝜑 → ((𝐹 ∘ 𝐺)‘𝐶) = (𝐹‘(𝐺‘𝐶))) | ||
| Theorem | fvco4i 7010 | Conditions for a composition to be expandable without conditions on the argument. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
| ⊢ ∅ = (𝐹‘∅) & ⊢ Fun 𝐺 ⇒ ⊢ ((𝐹 ∘ 𝐺)‘𝑋) = (𝐹‘(𝐺‘𝑋)) | ||
| Theorem | fvopab3g 7011* | Value of a function given by ordered-pair class abstraction. (Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro, 28-Apr-2015.) |
| ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 ∈ 𝐶 → ∃!𝑦𝜑) & ⊢ 𝐹 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐶 ∧ 𝜑)} ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ((𝐹‘𝐴) = 𝐵 ↔ 𝜒)) | ||
| Theorem | fvopab3ig 7012* | Value of a function given by ordered-pair class abstraction. (Contributed by NM, 23-Oct-1999.) |
| ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 ∈ 𝐶 → ∃*𝑦𝜑) & ⊢ 𝐹 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐶 ∧ 𝜑)} ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝜒 → (𝐹‘𝐴) = 𝐵)) | ||
| Theorem | brfvopabrbr 7013* | The binary relation of a function value which is an ordered-pair class abstraction of a restricted binary relation is the restricted binary relation. The first hypothesis can often be obtained by using fvmptopab 7487. (Contributed by AV, 29-Oct-2021.) |
| ⊢ (𝐴‘𝑍) = {〈𝑥, 𝑦〉 ∣ (𝑥(𝐵‘𝑍)𝑦 ∧ 𝜑)} & ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → (𝜑 ↔ 𝜓)) & ⊢ Rel (𝐵‘𝑍) ⇒ ⊢ (𝑋(𝐴‘𝑍)𝑌 ↔ (𝑋(𝐵‘𝑍)𝑌 ∧ 𝜓)) | ||
| Theorem | fvmptg 7014* | Value of a function given in maps-to notation. (Contributed by NM, 2-Oct-2007.) (Revised by Mario Carneiro, 31-Aug-2015.) |
| ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) & ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) ⇒ ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅) → (𝐹‘𝐴) = 𝐶) | ||
| Theorem | fvmpti 7015* | Value of a function given in maps-to notation. (Contributed by Mario Carneiro, 23-Apr-2014.) |
| ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) & ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) ⇒ ⊢ (𝐴 ∈ 𝐷 → (𝐹‘𝐴) = ( I ‘𝐶)) | ||
| Theorem | fvmpt 7016* | Value of a function given in maps-to notation. (Contributed by NM, 17-Aug-2011.) |
| ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) & ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) & ⊢ 𝐶 ∈ V ⇒ ⊢ (𝐴 ∈ 𝐷 → (𝐹‘𝐴) = 𝐶) | ||
| Theorem | fvmpt2f 7017 | Value of a function given by the maps-to notation. (Contributed by Thierry Arnoux, 9-Mar-2017.) |
| ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵) | ||
| Theorem | fvtresfn 7018* | Functionality of a tuple-restriction function. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝑥 ↾ 𝑉)) ⇒ ⊢ (𝑋 ∈ 𝐵 → (𝐹‘𝑋) = (𝑋 ↾ 𝑉)) | ||
| Theorem | fvmpts 7019* | Value of a function given in maps-to notation, using explicit class substitution. (Contributed by Scott Fenton, 17-Jul-2013.) (Revised by Mario Carneiro, 31-Aug-2015.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐶 ↦ 𝐵) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ ⦋𝐴 / 𝑥⦌𝐵 ∈ 𝑉) → (𝐹‘𝐴) = ⦋𝐴 / 𝑥⦌𝐵) | ||
| Theorem | fvmpt3 7020* | Value of a function given in maps-to notation, with a slightly different sethood condition. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
| ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) & ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) & ⊢ (𝑥 ∈ 𝐷 → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝐴 ∈ 𝐷 → (𝐹‘𝐴) = 𝐶) | ||
| Theorem | fvmpt3i 7021* | Value of a function given in maps-to notation, with a slightly different sethood condition. (Contributed by Mario Carneiro, 11-Sep-2015.) |
| ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) & ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∈ 𝐷 → (𝐹‘𝐴) = 𝐶) | ||
| Theorem | fvmptdf 7022* | Deduction version of fvmptd 7023 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by AV, 29-Mar-2024.) |
| ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐶 ⇒ ⊢ (𝜑 → (𝐹‘𝐴) = 𝐶) | ||
| Theorem | fvmptd 7023* | Deduction version of fvmpt 7016. (Contributed by Scott Fenton, 18-Feb-2013.) (Revised by Mario Carneiro, 31-Aug-2015.) (Proof shortened by AV, 29-Mar-2024.) |
| ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐹‘𝐴) = 𝐶) | ||
| Theorem | fvmptd2 7024* | Deduction version of fvmpt 7016 (where the definition of the mapping does not depend on the common antecedent 𝜑). (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐹‘𝐴) = 𝐶) | ||
| Theorem | mptrcl 7025* | Reverse closure for a mapping: If the function value of a mapping has a member, the argument belongs to the base class of the mapping. (Contributed by AV, 4-Apr-2020.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝐼 ∈ (𝐹‘𝑋) → 𝑋 ∈ 𝐴) | ||
| Theorem | fvmpt2i 7026* | Value of a function given by the maps-to notation. (Contributed by Mario Carneiro, 23-Apr-2014.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝑥 ∈ 𝐴 → (𝐹‘𝑥) = ( I ‘𝐵)) | ||
| Theorem | fvmpt2 7027* | Value of a function given by the maps-to notation. (Contributed by FL, 21-Jun-2010.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐹‘𝑥) = 𝐵) | ||
| Theorem | fvmptss 7028* | If all the values of the mapping are subsets of a class 𝐶, then so is any evaluation of the mapping, even if 𝐷 is not in the base set 𝐴. (Contributed by Mario Carneiro, 13-Feb-2015.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → (𝐹‘𝐷) ⊆ 𝐶) | ||
| Theorem | fvmpt2d 7029* | Deduction version of fvmpt2 7027. (Contributed by Thierry Arnoux, 8-Dec-2016.) |
| ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵) | ||
| Theorem | fvmptex 7030* | Express a function 𝐹 whose value 𝐵 may not always be a set in terms of another function 𝐺 for which sethood is guaranteed. (Note that ( I ‘𝐵) is just shorthand for if(𝐵 ∈ V, 𝐵, ∅), and it is always a set by fvex 6919.) Note also that these functions are not the same; wherever 𝐵(𝐶) is not a set, 𝐶 is not in the domain of 𝐹 (so it evaluates to the empty set), but 𝐶 is in the domain of 𝐺, and 𝐺(𝐶) is defined to be the empty set. (Contributed by Mario Carneiro, 14-Jul-2013.) (Revised by Mario Carneiro, 23-Apr-2014.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ ( I ‘𝐵)) ⇒ ⊢ (𝐹‘𝐶) = (𝐺‘𝐶) | ||
| Theorem | fvmptd3f 7031* | Alternate deduction version of fvmpt 7016 with three nonfreeness hypotheses instead of distinct variable conditions. (Contributed by AV, 19-Jan-2022.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → ((𝐹‘𝐴) = 𝐵 → 𝜓)) & ⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (𝜑 → (𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) → 𝜓)) | ||
| Theorem | fvmptd2f 7032* | Alternate deduction version of fvmpt 7016, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.) (Proof shortened by AV, 19-Jan-2022.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → ((𝐹‘𝐴) = 𝐵 → 𝜓)) & ⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (𝜑 → (𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) → 𝜓)) | ||
| Theorem | fvmptdv 7033* | Alternate deduction version of fvmpt 7016, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → ((𝐹‘𝐴) = 𝐵 → 𝜓)) ⇒ ⊢ (𝜑 → (𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) → 𝜓)) | ||
| Theorem | fvmptdv2 7034* | Alternate deduction version of fvmpt 7016, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) → (𝐹‘𝐴) = 𝐶)) | ||
| Theorem | mpteqb 7035* | Bidirectional equality theorem for a mapping abstraction. Equivalent to eqfnfv 7051. (Contributed by Mario Carneiro, 14-Nov-2014.) |
| ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ((𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶) ↔ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶)) | ||
| Theorem | fvmptt 7036* | Closed theorem form of fvmpt 7016. (Contributed by Scott Fenton, 21-Feb-2013.) (Revised by Mario Carneiro, 11-Sep-2015.) |
| ⊢ ((∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) ∧ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) ∧ (𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉)) → (𝐹‘𝐴) = 𝐶) | ||
| Theorem | fvmptf 7037* | Value of a function given by an ordered-pair class abstraction. This version of fvmptg 7014 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 8-Nov-2005.) (Revised by Mario Carneiro, 15-Oct-2016.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) & ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) ⇒ ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉) → (𝐹‘𝐴) = 𝐶) | ||
| Theorem | fvmptnf 7038* | The value of a function given by an ordered-pair class abstraction is the empty set when the class it would otherwise map to is a proper class. This version of fvmptn 7041 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 21-Oct-2003.) (Revised by Mario Carneiro, 11-Sep-2015.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) & ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) ⇒ ⊢ (¬ 𝐶 ∈ V → (𝐹‘𝐴) = ∅) | ||
| Theorem | fvmptd3 7039* | Deduction version of fvmpt 7016. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐹‘𝐴) = 𝐶) | ||
| Theorem | fvmptd4 7040* | Deduction version of fvmpt 7016 (where the substitution hypothesis does not have the antecedent 𝜑). (Contributed by SN, 26-Jul-2024.) |
| ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)) & ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐹‘𝐴) = 𝐶) | ||
| Theorem | fvmptn 7041* | This somewhat non-intuitive theorem tells us the value of its function is the empty set when the class 𝐶 it would otherwise map to is a proper class. This is a technical lemma that can help eliminate redundant sethood antecedents otherwise required by fvmptg 7014. (Contributed by NM, 21-Oct-2003.) (Revised by Mario Carneiro, 9-Sep-2013.) |
| ⊢ (𝑥 = 𝐷 → 𝐵 = 𝐶) & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (¬ 𝐶 ∈ V → (𝐹‘𝐷) = ∅) | ||
| Theorem | fvmptss2 7042* | A mapping always evaluates to a subset of the substituted expression in the mapping, even if this is a proper class, or we are out of the domain. (Contributed by Mario Carneiro, 13-Feb-2015.) |
| ⊢ (𝑥 = 𝐷 → 𝐵 = 𝐶) & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝐹‘𝐷) ⊆ 𝐶 | ||
| Theorem | elfvmptrab1w 7043* | Implications for the value of a function defined by the maps-to notation with a class abstraction as a result having an element. Here, the base set of the class abstraction depends on the argument of the function. Version of elfvmptrab1 7044 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by Alexander van der Vekens, 15-Jul-2018.) Avoid ax-13 2377. (Revised by GG, 26-Jan-2024.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∈ ⦋𝑥 / 𝑚⦌𝑀 ∣ 𝜑}) & ⊢ (𝑋 ∈ 𝑉 → ⦋𝑋 / 𝑚⦌𝑀 ∈ V) ⇒ ⊢ (𝑌 ∈ (𝐹‘𝑋) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ ⦋𝑋 / 𝑚⦌𝑀)) | ||
| Theorem | elfvmptrab1 7044* | Implications for the value of a function defined by the maps-to notation with a class abstraction as a result having an element. Here, the base set of the class abstraction depends on the argument of the function. Usage of this theorem is discouraged because it depends on ax-13 2377. Use the weaker elfvmptrab1w 7043 when possible. (Contributed by Alexander van der Vekens, 15-Jul-2018.) (New usage is discouraged.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∈ ⦋𝑥 / 𝑚⦌𝑀 ∣ 𝜑}) & ⊢ (𝑋 ∈ 𝑉 → ⦋𝑋 / 𝑚⦌𝑀 ∈ V) ⇒ ⊢ (𝑌 ∈ (𝐹‘𝑋) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ ⦋𝑋 / 𝑚⦌𝑀)) | ||
| Theorem | elfvmptrab 7045* | Implications for the value of a function defined by the maps-to notation with a class abstraction as a result having an element. (Contributed by Alexander van der Vekens, 15-Jul-2018.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∈ 𝑀 ∣ 𝜑}) & ⊢ (𝑋 ∈ 𝑉 → 𝑀 ∈ V) ⇒ ⊢ (𝑌 ∈ (𝐹‘𝑋) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑀)) | ||
| Theorem | fvopab4ndm 7046* | Value of a function given by an ordered-pair class abstraction, outside of its domain. (Contributed by NM, 28-Mar-2008.) |
| ⊢ 𝐹 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⇒ ⊢ (¬ 𝐵 ∈ 𝐴 → (𝐹‘𝐵) = ∅) | ||
| Theorem | fvmptndm 7047* | Value of a function given by the maps-to notation, outside of its domain. (Contributed by AV, 31-Dec-2020.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (¬ 𝑋 ∈ 𝐴 → (𝐹‘𝑋) = ∅) | ||
| Theorem | fvmptrabfv 7048* | Value of a function mapping a set to a class abstraction restricting the value of another function. (Contributed by AV, 18-Feb-2022.) |
| ⊢ 𝐹 = (𝑥 ∈ V ↦ {𝑦 ∈ (𝐺‘𝑥) ∣ 𝜑}) & ⊢ (𝑥 = 𝑋 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐹‘𝑋) = {𝑦 ∈ (𝐺‘𝑋) ∣ 𝜓} | ||
| Theorem | fvopab5 7049* | The value of a function that is expressed as an ordered pair abstraction. (Contributed by NM, 19-Feb-2006.) (Revised by Mario Carneiro, 11-Sep-2015.) |
| ⊢ 𝐹 = {〈𝑥, 𝑦〉 ∣ 𝜑} & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐹‘𝐴) = (℩𝑦𝜓)) | ||
| Theorem | fvopab6 7050* | Value of a function given by ordered-pair class abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 11-Sep-2015.) |
| ⊢ 𝐹 = {〈𝑥, 𝑦〉 ∣ (𝜑 ∧ 𝑦 = 𝐵)} & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅 ∧ 𝜓) → (𝐹‘𝐴) = 𝐶) | ||
| Theorem | eqfnfv 7051* | Equality of functions is determined by their values. Special case of Exercise 4 of [TakeutiZaring] p. 28 (with domain equality omitted). (Contributed by NM, 3-Aug-1994.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) (Proof shortened by Mario Carneiro, 31-Aug-2015.) |
| ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))) | ||
| Theorem | eqfnfv2 7052* | Equality of functions is determined by their values. Exercise 4 of [TakeutiZaring] p. 28. (Contributed by NM, 3-Aug-1994.) (Revised by Mario Carneiro, 31-Aug-2015.) |
| ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → (𝐹 = 𝐺 ↔ (𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))) | ||
| Theorem | eqfnfv3 7053* | Derive equality of functions from equality of their values. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → (𝐹 = 𝐺 ↔ (𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝐵 ∧ (𝐹‘𝑥) = (𝐺‘𝑥))))) | ||
| Theorem | eqfnfvd 7054* | Deduction for equality of functions. (Contributed by Mario Carneiro, 24-Jul-2014.) |
| ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = (𝐺‘𝑥)) ⇒ ⊢ (𝜑 → 𝐹 = 𝐺) | ||
| Theorem | eqfnfv2f 7055* | Equality of functions is determined by their values. Special case of Exercise 4 of [TakeutiZaring] p. 28 (with domain equality omitted). This version of eqfnfv 7051 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 29-Jan-2004.) |
| ⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝐺 ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))) | ||
| Theorem | eqfunfv 7056* | Equality of functions is determined by their values. (Contributed by Scott Fenton, 19-Jun-2011.) |
| ⊢ ((Fun 𝐹 ∧ Fun 𝐺) → (𝐹 = 𝐺 ↔ (dom 𝐹 = dom 𝐺 ∧ ∀𝑥 ∈ dom 𝐹(𝐹‘𝑥) = (𝐺‘𝑥)))) | ||
| Theorem | eqfnun 7057 | Two functions on 𝐴 ∪ 𝐵 are equal if and only if they have equal restrictions to both 𝐴 and 𝐵. (Contributed by Jeff Madsen, 19-Jun-2011.) |
| ⊢ ((𝐹 Fn (𝐴 ∪ 𝐵) ∧ 𝐺 Fn (𝐴 ∪ 𝐵)) → (𝐹 = 𝐺 ↔ ((𝐹 ↾ 𝐴) = (𝐺 ↾ 𝐴) ∧ (𝐹 ↾ 𝐵) = (𝐺 ↾ 𝐵)))) | ||
| Theorem | fvreseq0 7058* | Equality of restricted functions is determined by their values (for functions with different domains). (Contributed by AV, 6-Jan-2019.) |
| ⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐶) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ⊆ 𝐶)) → ((𝐹 ↾ 𝐵) = (𝐺 ↾ 𝐵) ↔ ∀𝑥 ∈ 𝐵 (𝐹‘𝑥) = (𝐺‘𝑥))) | ||
| Theorem | fvreseq1 7059* | Equality of a function restricted to the domain of another function. (Contributed by AV, 6-Jan-2019.) |
| ⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ 𝐵 ⊆ 𝐴) → ((𝐹 ↾ 𝐵) = 𝐺 ↔ ∀𝑥 ∈ 𝐵 (𝐹‘𝑥) = (𝐺‘𝑥))) | ||
| Theorem | fvreseq 7060* | Equality of restricted functions is determined by their values. (Contributed by NM, 3-Aug-1994.) (Proof shortened by AV, 4-Mar-2019.) |
| ⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ 𝐵 ⊆ 𝐴) → ((𝐹 ↾ 𝐵) = (𝐺 ↾ 𝐵) ↔ ∀𝑥 ∈ 𝐵 (𝐹‘𝑥) = (𝐺‘𝑥))) | ||
| Theorem | fnmptfvd 7061* | A function with a given domain is a mapping defined by its function values. (Contributed by AV, 1-Mar-2019.) |
| ⊢ (𝜑 → 𝑀 Fn 𝐴) & ⊢ (𝑖 = 𝑎 → 𝐷 = 𝐶) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → 𝐷 ∈ 𝑈) & ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑀 = (𝑎 ∈ 𝐴 ↦ 𝐶) ↔ ∀𝑖 ∈ 𝐴 (𝑀‘𝑖) = 𝐷)) | ||
| Theorem | fndmdif 7062* | Two ways to express the locus of differences between two functions. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
| ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → dom (𝐹 ∖ 𝐺) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ≠ (𝐺‘𝑥)}) | ||
| Theorem | fndmdifcom 7063 | The difference set between two functions is commutative. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
| ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → dom (𝐹 ∖ 𝐺) = dom (𝐺 ∖ 𝐹)) | ||
| Theorem | fndmdifeq0 7064 | The difference set of two functions is empty if and only if the functions are equal. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
| ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (dom (𝐹 ∖ 𝐺) = ∅ ↔ 𝐹 = 𝐺)) | ||
| Theorem | fndmin 7065* | Two ways to express the locus of equality between two functions. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
| ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → dom (𝐹 ∩ 𝐺) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) = (𝐺‘𝑥)}) | ||
| Theorem | fneqeql 7066 | Two functions are equal iff their equalizer is the whole domain. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
| ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ dom (𝐹 ∩ 𝐺) = 𝐴)) | ||
| Theorem | fneqeql2 7067 | Two functions are equal iff their equalizer contains the whole domain. (Contributed by Stefan O'Rear, 9-Mar-2015.) |
| ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ 𝐴 ⊆ dom (𝐹 ∩ 𝐺))) | ||
| Theorem | fnreseql 7068 | Two functions are equal on a subset iff their equalizer contains that subset. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
| ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ∧ 𝑋 ⊆ 𝐴) → ((𝐹 ↾ 𝑋) = (𝐺 ↾ 𝑋) ↔ 𝑋 ⊆ dom (𝐹 ∩ 𝐺))) | ||
| Theorem | chfnrn 7069* | The range of a choice function (a function that chooses an element from each member of its domain) is included in the union of its domain. (Contributed by NM, 31-Aug-1999.) |
| ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝑥) → ran 𝐹 ⊆ ∪ 𝐴) | ||
| Theorem | funfvop 7070 | Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1] p. 41. (Contributed by NM, 14-Oct-1996.) |
| ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → 〈𝐴, (𝐹‘𝐴)〉 ∈ 𝐹) | ||
| Theorem | funfvbrb 7071 | Two ways to say that 𝐴 is in the domain of 𝐹. (Contributed by Mario Carneiro, 1-May-2014.) |
| ⊢ (Fun 𝐹 → (𝐴 ∈ dom 𝐹 ↔ 𝐴𝐹(𝐹‘𝐴))) | ||
| Theorem | fvimacnvi 7072 | A member of a preimage is a function value argument. (Contributed by NM, 4-May-2007.) |
| ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ (◡𝐹 “ 𝐵)) → (𝐹‘𝐴) ∈ 𝐵) | ||
| Theorem | fvimacnv 7073 | The argument of a function value belongs to the preimage of any class containing the function value. Raph Levien remarks: "This proof is unsatisfying, because it seems to me that funimass2 6649 could probably be strengthened to a biconditional." (Contributed by Raph Levien, 20-Nov-2006.) |
| ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → ((𝐹‘𝐴) ∈ 𝐵 ↔ 𝐴 ∈ (◡𝐹 “ 𝐵))) | ||
| Theorem | funimass3 7074 | A kind of contraposition law that infers an image subclass from a subclass of a preimage. Raph Levien remarks: "Likely this could be proved directly, and fvimacnv 7073 would be the special case of 𝐴 being a singleton, but it works this way round too." (Contributed by Raph Levien, 20-Nov-2006.) |
| ⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → ((𝐹 “ 𝐴) ⊆ 𝐵 ↔ 𝐴 ⊆ (◡𝐹 “ 𝐵))) | ||
| Theorem | funimass5 7075* | A subclass of a preimage in terms of function values. (Contributed by NM, 15-May-2007.) |
| ⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐴 ⊆ (◡𝐹 “ 𝐵) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) | ||
| Theorem | funconstss 7076* | Two ways of specifying that a function is constant on a subdomain. (Contributed by NM, 8-Mar-2007.) |
| ⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵 ↔ 𝐴 ⊆ (◡𝐹 “ {𝐵}))) | ||
| Theorem | fvimacnvALT 7077 | Alternate proof of fvimacnv 7073, based on funimass3 7074. If funimass3 7074 is ever proved directly, as opposed to using funimacnv 6647 pointwise, then the proof of funimacnv 6647 should be replaced with this one. (Contributed by Raph Levien, 20-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → ((𝐹‘𝐴) ∈ 𝐵 ↔ 𝐴 ∈ (◡𝐹 “ 𝐵))) | ||
| Theorem | elpreima 7078 | Membership in the preimage of a set under a function. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) ↔ (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶))) | ||
| Theorem | elpreimad 7079 | Membership in the preimage of a set under a function. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ (𝜑 → (𝐹‘𝐵) ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐵 ∈ (◡𝐹 “ 𝐶)) | ||
| Theorem | fniniseg 7080 | Membership in the preimage of a singleton, under a function. (Contributed by Mario Carneiro, 12-May-2014.) (Proof shortened by Mario Carneiro , 28-Apr-2015.) |
| ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵))) | ||
| Theorem | fncnvima2 7081* | Inverse images under functions expressed as abstractions. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
| ⊢ (𝐹 Fn 𝐴 → (◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ∈ 𝐵}) | ||
| Theorem | fniniseg2 7082* | Inverse point images under functions expressed as abstractions. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
| ⊢ (𝐹 Fn 𝐴 → (◡𝐹 “ {𝐵}) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) = 𝐵}) | ||
| Theorem | unpreima 7083 | Preimage of a union. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ (Fun 𝐹 → (◡𝐹 “ (𝐴 ∪ 𝐵)) = ((◡𝐹 “ 𝐴) ∪ (◡𝐹 “ 𝐵))) | ||
| Theorem | inpreima 7084 | Preimage of an intersection. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 14-Jun-2016.) |
| ⊢ (Fun 𝐹 → (◡𝐹 “ (𝐴 ∩ 𝐵)) = ((◡𝐹 “ 𝐴) ∩ (◡𝐹 “ 𝐵))) | ||
| Theorem | difpreima 7085 | Preimage of a difference. (Contributed by Mario Carneiro, 14-Jun-2016.) |
| ⊢ (Fun 𝐹 → (◡𝐹 “ (𝐴 ∖ 𝐵)) = ((◡𝐹 “ 𝐴) ∖ (◡𝐹 “ 𝐵))) | ||
| Theorem | respreima 7086 | The preimage of a restricted function. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ (Fun 𝐹 → (◡(𝐹 ↾ 𝐵) “ 𝐴) = ((◡𝐹 “ 𝐴) ∩ 𝐵)) | ||
| Theorem | cnvimainrn 7087 | The preimage of the intersection of the range of a class and a class 𝐴 is the preimage of the class 𝐴. (Contributed by AV, 17-Sep-2024.) |
| ⊢ (Fun 𝐹 → (◡𝐹 “ (ran 𝐹 ∩ 𝐴)) = (◡𝐹 “ 𝐴)) | ||
| Theorem | sspreima 7088 | The preimage of a subset is a subset of the preimage. (Contributed by Brendan Leahy, 23-Sep-2017.) |
| ⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ 𝐵) → (◡𝐹 “ 𝐴) ⊆ (◡𝐹 “ 𝐵)) | ||
| Theorem | iinpreima 7089* | Preimage of an intersection. (Contributed by FL, 16-Apr-2012.) |
| ⊢ ((Fun 𝐹 ∧ 𝐴 ≠ ∅) → (◡𝐹 “ ∩ 𝑥 ∈ 𝐴 𝐵) = ∩ 𝑥 ∈ 𝐴 (◡𝐹 “ 𝐵)) | ||
| Theorem | intpreima 7090* | Preimage of an intersection. (Contributed by FL, 28-Apr-2012.) |
| ⊢ ((Fun 𝐹 ∧ 𝐴 ≠ ∅) → (◡𝐹 “ ∩ 𝐴) = ∩ 𝑥 ∈ 𝐴 (◡𝐹 “ 𝑥)) | ||
| Theorem | fimacnvinrn 7091 | Taking the converse image of a set can be limited to the range of the function used. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
| ⊢ (Fun 𝐹 → (◡𝐹 “ 𝐴) = (◡𝐹 “ (𝐴 ∩ ran 𝐹))) | ||
| Theorem | fimacnvinrn2 7092 | Taking the converse image of a set can be limited to the range of the function used. (Contributed by Thierry Arnoux, 17-Feb-2017.) |
| ⊢ ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝐵) → (◡𝐹 “ 𝐴) = (◡𝐹 “ (𝐴 ∩ 𝐵))) | ||
| Theorem | rescnvimafod 7093 | The restriction of a function to a preimage of a class is a function onto the intersection of this class and the range of the function. (Contributed by AV, 13-Sep-2024.) (Revised by AV, 29-Sep-2024.) |
| ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐸 = (ran 𝐹 ∩ 𝐵)) & ⊢ (𝜑 → 𝐷 = (◡𝐹 “ 𝐵)) ⇒ ⊢ (𝜑 → (𝐹 ↾ 𝐷):𝐷–onto→𝐸) | ||
| Theorem | fvn0ssdmfun 7094* | If a class' function values for certain arguments is not the empty set, the arguments are contained in the domain of the class, and the class restricted to the arguments is a function, analogous to fvfundmfvn0 6949. (Contributed by AV, 27-Jan-2020.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
| ⊢ (∀𝑎 ∈ 𝐷 (𝐹‘𝑎) ≠ ∅ → (𝐷 ⊆ dom 𝐹 ∧ Fun (𝐹 ↾ 𝐷))) | ||
| Theorem | fnopfv 7095 | Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1] p. 41. (Contributed by NM, 30-Sep-2004.) |
| ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → 〈𝐵, (𝐹‘𝐵)〉 ∈ 𝐹) | ||
| Theorem | fvelrn 7096 | A function's value belongs to its range. (Contributed by NM, 14-Oct-1996.) |
| ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → (𝐹‘𝐴) ∈ ran 𝐹) | ||
| Theorem | nelrnfvne 7097 | A function value cannot be any element not contained in the range of the function. (Contributed by AV, 28-Jan-2020.) |
| ⊢ ((Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹 ∧ 𝑌 ∉ ran 𝐹) → (𝐹‘𝑋) ≠ 𝑌) | ||
| Theorem | fveqdmss 7098* | If the empty set is not contained in the range of a function, and the function values of another class (not necessarily a function) are equal to the function values of the function for all elements of the domain of the function, then the domain of the function is contained in the domain of the class. (Contributed by AV, 28-Jan-2020.) |
| ⊢ 𝐷 = dom 𝐵 ⇒ ⊢ ((Fun 𝐵 ∧ ∅ ∉ ran 𝐵 ∧ ∀𝑥 ∈ 𝐷 (𝐴‘𝑥) = (𝐵‘𝑥)) → 𝐷 ⊆ dom 𝐴) | ||
| Theorem | fveqressseq 7099* | If the empty set is not contained in the range of a function, and the function values of another class (not necessarily a function) are equal to the function values of the function for all elements of the domain of the function, then the class restricted to the domain of the function is the function itself. (Contributed by AV, 28-Jan-2020.) |
| ⊢ 𝐷 = dom 𝐵 ⇒ ⊢ ((Fun 𝐵 ∧ ∅ ∉ ran 𝐵 ∧ ∀𝑥 ∈ 𝐷 (𝐴‘𝑥) = (𝐵‘𝑥)) → (𝐴 ↾ 𝐷) = 𝐵) | ||
| Theorem | fnfvelrn 7100 | A function's value belongs to its range. (Contributed by NM, 15-Oct-1996.) |
| ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐹‘𝐵) ∈ ran 𝐹) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |