Home | Metamath
Proof Explorer Theorem List (p. 65 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | funsn 6401 | A singleton of an ordered pair is a function. Theorem 10.5 of [Quine] p. 65. (Contributed by NM, 12-Aug-1994.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ Fun {〈𝐴, 𝐵〉} | ||
Theorem | funprg 6402 | A set of two pairs is a function if their first members are different. (Contributed by FL, 26-Jun-2011.) (Proof shortened by JJ, 14-Jul-2021.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) → Fun {〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉}) | ||
Theorem | funtpg 6403 | A set of three pairs is a function if their first members are different. (Contributed by Alexander van der Vekens, 5-Dec-2017.) (Proof shortened by JJ, 14-Jul-2021.) |
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → Fun {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉, 〈𝑍, 𝐶〉}) | ||
Theorem | funpr 6404 | A function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ (𝐴 ≠ 𝐵 → Fun {〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉}) | ||
Theorem | funtp 6405 | A function with a domain of three elements. (Contributed by NM, 14-Sep-2011.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V & ⊢ 𝐸 ∈ V & ⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → Fun {〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉}) | ||
Theorem | fnsn 6406 | Functionality and domain of the singleton of an ordered pair. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ {〈𝐴, 𝐵〉} Fn {𝐴} | ||
Theorem | fnprg 6407 | Function with a domain of two different values. (Contributed by FL, 26-Jun-2011.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) → {〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉} Fn {𝐴, 𝐵}) | ||
Theorem | fntpg 6408 | Function with a domain of three different values. (Contributed by Alexander van der Vekens, 5-Dec-2017.) |
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉, 〈𝑍, 𝐶〉} Fn {𝑋, 𝑌, 𝑍}) | ||
Theorem | fntp 6409 | A function with a domain of three elements. (Contributed by NM, 14-Sep-2011.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V & ⊢ 𝐸 ∈ V & ⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → {〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉} Fn {𝐴, 𝐵, 𝐶}) | ||
Theorem | funcnvpr 6410 | The converse pair of ordered pairs is a function if the second members are different. Note that the second members need not be sets. (Contributed by AV, 23-Jan-2021.) |
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷) → Fun ◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉}) | ||
Theorem | funcnvtp 6411 | The converse triple of ordered pairs is a function if the second members are pairwise different. Note that the second members need not be sets. (Contributed by AV, 23-Jan-2021.) |
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐷 ≠ 𝐹)) → Fun ◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉, 〈𝐸, 𝐹〉}) | ||
Theorem | funcnvqp 6412 | The converse quadruple of ordered pairs is a function if the second members are pairwise different. Note that the second members need not be sets. (Contributed by AV, 23-Jan-2021.) (Proof shortened by JJ, 14-Jul-2021.) |
⊢ ((((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) ∧ (𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇)) ∧ ((𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻) ∧ (𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐻) ∧ 𝐹 ≠ 𝐻)) → Fun ◡({〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ∪ {〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉})) | ||
Theorem | fun0 6413 | The empty set is a function. Theorem 10.3 of [Quine] p. 65. (Contributed by NM, 7-Apr-1998.) |
⊢ Fun ∅ | ||
Theorem | funcnv0 6414 | The converse of the empty set is a function. (Contributed by AV, 7-Jan-2021.) |
⊢ Fun ◡∅ | ||
Theorem | funcnvcnv 6415 | The double converse of a function is a function. (Contributed by NM, 21-Sep-2004.) |
⊢ (Fun 𝐴 → Fun ◡◡𝐴) | ||
Theorem | funcnv2 6416* | A simpler equivalence for single-rooted (see funcnv 6417). (Contributed by NM, 9-Aug-2004.) |
⊢ (Fun ◡𝐴 ↔ ∀𝑦∃*𝑥 𝑥𝐴𝑦) | ||
Theorem | funcnv 6417* | The converse of a class is a function iff the class is single-rooted, which means that for any 𝑦 in the range of 𝐴 there is at most one 𝑥 such that 𝑥𝐴𝑦. Definition of single-rooted in [Enderton] p. 43. See funcnv2 6416 for a simpler version. (Contributed by NM, 13-Aug-2004.) |
⊢ (Fun ◡𝐴 ↔ ∀𝑦 ∈ ran 𝐴∃*𝑥 𝑥𝐴𝑦) | ||
Theorem | funcnv3 6418* | A condition showing a class is single-rooted. (See funcnv 6417). (Contributed by NM, 26-May-2006.) |
⊢ (Fun ◡𝐴 ↔ ∀𝑦 ∈ ran 𝐴∃!𝑥 ∈ dom 𝐴 𝑥𝐴𝑦) | ||
Theorem | fun2cnv 6419* | The double converse of a class is a function iff the class is single-valued. Each side is equivalent to Definition 6.4(2) of [TakeutiZaring] p. 23, who use the notation "Un(A)" for single-valued. Note that 𝐴 is not necessarily a function. (Contributed by NM, 13-Aug-2004.) |
⊢ (Fun ◡◡𝐴 ↔ ∀𝑥∃*𝑦 𝑥𝐴𝑦) | ||
Theorem | svrelfun 6420 | A single-valued relation is a function. (See fun2cnv 6419 for "single-valued.") Definition 6.4(4) of [TakeutiZaring] p. 24. (Contributed by NM, 17-Jan-2006.) |
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ Fun ◡◡𝐴)) | ||
Theorem | fncnv 6421* | Single-rootedness (see funcnv 6417) of a class cut down by a Cartesian product. (Contributed by NM, 5-Mar-2007.) |
⊢ (◡(𝑅 ∩ (𝐴 × 𝐵)) Fn 𝐵 ↔ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑥𝑅𝑦) | ||
Theorem | fun11 6422* | Two ways of stating that 𝐴 is one-to-one (but not necessarily a function). Each side is equivalent to Definition 6.4(3) of [TakeutiZaring] p. 24, who use the notation "Un2 (A)" for one-to-one (but not necessarily a function). (Contributed by NM, 17-Jan-2006.) |
⊢ ((Fun ◡◡𝐴 ∧ Fun ◡𝐴) ↔ ∀𝑥∀𝑦∀𝑧∀𝑤((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → (𝑥 = 𝑧 ↔ 𝑦 = 𝑤))) | ||
Theorem | fununi 6423* | The union of a chain (with respect to inclusion) of functions is a function. (Contributed by NM, 10-Aug-2004.) |
⊢ (∀𝑓 ∈ 𝐴 (Fun 𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → Fun ∪ 𝐴) | ||
Theorem | funin 6424 | The intersection with a function is a function. Exercise 14(a) of [Enderton] p. 53. (Contributed by NM, 19-Mar-2004.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
⊢ (Fun 𝐹 → Fun (𝐹 ∩ 𝐺)) | ||
Theorem | funres11 6425 | The restriction of a one-to-one function is one-to-one. (Contributed by NM, 25-Mar-1998.) |
⊢ (Fun ◡𝐹 → Fun ◡(𝐹 ↾ 𝐴)) | ||
Theorem | funcnvres 6426 | The converse of a restricted function. (Contributed by NM, 27-Mar-1998.) |
⊢ (Fun ◡𝐹 → ◡(𝐹 ↾ 𝐴) = (◡𝐹 ↾ (𝐹 “ 𝐴))) | ||
Theorem | cnvresid 6427 | Converse of a restricted identity function. (Contributed by FL, 4-Mar-2007.) |
⊢ ◡( I ↾ 𝐴) = ( I ↾ 𝐴) | ||
Theorem | funcnvres2 6428 | The converse of a restriction of the converse of a function equals the function restricted to the image of its converse. (Contributed by NM, 4-May-2005.) |
⊢ (Fun 𝐹 → ◡(◡𝐹 ↾ 𝐴) = (𝐹 ↾ (◡𝐹 “ 𝐴))) | ||
Theorem | funimacnv 6429 | The image of the preimage of a function. (Contributed by NM, 25-May-2004.) |
⊢ (Fun 𝐹 → (𝐹 “ (◡𝐹 “ 𝐴)) = (𝐴 ∩ ran 𝐹)) | ||
Theorem | funimass1 6430 | A kind of contraposition law that infers a subclass of an image from a preimage subclass. (Contributed by NM, 25-May-2004.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ ran 𝐹) → ((◡𝐹 “ 𝐴) ⊆ 𝐵 → 𝐴 ⊆ (𝐹 “ 𝐵))) | ||
Theorem | funimass2 6431 | A kind of contraposition law that infers an image subclass from a subclass of a preimage. (Contributed by NM, 25-May-2004.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ (◡𝐹 “ 𝐵)) → (𝐹 “ 𝐴) ⊆ 𝐵) | ||
Theorem | imadif 6432 | The image of a difference is the difference of images. (Contributed by NM, 24-May-1998.) |
⊢ (Fun ◡𝐹 → (𝐹 “ (𝐴 ∖ 𝐵)) = ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵))) | ||
Theorem | imain 6433 | The image of an intersection is the intersection of images. (Contributed by Paul Chapman, 11-Apr-2009.) |
⊢ (Fun ◡𝐹 → (𝐹 “ (𝐴 ∩ 𝐵)) = ((𝐹 “ 𝐴) ∩ (𝐹 “ 𝐵))) | ||
Theorem | funimaexg 6434 | Axiom of Replacement using abbreviations. Axiom 39(vi) of [Quine] p. 284. Compare Exercise 9 of [TakeutiZaring] p. 29. (Contributed by NM, 10-Sep-2006.) |
⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 “ 𝐵) ∈ V) | ||
Theorem | funimaex 6435 | The image of a set under any function is also a set. Equivalent of Axiom of Replacement ax-rep 5182. Axiom 39(vi) of [Quine] p. 284. Compare Exercise 9 of [TakeutiZaring] p. 29. (Contributed by NM, 17-Nov-2002.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (Fun 𝐴 → (𝐴 “ 𝐵) ∈ V) | ||
Theorem | isarep1 6436* | Part of a study of the Axiom of Replacement used by the Isabelle prover. The object PrimReplace is apparently the image of the function encoded by 𝜑(𝑥, 𝑦) i.e. the class ({〈𝑥, 𝑦〉 ∣ 𝜑} “ 𝐴). If so, we can prove Isabelle's "Axiom of Replacement" conclusion without using the Axiom of Replacement, for which I (N. Megill) currently have no explanation. (Contributed by NM, 26-Oct-2006.) (Proof shortened by Mario Carneiro, 4-Dec-2016.) |
⊢ (𝑏 ∈ ({〈𝑥, 𝑦〉 ∣ 𝜑} “ 𝐴) ↔ ∃𝑥 ∈ 𝐴 [𝑏 / 𝑦]𝜑) | ||
Theorem | isarep2 6437* | Part of a study of the Axiom of Replacement used by the Isabelle prover. In Isabelle, the sethood of PrimReplace is apparently postulated implicitly by its type signature "[ i, [ i, i ] => o ] => i", which automatically asserts that it is a set without using any axioms. To prove that it is a set in Metamath, we need the hypotheses of Isabelle's "Axiom of Replacement" as well as the Axiom of Replacement in the form funimaex 6435. (Contributed by NM, 26-Oct-2006.) |
⊢ 𝐴 ∈ V & ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦∀𝑧((𝜑 ∧ [𝑧 / 𝑦]𝜑) → 𝑦 = 𝑧) ⇒ ⊢ ∃𝑤 𝑤 = ({〈𝑥, 𝑦〉 ∣ 𝜑} “ 𝐴) | ||
Theorem | fneq1 6438 | Equality theorem for function predicate with domain. (Contributed by NM, 1-Aug-1994.) |
⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴)) | ||
Theorem | fneq2 6439 | Equality theorem for function predicate with domain. (Contributed by NM, 1-Aug-1994.) |
⊢ (𝐴 = 𝐵 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵)) | ||
Theorem | fneq1d 6440 | Equality deduction for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ (𝜑 → 𝐹 = 𝐺) ⇒ ⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴)) | ||
Theorem | fneq2d 6441 | Equality deduction for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵)) | ||
Theorem | fneq12d 6442 | Equality deduction for function predicate with domain. (Contributed by NM, 26-Jun-2011.) |
⊢ (𝜑 → 𝐹 = 𝐺) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐵)) | ||
Theorem | fneq12 6443 | Equality theorem for function predicate with domain. (Contributed by Thierry Arnoux, 31-Jan-2017.) |
⊢ ((𝐹 = 𝐺 ∧ 𝐴 = 𝐵) → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐵)) | ||
Theorem | fneq1i 6444 | Equality inference for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ 𝐹 = 𝐺 ⇒ ⊢ (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴) | ||
Theorem | fneq2i 6445 | Equality inference for function predicate with domain. (Contributed by NM, 4-Sep-2011.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵) | ||
Theorem | nffn 6446 | Bound-variable hypothesis builder for a function with domain. (Contributed by NM, 30-Jan-2004.) |
⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝐹 Fn 𝐴 | ||
Theorem | fnfun 6447 | A function with domain is a function. (Contributed by NM, 1-Aug-1994.) |
⊢ (𝐹 Fn 𝐴 → Fun 𝐹) | ||
Theorem | fnrel 6448 | A function with domain is a relation. (Contributed by NM, 1-Aug-1994.) |
⊢ (𝐹 Fn 𝐴 → Rel 𝐹) | ||
Theorem | fndm 6449 | The domain of a function. (Contributed by NM, 2-Aug-1994.) |
⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) | ||
Theorem | fndmd 6450 | The domain of a function. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) ⇒ ⊢ (𝜑 → dom 𝐹 = 𝐴) | ||
Theorem | funfni 6451 | Inference to convert a function and domain antecedent. (Contributed by NM, 22-Apr-2004.) |
⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → 𝜑) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝜑) | ||
Theorem | fndmu 6452 | A function has a unique domain. (Contributed by NM, 11-Aug-1994.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐹 Fn 𝐵) → 𝐴 = 𝐵) | ||
Theorem | fnbr 6453 | The first argument of binary relation on a function belongs to the function's domain. (Contributed by NM, 7-May-2004.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵𝐹𝐶) → 𝐵 ∈ 𝐴) | ||
Theorem | fnop 6454 | The first argument of an ordered pair in a function belongs to the function's domain. (Contributed by NM, 8-Aug-1994.) |
⊢ ((𝐹 Fn 𝐴 ∧ 〈𝐵, 𝐶〉 ∈ 𝐹) → 𝐵 ∈ 𝐴) | ||
Theorem | fneu 6455* | There is exactly one value of a function. (Contributed by NM, 22-Apr-2004.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ∃!𝑦 𝐵𝐹𝑦) | ||
Theorem | fneu2 6456* | There is exactly one value of a function. (Contributed by NM, 7-Nov-1995.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ∃!𝑦〈𝐵, 𝑦〉 ∈ 𝐹) | ||
Theorem | fnun 6457 | The union of two functions with disjoint domains. (Contributed by NM, 22-Sep-2004.) |
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐹 ∪ 𝐺) Fn (𝐴 ∪ 𝐵)) | ||
Theorem | fnunsn 6458 | Extension of a function with a new ordered pair. (Contributed by NM, 28-Sep-2013.) (Revised by Mario Carneiro, 30-Apr-2015.) |
⊢ (𝜑 → 𝑋 ∈ V) & ⊢ (𝜑 → 𝑌 ∈ V) & ⊢ (𝜑 → 𝐹 Fn 𝐷) & ⊢ 𝐺 = (𝐹 ∪ {〈𝑋, 𝑌〉}) & ⊢ 𝐸 = (𝐷 ∪ {𝑋}) & ⊢ (𝜑 → ¬ 𝑋 ∈ 𝐷) ⇒ ⊢ (𝜑 → 𝐺 Fn 𝐸) | ||
Theorem | fnco 6459 | Composition of two functions. (Contributed by NM, 22-May-2006.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴) → (𝐹 ∘ 𝐺) Fn 𝐵) | ||
Theorem | fnresdm 6460 | A function does not change when restricted to its domain. (Contributed by NM, 5-Sep-2004.) |
⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹) | ||
Theorem | fnresdisj 6461 | A function restricted to a class disjoint with its domain is empty. (Contributed by NM, 23-Sep-2004.) |
⊢ (𝐹 Fn 𝐴 → ((𝐴 ∩ 𝐵) = ∅ ↔ (𝐹 ↾ 𝐵) = ∅)) | ||
Theorem | 2elresin 6462 | Membership in two functions restricted by each other's domain. (Contributed by NM, 8-Aug-1994.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐺) ↔ (〈𝑥, 𝑦〉 ∈ (𝐹 ↾ (𝐴 ∩ 𝐵)) ∧ 〈𝑥, 𝑧〉 ∈ (𝐺 ↾ (𝐴 ∩ 𝐵))))) | ||
Theorem | fnssresb 6463 | Restriction of a function with a subclass of its domain. (Contributed by NM, 10-Oct-2007.) |
⊢ (𝐹 Fn 𝐴 → ((𝐹 ↾ 𝐵) Fn 𝐵 ↔ 𝐵 ⊆ 𝐴)) | ||
Theorem | fnssres 6464 | Restriction of a function with a subclass of its domain. (Contributed by NM, 2-Aug-1994.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ↾ 𝐵) Fn 𝐵) | ||
Theorem | fnssresd 6465 | Restriction of a function to a subclass of its domain. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → (𝐹 ↾ 𝐵) Fn 𝐵) | ||
Theorem | fnresin1 6466 | Restriction of a function's domain with an intersection. (Contributed by NM, 9-Aug-1994.) |
⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ (𝐴 ∩ 𝐵)) Fn (𝐴 ∩ 𝐵)) | ||
Theorem | fnresin2 6467 | Restriction of a function's domain with an intersection. (Contributed by NM, 9-Aug-1994.) |
⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ (𝐵 ∩ 𝐴)) Fn (𝐵 ∩ 𝐴)) | ||
Theorem | fnres 6468* | An equivalence for functionality of a restriction. Compare dffun8 6377. (Contributed by Mario Carneiro, 20-May-2015.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
⊢ ((𝐹 ↾ 𝐴) Fn 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦) | ||
Theorem | idfn 6469 | The identity relation is a function on the universal class. See also funi 6381. (Contributed by BJ, 23-Dec-2023.) |
⊢ I Fn V | ||
Theorem | fnresi 6470 | The restricted identity relation is a function on the restricting class. (Contributed by NM, 27-Aug-2004.) (Proof shortened by BJ, 27-Dec-2023.) |
⊢ ( I ↾ 𝐴) Fn 𝐴 | ||
Theorem | fnresiOLD 6471 | Obsolete proof of fnresi 6470 as of 27-Dec-2023. (Contributed by NM, 27-Aug-2004.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( I ↾ 𝐴) Fn 𝐴 | ||
Theorem | fnima 6472 | The image of a function's domain is its range. (Contributed by NM, 4-Nov-2004.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
⊢ (𝐹 Fn 𝐴 → (𝐹 “ 𝐴) = ran 𝐹) | ||
Theorem | fn0 6473 | A function with empty domain is empty. (Contributed by NM, 15-Apr-1998.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
⊢ (𝐹 Fn ∅ ↔ 𝐹 = ∅) | ||
Theorem | fnimadisj 6474 | A class that is disjoint with the domain of a function has an empty image under the function. (Contributed by FL, 24-Jan-2007.) |
⊢ ((𝐹 Fn 𝐴 ∧ (𝐴 ∩ 𝐶) = ∅) → (𝐹 “ 𝐶) = ∅) | ||
Theorem | fnimaeq0 6475 | Images under a function never map nonempty sets to empty sets. EDITORIAL: usable in fnwe2lem2 39531. (Contributed by Stefan O'Rear, 21-Jan-2015.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → ((𝐹 “ 𝐵) = ∅ ↔ 𝐵 = ∅)) | ||
Theorem | dfmpt3 6476 | Alternate definition for the maps-to notation df-mpt 5139. (Contributed by Mario Carneiro, 30-Dec-2016.) |
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = ∪ 𝑥 ∈ 𝐴 ({𝑥} × {𝐵}) | ||
Theorem | mptfnf 6477 | The maps-to notation defines a function with domain. (Contributed by Scott Fenton, 21-Mar-2011.) (Revised by Thierry Arnoux, 10-May-2017.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ V ↔ (𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴) | ||
Theorem | fnmptf 6478 | The maps-to notation defines a function with domain. (Contributed by NM, 9-Apr-2013.) (Revised by Thierry Arnoux, 10-May-2017.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴) | ||
Theorem | fnopabg 6479* | Functionality and domain of an ordered-pair class abstraction. (Contributed by NM, 30-Jan-2004.) (Proof shortened by Mario Carneiro, 4-Dec-2016.) |
⊢ 𝐹 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∃!𝑦𝜑 ↔ 𝐹 Fn 𝐴) | ||
Theorem | fnopab 6480* | Functionality and domain of an ordered-pair class abstraction. (Contributed by NM, 5-Mar-1996.) |
⊢ (𝑥 ∈ 𝐴 → ∃!𝑦𝜑) & ⊢ 𝐹 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⇒ ⊢ 𝐹 Fn 𝐴 | ||
Theorem | mptfng 6481* | The maps-to notation defines a function with domain. (Contributed by Scott Fenton, 21-Mar-2011.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ V ↔ 𝐹 Fn 𝐴) | ||
Theorem | fnmpt 6482* | The maps-to notation defines a function with domain. (Contributed by NM, 9-Apr-2013.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐹 Fn 𝐴) | ||
Theorem | fnmptd 6483* | The maps-to notation defines a function with domain. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝜑 → 𝐹 Fn 𝐴) | ||
Theorem | mpt0 6484 | A mapping operation with empty domain. (Contributed by Mario Carneiro, 28-Dec-2014.) |
⊢ (𝑥 ∈ ∅ ↦ 𝐴) = ∅ | ||
Theorem | fnmpti 6485* | Functionality and domain of an ordered-pair class abstraction. (Contributed by NM, 29-Jan-2004.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ 𝐵 ∈ V & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ 𝐹 Fn 𝐴 | ||
Theorem | dmmpti 6486* | Domain of the mapping operation. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ 𝐵 ∈ V & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ dom 𝐹 = 𝐴 | ||
Theorem | dmmptd 6487* | The domain of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐴 = (𝑥 ∈ 𝐵 ↦ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → dom 𝐴 = 𝐵) | ||
Theorem | mptun 6488 | Union of mappings which are mutually compatible. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↦ 𝐶) = ((𝑥 ∈ 𝐴 ↦ 𝐶) ∪ (𝑥 ∈ 𝐵 ↦ 𝐶)) | ||
Theorem | feq1 6489 | Equality theorem for functions. (Contributed by NM, 1-Aug-1994.) |
⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵)) | ||
Theorem | feq2 6490 | Equality theorem for functions. (Contributed by NM, 1-Aug-1994.) |
⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶)) | ||
Theorem | feq3 6491 | Equality theorem for functions. (Contributed by NM, 1-Aug-1994.) |
⊢ (𝐴 = 𝐵 → (𝐹:𝐶⟶𝐴 ↔ 𝐹:𝐶⟶𝐵)) | ||
Theorem | feq23 6492 | Equality theorem for functions. (Contributed by FL, 14-Jul-2007.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → (𝐹:𝐴⟶𝐵 ↔ 𝐹:𝐶⟶𝐷)) | ||
Theorem | feq1d 6493 | Equality deduction for functions. (Contributed by NM, 19-Feb-2008.) |
⊢ (𝜑 → 𝐹 = 𝐺) ⇒ ⊢ (𝜑 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵)) | ||
Theorem | feq2d 6494 | Equality deduction for functions. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶)) | ||
Theorem | feq3d 6495 | Equality deduction for functions. (Contributed by AV, 1-Jan-2020.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐹:𝑋⟶𝐴 ↔ 𝐹:𝑋⟶𝐵)) | ||
Theorem | feq12d 6496 | Equality deduction for functions. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ (𝜑 → 𝐹 = 𝐺) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐺:𝐵⟶𝐶)) | ||
Theorem | feq123d 6497 | Equality deduction for functions. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ (𝜑 → 𝐹 = 𝐺) & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐺:𝐵⟶𝐷)) | ||
Theorem | feq123 6498 | Equality theorem for functions. (Contributed by FL, 16-Nov-2008.) |
⊢ ((𝐹 = 𝐺 ∧ 𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐶⟶𝐷)) | ||
Theorem | feq1i 6499 | Equality inference for functions. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ 𝐹 = 𝐺 ⇒ ⊢ (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵) | ||
Theorem | feq2i 6500 | Equality inference for functions. (Contributed by NM, 5-Sep-2011.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |