![]() |
Metamath
Proof Explorer Theorem List (p. 71 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fvun1d 7001 | 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 7002 | 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 7003 | Alternate definition of function value df-fv 6570 that doesn't require dummy variables. (Contributed by NM, 4-Aug-2010.) |
⊢ (𝐹‘𝐴) = ∪ ((𝐹 “ {𝐴}) ∖ ∪ ∪ (((𝐹 ↾ {𝐴}) ∘ ◡(𝐹 ↾ {𝐴})) ∖ I )) | ||
Theorem | dmfco 7004 | Domains of a function composition. (Contributed by NM, 27-Jan-1997.) |
⊢ ((Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺) → (𝐴 ∈ dom (𝐹 ∘ 𝐺) ↔ (𝐺‘𝐴) ∈ dom 𝐹)) | ||
Theorem | fvco2 7005 | 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 7006 | 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 7007 | Value of a function composition. (Contributed by NM, 3-Jan-2004.) (Revised by Mario Carneiro, 26-Dec-2014.) |
⊢ ((𝐺:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → ((𝐹 ∘ 𝐺)‘𝐶) = (𝐹‘(𝐺‘𝐶))) | ||
Theorem | fvco3d 7008 | Value of a function composition. Deduction form of fvco3 7007. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → 𝐺:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) ⇒ ⊢ (𝜑 → ((𝐹 ∘ 𝐺)‘𝐶) = (𝐹‘(𝐺‘𝐶))) | ||
Theorem | fvco4i 7009 | Conditions for a composition to be expandable without conditions on the argument. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
⊢ ∅ = (𝐹‘∅) & ⊢ Fun 𝐺 ⇒ ⊢ ((𝐹 ∘ 𝐺)‘𝑋) = (𝐹‘(𝐺‘𝑋)) | ||
Theorem | fvopab3g 7010* | 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 7011* | Value of a function given by ordered-pair class abstraction. (Contributed by NM, 23-Oct-1999.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 ∈ 𝐶 → ∃*𝑦𝜑) & ⊢ 𝐹 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐶 ∧ 𝜑)} ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝜒 → (𝐹‘𝐴) = 𝐵)) | ||
Theorem | brfvopabrbr 7012* | 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 7486. (Contributed by AV, 29-Oct-2021.) |
⊢ (𝐴‘𝑍) = {〈𝑥, 𝑦〉 ∣ (𝑥(𝐵‘𝑍)𝑦 ∧ 𝜑)} & ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → (𝜑 ↔ 𝜓)) & ⊢ Rel (𝐵‘𝑍) ⇒ ⊢ (𝑋(𝐴‘𝑍)𝑌 ↔ (𝑋(𝐵‘𝑍)𝑌 ∧ 𝜓)) | ||
Theorem | fvmptg 7013* | Value of a function given in maps-to notation. (Contributed by NM, 2-Oct-2007.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) & ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) ⇒ ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅) → (𝐹‘𝐴) = 𝐶) | ||
Theorem | fvmpti 7014* | Value of a function given in maps-to notation. (Contributed by Mario Carneiro, 23-Apr-2014.) |
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) & ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) ⇒ ⊢ (𝐴 ∈ 𝐷 → (𝐹‘𝐴) = ( I ‘𝐶)) | ||
Theorem | fvmpt 7015* | Value of a function given in maps-to notation. (Contributed by NM, 17-Aug-2011.) |
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) & ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) & ⊢ 𝐶 ∈ V ⇒ ⊢ (𝐴 ∈ 𝐷 → (𝐹‘𝐴) = 𝐶) | ||
Theorem | fvmpt2f 7016 | Value of a function given by the maps-to notation. (Contributed by Thierry Arnoux, 9-Mar-2017.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵) | ||
Theorem | fvtresfn 7017* | Functionality of a tuple-restriction function. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝑥 ↾ 𝑉)) ⇒ ⊢ (𝑋 ∈ 𝐵 → (𝐹‘𝑋) = (𝑋 ↾ 𝑉)) | ||
Theorem | fvmpts 7018* | 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 7019* | 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 7020* | 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 7021* | Deduction version of fvmptd 7022 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by AV, 29-Mar-2024.) |
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐶 ⇒ ⊢ (𝜑 → (𝐹‘𝐴) = 𝐶) | ||
Theorem | fvmptd 7022* | Deduction version of fvmpt 7015. (Contributed by Scott Fenton, 18-Feb-2013.) (Revised by Mario Carneiro, 31-Aug-2015.) (Proof shortened by AV, 29-Mar-2024.) |
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐹‘𝐴) = 𝐶) | ||
Theorem | fvmptd2 7023* | Deduction version of fvmpt 7015 (where the definition of the mapping does not depend on the common antecedent 𝜑). (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐹‘𝐴) = 𝐶) | ||
Theorem | mptrcl 7024* | 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 7025* | Value of a function given by the maps-to notation. (Contributed by Mario Carneiro, 23-Apr-2014.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝑥 ∈ 𝐴 → (𝐹‘𝑥) = ( I ‘𝐵)) | ||
Theorem | fvmpt2 7026* | Value of a function given by the maps-to notation. (Contributed by FL, 21-Jun-2010.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐹‘𝑥) = 𝐵) | ||
Theorem | fvmptss 7027* | 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 7028* | Deduction version of fvmpt2 7026. (Contributed by Thierry Arnoux, 8-Dec-2016.) |
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵) | ||
Theorem | fvmptex 7029* | 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 7030* | Alternate deduction version of fvmpt 7015 with three nonfreeness hypotheses instead of distinct variable conditions. (Contributed by AV, 19-Jan-2022.) |
⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → ((𝐹‘𝐴) = 𝐵 → 𝜓)) & ⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (𝜑 → (𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) → 𝜓)) | ||
Theorem | fvmptd2f 7031* | Alternate deduction version of fvmpt 7015, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.) (Proof shortened by AV, 19-Jan-2022.) |
⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → ((𝐹‘𝐴) = 𝐵 → 𝜓)) & ⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (𝜑 → (𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) → 𝜓)) | ||
Theorem | fvmptdv 7032* | Alternate deduction version of fvmpt 7015, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → ((𝐹‘𝐴) = 𝐵 → 𝜓)) ⇒ ⊢ (𝜑 → (𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) → 𝜓)) | ||
Theorem | fvmptdv2 7033* | Alternate deduction version of fvmpt 7015, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) → (𝐹‘𝐴) = 𝐶)) | ||
Theorem | mpteqb 7034* | Bidirectional equality theorem for a mapping abstraction. Equivalent to eqfnfv 7050. (Contributed by Mario Carneiro, 14-Nov-2014.) |
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ((𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶) ↔ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶)) | ||
Theorem | fvmptt 7035* | Closed theorem form of fvmpt 7015. (Contributed by Scott Fenton, 21-Feb-2013.) (Revised by Mario Carneiro, 11-Sep-2015.) |
⊢ ((∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) ∧ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) ∧ (𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉)) → (𝐹‘𝐴) = 𝐶) | ||
Theorem | fvmptf 7036* | Value of a function given by an ordered-pair class abstraction. This version of fvmptg 7013 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 8-Nov-2005.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) & ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) ⇒ ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉) → (𝐹‘𝐴) = 𝐶) | ||
Theorem | fvmptnf 7037* | 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 7040 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 7038* | Deduction version of fvmpt 7015. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐹‘𝐴) = 𝐶) | ||
Theorem | fvmptd4 7039* | Deduction version of fvmpt 7015 (where the substitution hypothesis does not have the antecedent 𝜑). (Contributed by SN, 26-Jul-2024.) |
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)) & ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐹‘𝐴) = 𝐶) | ||
Theorem | fvmptn 7040* | 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 7013. (Contributed by NM, 21-Oct-2003.) (Revised by Mario Carneiro, 9-Sep-2013.) |
⊢ (𝑥 = 𝐷 → 𝐵 = 𝐶) & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (¬ 𝐶 ∈ V → (𝐹‘𝐷) = ∅) | ||
Theorem | fvmptss2 7041* | 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 7042* | 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 7043 with a disjoint variable condition, which does not require ax-13 2374. (Contributed by Alexander van der Vekens, 15-Jul-2018.) Avoid ax-13 2374. (Revised by GG, 26-Jan-2024.) |
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∈ ⦋𝑥 / 𝑚⦌𝑀 ∣ 𝜑}) & ⊢ (𝑋 ∈ 𝑉 → ⦋𝑋 / 𝑚⦌𝑀 ∈ V) ⇒ ⊢ (𝑌 ∈ (𝐹‘𝑋) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ ⦋𝑋 / 𝑚⦌𝑀)) | ||
Theorem | elfvmptrab1 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. Usage of this theorem is discouraged because it depends on ax-13 2374. Use the weaker elfvmptrab1w 7042 when possible. (Contributed by Alexander van der Vekens, 15-Jul-2018.) (New usage is discouraged.) |
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∈ ⦋𝑥 / 𝑚⦌𝑀 ∣ 𝜑}) & ⊢ (𝑋 ∈ 𝑉 → ⦋𝑋 / 𝑚⦌𝑀 ∈ V) ⇒ ⊢ (𝑌 ∈ (𝐹‘𝑋) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ ⦋𝑋 / 𝑚⦌𝑀)) | ||
Theorem | elfvmptrab 7044* | 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 7045* | Value of a function given by an ordered-pair class abstraction, outside of its domain. (Contributed by NM, 28-Mar-2008.) |
⊢ 𝐹 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⇒ ⊢ (¬ 𝐵 ∈ 𝐴 → (𝐹‘𝐵) = ∅) | ||
Theorem | fvmptndm 7046* | Value of a function given by the maps-to notation, outside of its domain. (Contributed by AV, 31-Dec-2020.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (¬ 𝑋 ∈ 𝐴 → (𝐹‘𝑋) = ∅) | ||
Theorem | fvmptrabfv 7047* | 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 7048* | 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 7049* | 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 7050* | 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 7051* | 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 7052* | Derive equality of functions from equality of their values. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → (𝐹 = 𝐺 ↔ (𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝐵 ∧ (𝐹‘𝑥) = (𝐺‘𝑥))))) | ||
Theorem | eqfnfvd 7053* | Deduction for equality of functions. (Contributed by Mario Carneiro, 24-Jul-2014.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = (𝐺‘𝑥)) ⇒ ⊢ (𝜑 → 𝐹 = 𝐺) | ||
Theorem | eqfnfv2f 7054* | 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 7050 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 29-Jan-2004.) |
⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝐺 ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))) | ||
Theorem | eqfunfv 7055* | Equality of functions is determined by their values. (Contributed by Scott Fenton, 19-Jun-2011.) |
⊢ ((Fun 𝐹 ∧ Fun 𝐺) → (𝐹 = 𝐺 ↔ (dom 𝐹 = dom 𝐺 ∧ ∀𝑥 ∈ dom 𝐹(𝐹‘𝑥) = (𝐺‘𝑥)))) | ||
Theorem | eqfnun 7056 | 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 7057* | Equality of restricted functions is determined by their values (for functions with different domains). (Contributed by AV, 6-Jan-2019.) |
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐶) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ⊆ 𝐶)) → ((𝐹 ↾ 𝐵) = (𝐺 ↾ 𝐵) ↔ ∀𝑥 ∈ 𝐵 (𝐹‘𝑥) = (𝐺‘𝑥))) | ||
Theorem | fvreseq1 7058* | Equality of a function restricted to the domain of another function. (Contributed by AV, 6-Jan-2019.) |
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ 𝐵 ⊆ 𝐴) → ((𝐹 ↾ 𝐵) = 𝐺 ↔ ∀𝑥 ∈ 𝐵 (𝐹‘𝑥) = (𝐺‘𝑥))) | ||
Theorem | fvreseq 7059* | 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 7060* | A function with a given domain is a mapping defined by its function values. (Contributed by AV, 1-Mar-2019.) |
⊢ (𝜑 → 𝑀 Fn 𝐴) & ⊢ (𝑖 = 𝑎 → 𝐷 = 𝐶) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → 𝐷 ∈ 𝑈) & ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑀 = (𝑎 ∈ 𝐴 ↦ 𝐶) ↔ ∀𝑖 ∈ 𝐴 (𝑀‘𝑖) = 𝐷)) | ||
Theorem | fndmdif 7061* | Two ways to express the locus of differences between two functions. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → dom (𝐹 ∖ 𝐺) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ≠ (𝐺‘𝑥)}) | ||
Theorem | fndmdifcom 7062 | The difference set between two functions is commutative. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → dom (𝐹 ∖ 𝐺) = dom (𝐺 ∖ 𝐹)) | ||
Theorem | fndmdifeq0 7063 | 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 7064* | Two ways to express the locus of equality between two functions. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → dom (𝐹 ∩ 𝐺) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) = (𝐺‘𝑥)}) | ||
Theorem | fneqeql 7065 | Two functions are equal iff their equalizer is the whole domain. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ dom (𝐹 ∩ 𝐺) = 𝐴)) | ||
Theorem | fneqeql2 7066 | Two functions are equal iff their equalizer contains the whole domain. (Contributed by Stefan O'Rear, 9-Mar-2015.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ 𝐴 ⊆ dom (𝐹 ∩ 𝐺))) | ||
Theorem | fnreseql 7067 | 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 7068* | 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 7069 | 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 7070 | Two ways to say that 𝐴 is in the domain of 𝐹. (Contributed by Mario Carneiro, 1-May-2014.) |
⊢ (Fun 𝐹 → (𝐴 ∈ dom 𝐹 ↔ 𝐴𝐹(𝐹‘𝐴))) | ||
Theorem | fvimacnvi 7071 | A member of a preimage is a function value argument. (Contributed by NM, 4-May-2007.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ (◡𝐹 “ 𝐵)) → (𝐹‘𝐴) ∈ 𝐵) | ||
Theorem | fvimacnv 7072 | 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 6650 could probably be strengthened to a biconditional." (Contributed by Raph Levien, 20-Nov-2006.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → ((𝐹‘𝐴) ∈ 𝐵 ↔ 𝐴 ∈ (◡𝐹 “ 𝐵))) | ||
Theorem | funimass3 7073 | 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 7072 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 7074* | A subclass of a preimage in terms of function values. (Contributed by NM, 15-May-2007.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐴 ⊆ (◡𝐹 “ 𝐵) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) | ||
Theorem | funconstss 7075* | Two ways of specifying that a function is constant on a subdomain. (Contributed by NM, 8-Mar-2007.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵 ↔ 𝐴 ⊆ (◡𝐹 “ {𝐵}))) | ||
Theorem | fvimacnvALT 7076 | Alternate proof of fvimacnv 7072, based on funimass3 7073. If funimass3 7073 is ever proved directly, as opposed to using funimacnv 6648 pointwise, then the proof of funimacnv 6648 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 7077 | Membership in the preimage of a set under a function. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) ↔ (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶))) | ||
Theorem | elpreimad 7078 | Membership in the preimage of a set under a function. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ (𝜑 → (𝐹‘𝐵) ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐵 ∈ (◡𝐹 “ 𝐶)) | ||
Theorem | fniniseg 7079 | 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 7080* | Inverse images under functions expressed as abstractions. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ (𝐹 Fn 𝐴 → (◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ∈ 𝐵}) | ||
Theorem | fniniseg2 7081* | Inverse point images under functions expressed as abstractions. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ (𝐹 Fn 𝐴 → (◡𝐹 “ {𝐵}) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) = 𝐵}) | ||
Theorem | unpreima 7082 | Preimage of a union. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (Fun 𝐹 → (◡𝐹 “ (𝐴 ∪ 𝐵)) = ((◡𝐹 “ 𝐴) ∪ (◡𝐹 “ 𝐵))) | ||
Theorem | inpreima 7083 | Preimage of an intersection. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 14-Jun-2016.) |
⊢ (Fun 𝐹 → (◡𝐹 “ (𝐴 ∩ 𝐵)) = ((◡𝐹 “ 𝐴) ∩ (◡𝐹 “ 𝐵))) | ||
Theorem | difpreima 7084 | Preimage of a difference. (Contributed by Mario Carneiro, 14-Jun-2016.) |
⊢ (Fun 𝐹 → (◡𝐹 “ (𝐴 ∖ 𝐵)) = ((◡𝐹 “ 𝐴) ∖ (◡𝐹 “ 𝐵))) | ||
Theorem | respreima 7085 | The preimage of a restricted function. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (Fun 𝐹 → (◡(𝐹 ↾ 𝐵) “ 𝐴) = ((◡𝐹 “ 𝐴) ∩ 𝐵)) | ||
Theorem | cnvimainrn 7086 | 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 7087 | The preimage of a subset is a subset of the preimage. (Contributed by Brendan Leahy, 23-Sep-2017.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ 𝐵) → (◡𝐹 “ 𝐴) ⊆ (◡𝐹 “ 𝐵)) | ||
Theorem | iinpreima 7088* | Preimage of an intersection. (Contributed by FL, 16-Apr-2012.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ≠ ∅) → (◡𝐹 “ ∩ 𝑥 ∈ 𝐴 𝐵) = ∩ 𝑥 ∈ 𝐴 (◡𝐹 “ 𝐵)) | ||
Theorem | intpreima 7089* | Preimage of an intersection. (Contributed by FL, 28-Apr-2012.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ≠ ∅) → (◡𝐹 “ ∩ 𝐴) = ∩ 𝑥 ∈ 𝐴 (◡𝐹 “ 𝑥)) | ||
Theorem | fimacnvinrn 7090 | 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 7091 | 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 7092 | 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 7093* | 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 7094 | Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1] p. 41. (Contributed by NM, 30-Sep-2004.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → 〈𝐵, (𝐹‘𝐵)〉 ∈ 𝐹) | ||
Theorem | fvelrn 7095 | A function's value belongs to its range. (Contributed by NM, 14-Oct-1996.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → (𝐹‘𝐴) ∈ ran 𝐹) | ||
Theorem | nelrnfvne 7096 | 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 7097* | 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 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 class restricted to the domain of the function is the function itself. (Contributed by AV, 28-Jan-2020.) |
⊢ 𝐷 = dom 𝐵 ⇒ ⊢ ((Fun 𝐵 ∧ ∅ ∉ ran 𝐵 ∧ ∀𝑥 ∈ 𝐷 (𝐴‘𝑥) = (𝐵‘𝑥)) → (𝐴 ↾ 𝐷) = 𝐵) | ||
Theorem | fnfvelrn 7099 | A function's value belongs to its range. (Contributed by NM, 15-Oct-1996.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐹‘𝐵) ∈ ran 𝐹) | ||
Theorem | ffvelcdm 7100 | A function's value belongs to its codomain. (Contributed by NM, 12-Aug-1999.) |
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |