![]() |
Metamath
Proof Explorer Theorem List (p. 437 of 454) | < 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-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | adh-minim-ax2-lem6 43601 | Sixth lemma for the derivation of ax-2 7 from adh-minim 43594 and ax-mp 5. Polish prefix notation: CCpCCCCqrsCCrCstCrtuCpu . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → ((((𝜓 → 𝜒) → 𝜃) → ((𝜒 → (𝜃 → 𝜏)) → (𝜒 → 𝜏))) → 𝜂)) → (𝜑 → 𝜂)) | ||
Theorem | adh-minim-ax2c 43602 | Derivation of a commuted form of ax-2 7 from adh-minim 43594 and ax-mp 5. Polish prefix notation: CCpqCCpCqrCpr . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → 𝜓) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒))) | ||
Theorem | adh-minim-ax2 43603 | Derivation of ax-2 7 from adh-minim 43594 and ax-mp 5. Carew Arthur Meredith derived ax-2 7 in A single axiom of positive logic, The Journal of Computing Systems, volume 1, issue 3, July 1953, pages 169--170. However, here we follow the shortened derivation by Ivo Thomas, On Meredith's sole positive axiom, Notre Dame Journal of Formal Logic, volume XV, number 3, July 1974, page 477. Polish prefix notation: CCpCqrCCpqCpr . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒))) | ||
Theorem | adh-minim-idALT 43604 | Derivation of id 22 (reflexivity of implication, PM *2.08 WhiteheadRussell p. 101) from adh-minim-ax1 43599, adh-minim-ax2 43603, and ax-mp 5. It uses the derivation written DD211 in D-notation. (See head comment for an explanation.) Polish prefix notation: Cpp . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜑) | ||
Theorem | adh-minim-pm2.43 43605 | Derivation of pm2.43 56 WhiteheadRussell p. 106 (also called "hilbert" or "W") from adh-minim-ax1 43599, adh-minim-ax2 43603, and ax-mp 5. It uses the derivation written DD22D21 in D-notation. (See head comment for an explanation.) (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → (𝜑 → 𝜓)) → (𝜑 → 𝜓)) | ||
Theorem | adh-minimp 43606 | Another single axiom for minimal implicational calculus, due to Meredith. Other single axioms of the same length are known, but it is thought to be the minimal length. Among single axioms of this length, it is the one with simplest antecedents (i.e., in the corresponding ordering of binary trees which first compares left subtrees, it is the first one). Known as "HI-2" on Dolph Edward "Ted" Ulrich's web page. In the next 4 lemmas and 5 theorems, ax-1 6 and ax-2 7 are derived from this other single axiom in 20 detachments (instances of ax-mp 5) in total. Polish prefix notation: CpCCqrCCCsqCrtCqt ; or CtCCpqCCCspCqrCpr in Carew Arthur Meredith and Arthur Norman Prior, Notes on the axiomatics of the propositional calculus, Notre Dame Journal of Formal Logic, volume IV, number 3, July 1963, pages 171--187, on page 180. (Contributed by BJ, 4-Apr-2021.) (Revised by ADH, 10-Nov-2023.) |
⊢ (𝜑 → ((𝜓 → 𝜒) → (((𝜃 → 𝜓) → (𝜒 → 𝜏)) → (𝜓 → 𝜏)))) | ||
Theorem | adh-minimp-jarr-imim1-ax2c-lem1 43607 | First lemma for the derivation of jarr 106, imim1 83, and a commuted form of ax-2 7, and indirectly ax-1 6 and ax-2 7, from adh-minimp 43606 and ax-mp 5. Polish prefix notation: CCpqCCCrpCqsCps . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → 𝜓) → (((𝜒 → 𝜑) → (𝜓 → 𝜃)) → (𝜑 → 𝜃))) | ||
Theorem | adh-minimp-jarr-lem2 43608 | Second lemma for the derivation of jarr 106, and indirectly ax-1 6, a commuted form of ax-2 7, and ax-2 7 proper, from adh-minimp 43606 and ax-mp 5. Polish prefix notation: CCCpqCCCrsCCCtrCsuCruvCqv . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝜑 → 𝜓) → (((𝜒 → 𝜃) → (((𝜏 → 𝜒) → (𝜃 → 𝜂)) → (𝜒 → 𝜂))) → 𝜁)) → (𝜓 → 𝜁)) | ||
Theorem | adh-minimp-jarr-ax2c-lem3 43609 | Third lemma for the derivation of jarr 106 and a commuted form of ax-2 7, and indirectly ax-1 6 and ax-2 7 proper , from adh-minimp 43606 and ax-mp 5. Polish prefix notation: CCCCpqCCCrpCqsCpstt . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((((𝜑 → 𝜓) → (((𝜒 → 𝜑) → (𝜓 → 𝜃)) → (𝜑 → 𝜃))) → 𝜏) → 𝜏) | ||
Theorem | adh-minimp-sylsimp 43610 | Derivation of jarr 106 (also called "syll-simp") from minimp 1623 and ax-mp 5. Polish prefix notation: CCCpqrCqr . (Contributed by BJ, 4-Apr-2021.) (Revised by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝜑 → 𝜓) → 𝜒) → (𝜓 → 𝜒)) | ||
Theorem | adh-minimp-ax1 43611 | Derivation of ax-1 6 from adh-minimp 43606 and ax-mp 5. Polish prefix notation: CpCqp . (Contributed by BJ, 4-Apr-2021.) (Revised by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜑)) | ||
Theorem | adh-minimp-imim1 43612 | Derivation of imim1 83 ("left antimonotonicity of implication", theorem *2.06 of [WhiteheadRussell] p. 100) from adh-minimp 43606 and ax-mp 5. Polish prefix notation: CCpqCCqrCpr . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒))) | ||
Theorem | adh-minimp-ax2c 43613 | Derivation of a commuted form of ax-2 7 from adh-minimp 43606 and ax-mp 5. Polish prefix notation: CCpqCCpCqrCpr . (Contributed by BJ, 4-Apr-2021.) (Revised by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → 𝜓) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒))) | ||
Theorem | adh-minimp-ax2-lem4 43614 | Fourth lemma for the derivation of ax-2 7 from adh-minimp 43606 and ax-mp 5. Polish prefix notation: CpCCqCprCqr . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → ((𝜓 → (𝜑 → 𝜒)) → (𝜓 → 𝜒))) | ||
Theorem | adh-minimp-ax2 43615 | Derivation of ax-2 7 from adh-minimp 43606 and ax-mp 5. Polish prefix notation: CCpCqrCCpqCpr . (Contributed by BJ, 4-Apr-2021.) (Revised by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒))) | ||
Theorem | adh-minimp-idALT 43616 | Derivation of id 22 (reflexivity of implication, PM *2.08 WhiteheadRussell p. 101) from adh-minimp-ax1 43611, adh-minimp-ax2 43615, and ax-mp 5. It uses the derivation written DD211 in D-notation. (See head comment for an explanation.) Polish prefix notation: Cpp . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜑) | ||
Theorem | adh-minimp-pm2.43 43617 | Derivation of pm2.43 56 WhiteheadRussell p. 106 (also called "hilbert" or "W") from adh-minimp-ax1 43611, adh-minimp-ax2 43615, and ax-mp 5. It uses the derivation written DD22D21 in D-notation. (See head comment for an explanation.) Polish prefix notation: CCpCpqCpq . (Contributed by BJ, 31-May-2021.) (Revised by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → (𝜑 → 𝜓)) → (𝜑 → 𝜓)) | ||
Theorem | eusnsn 43618* | There is a unique element of a singleton which is equal to another singleton. (Contributed by AV, 24-Aug-2022.) |
⊢ ∃!𝑥{𝑥} = {𝑦} | ||
Theorem | absnsb 43619* | If the class abstraction {𝑥 ∣ 𝜑} associated with the wff 𝜑 is a singleton, the wff is true for the singleton element. (Contributed by AV, 24-Aug-2022.) |
⊢ ({𝑥 ∣ 𝜑} = {𝑦} → [𝑦 / 𝑥]𝜑) | ||
Theorem | euabsneu 43620* | Another way to express existential uniqueness of a wff 𝜑: its associated class abstraction {𝑥 ∣ 𝜑} is a singleton. Variant of euabsn2 4621 using existential uniqueness for the singleton element instead of existence only. (Contributed by AV, 24-Aug-2022.) |
⊢ (∃!𝑥𝜑 ↔ ∃!𝑦{𝑥 ∣ 𝜑} = {𝑦}) | ||
Theorem | elprneb 43621 | An element of a proper unordered pair is the first element iff it is not the second element. (Contributed by AV, 18-Jun-2020.) |
⊢ ((𝐴 ∈ {𝐵, 𝐶} ∧ 𝐵 ≠ 𝐶) → (𝐴 = 𝐵 ↔ 𝐴 ≠ 𝐶)) | ||
Theorem | oppr 43622 | Equality for ordered pairs implies equality of unordered pairs with the same elements. (Contributed by AV, 9-Jul-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → {𝐴, 𝐵} = {𝐶, 𝐷})) | ||
Theorem | opprb 43623 | Equality for unordered pairs corresponds to equality of unordered pairs with the same elements. (Contributed by AV, 9-Jul-2023.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 ∨ 〈𝐴, 𝐵〉 = 〈𝐷, 𝐶〉))) | ||
Theorem | or2expropbilem1 43624* | Lemma 1 for or2expropbi 43626 and ich2exprop 43988. (Contributed by AV, 16-Jul-2023.) |
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 = 𝑎 ∧ 𝐵 = 𝑏) → (𝜑 → ∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ [𝑦 / 𝑏][𝑥 / 𝑎]𝜑)))) | ||
Theorem | or2expropbilem2 43625* | Lemma 2 for or2expropbi 43626 and ich2exprop 43988. (Contributed by AV, 16-Jul-2023.) |
⊢ (∃𝑎∃𝑏(〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) ↔ ∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ [𝑦 / 𝑏][𝑥 / 𝑎]𝜑)) | ||
Theorem | or2expropbi 43626* | If two classes are strictly ordered, there is an ordered pair of both classes fulfilling a wff iff there is an unordered pair of both classes fulfilling the wff. (Contributed by AV, 26-Aug-2023.) |
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵)) → (∃𝑎∃𝑏({𝐴, 𝐵} = {𝑎, 𝑏} ∧ (𝑎𝑅𝑏 ∧ 𝜑)) ↔ ∃𝑎∃𝑏(〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ∧ (𝑎𝑅𝑏 ∧ 𝜑)))) | ||
Theorem | eubrv 43627* | If there is a unique set which is related to a class, then the class must be a set. (Contributed by AV, 25-Aug-2022.) |
⊢ (∃!𝑏 𝐴𝑅𝑏 → 𝐴 ∈ V) | ||
Theorem | eubrdm 43628* | If there is a unique set which is related to a class, then the class is an element of the domain of the relation. (Contributed by AV, 25-Aug-2022.) |
⊢ (∃!𝑏 𝐴𝑅𝑏 → 𝐴 ∈ dom 𝑅) | ||
Theorem | eldmressn 43629 | Element of the domain of a restriction to a singleton. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
⊢ (𝐵 ∈ dom (𝐹 ↾ {𝐴}) → 𝐵 = 𝐴) | ||
Theorem | iota0def 43630* | Example for a defined iota being the empty set, i.e., ∀𝑦𝑥 ⊆ 𝑦 is a wff satisfied by a unique value 𝑥, namely 𝑥 = ∅ (the empty set is the one and only set which is a subset of every set). (Contributed by AV, 24-Aug-2022.) |
⊢ (℩𝑥∀𝑦 𝑥 ⊆ 𝑦) = ∅ | ||
Theorem | iota0ndef 43631* | Example for an undefined iota being the empty set, i.e., ∀𝑦𝑦 ∈ 𝑥 is a wff not satisfied by a (unique) value 𝑥 (there is no set, and therefore certainly no unique set, which contains every set). (Contributed by AV, 24-Aug-2022.) |
⊢ (℩𝑥∀𝑦 𝑦 ∈ 𝑥) = ∅ | ||
Theorem | fveqvfvv 43632 | If a function's value at an argument is the universal class (which can never be the case because of fvex 6658), the function's value at this argument is any set (especially the empty set). In short "If a function's value is a proper class, it is a set", which sounds strange/contradictory, but which is a consequence of that a contradiction implies anything (see pm2.21i 119). (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ ((𝐹‘𝐴) = V → (𝐹‘𝐴) = 𝐵) | ||
Theorem | fnresfnco 43633 | Composition of two functions, similar to fnco 6437. (Contributed by Alexander van der Vekens, 25-Jul-2017.) |
⊢ (((𝐹 ↾ ran 𝐺) Fn ran 𝐺 ∧ 𝐺 Fn 𝐵) → (𝐹 ∘ 𝐺) Fn 𝐵) | ||
Theorem | funcoressn 43634 | A composition restricted to a singleton is a function under certain conditions. (Contributed by Alexander van der Vekens, 25-Jul-2017.) |
⊢ ((((𝐺‘𝑋) ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {(𝐺‘𝑋)})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) | ||
Theorem | funressnfv 43635 | A restriction to a singleton with a function value is a function under certain conditions. (Contributed by Alexander van der Vekens, 25-Jul-2017.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → Fun (𝐹 ↾ {(𝐺‘𝑋)})) | ||
Theorem | funressndmfvrn 43636 | The value of a function 𝐹 at a set 𝐴 is in the range of the function 𝐹 if 𝐴 is in the domain of the function 𝐹. It is sufficient that 𝐹 is a function at 𝐴. (Contributed by AV, 1-Sep-2022.) |
⊢ ((Fun (𝐹 ↾ {𝐴}) ∧ 𝐴 ∈ dom 𝐹) → (𝐹‘𝐴) ∈ ran 𝐹) | ||
Theorem | funressnvmo 43637* | A function restricted to a singleton has at most one value for the singleton element as argument. (Contributed by AV, 2-Sep-2022.) |
⊢ (Fun (𝐹 ↾ {𝑥}) → ∃*𝑦 𝑥𝐹𝑦) | ||
Theorem | funressnmo 43638* | A function restricted to a singleton has at most one value for the singleton element as argument. (Contributed by AV, 2-Sep-2022.) |
⊢ ((𝐴 ∈ 𝑉 ∧ Fun (𝐹 ↾ {𝐴})) → ∃*𝑦 𝐴𝐹𝑦) | ||
Theorem | funressneu 43639* | There is exactly one value of a class which is a function restricted to a singleton, analogous to funeu 6349. 𝐴 ∈ V is required because otherwise ∃!𝑦𝐴𝐹𝑦, see brprcneu 6637. (Contributed by AV, 7-Sep-2022.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ Fun (𝐹 ↾ {𝐴}) ∧ 𝐴𝐹𝐵) → ∃!𝑦 𝐴𝐹𝑦) | ||
Syntax | caiota 43640 | Extend class notation with an alternative for Russell's definition of a description binder (inverted iota). |
class (℩'𝑥𝜑) | ||
Theorem | aiotajust 43641* | Soundness justification theorem for df-aiota 43642. (Contributed by AV, 24-Aug-2022.) |
⊢ ∩ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = ∩ {𝑧 ∣ {𝑥 ∣ 𝜑} = {𝑧}} | ||
Definition | df-aiota 43642* |
Alternate version of Russell's definition of a description binder, which
can be read as "the unique 𝑥 such that 𝜑", where 𝜑
ordinarily contains 𝑥 as a free variable. Our definition
is
meaningful only when there is exactly one 𝑥 such that 𝜑 is true
(see aiotaval 43650); otherwise, it is not a set (see aiotaexb 43646), or even
more concrete, it is the universe V (see aiotavb 43647). Since this
is an alternative for df-iota 6283, we call this symbol ℩'
alternate iota in the following.
The advantage of this definition is the clear distinguishability of the defined and undefined cases: the alternate iota over a wff is defined iff it is a set (see aiotaexb 43646). With the original definition, there is no corresponding theorem (∃!𝑥𝜑 ↔ (℩𝑥𝜑) ≠ ∅), because ∅ can be a valid unique set satisfying a wff (see, for example, iota0def 43630). Only the right to left implication would hold, see (negated) iotanul 6302. For defined cases, however, both definitions df-iota 6283 and df-aiota 43642 are equivalent, see reuaiotaiota 43645. (Proposed by BJ, 13-Aug-2022.) (Contributed by AV, 24-Aug-2022.) |
⊢ (℩'𝑥𝜑) = ∩ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} | ||
Theorem | dfaiota2 43643* | Alternate definition of the alternate version of Russell's definition of a description binder. Definition 8.18 in [Quine] p. 56. (Contributed by AV, 24-Aug-2022.) |
⊢ (℩'𝑥𝜑) = ∩ {𝑦 ∣ ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)} | ||
Theorem | reuabaiotaiota 43644* | The iota and the alternate iota over a wff 𝜑 are equal iff there is a unique satisfying value of {𝑥 ∣ 𝜑} = {𝑦}. (Contributed by AV, 25-Aug-2022.) |
⊢ (∃!𝑦{𝑥 ∣ 𝜑} = {𝑦} ↔ (℩𝑥𝜑) = (℩'𝑥𝜑)) | ||
Theorem | reuaiotaiota 43645 | The iota and the alternate iota over a wff 𝜑 are equal iff there is a unique value 𝑥 satisfying 𝜑. (Contributed by AV, 25-Aug-2022.) |
⊢ (∃!𝑥𝜑 ↔ (℩𝑥𝜑) = (℩'𝑥𝜑)) | ||
Theorem | aiotaexb 43646 | The alternate iota over a wff 𝜑 is a set iff there is a unique value 𝑥 satisfying 𝜑. (Contributed by AV, 25-Aug-2022.) |
⊢ (∃!𝑥𝜑 ↔ (℩'𝑥𝜑) ∈ V) | ||
Theorem | aiotavb 43647 | The alternate iota over a wff 𝜑 is the universe iff there is no unique value 𝑥 satisfying 𝜑. (Contributed by AV, 25-Aug-2022.) |
⊢ (¬ ∃!𝑥𝜑 ↔ (℩'𝑥𝜑) = V) | ||
Theorem | iotan0aiotaex 43648 | If the iota over a wff 𝜑 is not empty, the alternate iota over 𝜑 is a set. (Contributed by AV, 25-Aug-2022.) |
⊢ ((℩𝑥𝜑) ≠ ∅ → (℩'𝑥𝜑) ∈ V) | ||
Theorem | aiotaexaiotaiota 43649 | The alternate iota over a wff 𝜑 is a set iff the iota and the alternate iota over 𝜑 are equal. (Contributed by AV, 25-Aug-2022.) |
⊢ ((℩'𝑥𝜑) ∈ V ↔ (℩𝑥𝜑) = (℩'𝑥𝜑)) | ||
Theorem | aiotaval 43650* | Theorem 8.19 in [Quine] p. 57. This theorem is the fundamental property of (alternate) iota. (Contributed by AV, 24-Aug-2022.) |
⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → (℩'𝑥𝜑) = 𝑦) | ||
Theorem | aiota0def 43651* | Example for a defined alternate iota being the empty set, i.e., ∀𝑦𝑥 ⊆ 𝑦 is a wff satisfied by a unique value 𝑥, namely 𝑥 = ∅ (the empty set is the one and only set which is a subset of every set). This corresponds to iota0def 43630. (Contributed by AV, 25-Aug-2022.) |
⊢ (℩'𝑥∀𝑦 𝑥 ⊆ 𝑦) = ∅ | ||
Theorem | aiota0ndef 43652* | Example for an undefined alternate iota being no set, i.e., ∀𝑦𝑦 ∈ 𝑥 is a wff not satisfied by a (unique) value 𝑥 (there is no set, and therefore certainly no unique set, which contains every set). This is different from iota0ndef 43631, where the iota still is a set (the empty set). (Contributed by AV, 25-Aug-2022.) |
⊢ (℩'𝑥∀𝑦 𝑦 ∈ 𝑥) ∉ V | ||
Theorem | r19.32 43653 | Theorem 19.32 of [Margaris] p. 90 with restricted quantifiers, analogous to r19.32v 3294. (Contributed by Alexander van der Vekens, 29-Jun-2017.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∀𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | rexsb 43654* | An equivalent expression for restricted existence, analogous to exsb 2367. (Contributed by Alexander van der Vekens, 1-Jul-2017.) |
⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | rexrsb 43655* | An equivalent expression for restricted existence, analogous to exsb 2367. (Contributed by Alexander van der Vekens, 1-Jul-2017.) |
⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 = 𝑦 → 𝜑)) | ||
Theorem | 2rexsb 43656* | An equivalent expression for double restricted existence, analogous to rexsb 43654. (Contributed by Alexander van der Vekens, 1-Jul-2017.) |
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 ∀𝑥∀𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜑)) | ||
Theorem | 2rexrsb 43657* | An equivalent expression for double restricted existence, analogous to 2exsb 2368. (Contributed by Alexander van der Vekens, 1-Jul-2017.) |
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜑)) | ||
Theorem | cbvral2 43658* | Change bound variables of double restricted universal quantification, using implicit substitution, analogous to cbvral2v 3411. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑥𝜒 & ⊢ Ⅎ𝑤𝜒 & ⊢ Ⅎ𝑦𝜓 & ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 𝜓) | ||
Theorem | cbvrex2 43659* | Change bound variables of double restricted universal quantification, using implicit substitution, analogous to cbvrex2v 3412. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑥𝜒 & ⊢ Ⅎ𝑤𝜒 & ⊢ Ⅎ𝑦𝜓 & ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝜓) | ||
Theorem | 2ralbiim 43660 | Split a biconditional and distribute 2 quantifiers, analogous to 2albiim 1891 and ralbiim 3141. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ↔ 𝜓) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝜓) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜓 → 𝜑))) | ||
Theorem | ralndv1 43661 | Example for a theorem about a restricted universal quantification in which the restricting class depends on (actually is) the bound variable: All sets containing themselves contain the universal class. (Contributed by AV, 24-Jun-2023.) |
⊢ ∀𝑥 ∈ 𝑥 V ∈ 𝑥 | ||
Theorem | ralndv2 43662 | Second example for a theorem about a restricted universal quantification in which the restricting class depends on the bound variable: all subsets of a set are sets. (Contributed by AV, 24-Jun-2023.) |
⊢ ∀𝑥 ∈ 𝒫 𝑥𝑥 ∈ V | ||
Theorem | reuf1odnf 43663* | There is exactly one element in each of two isomorphic sets. Variant of reuf1od 43664 with no distinct variable condition for 𝜒. (Contributed by AV, 19-Mar-2023.) |
⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐵) & ⊢ ((𝜑 ∧ 𝑥 = (𝐹‘𝑦)) → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝑧 → (𝜓 ↔ 𝜃)) & ⊢ Ⅎ𝑥𝜒 ⇒ ⊢ (𝜑 → (∃!𝑥 ∈ 𝐵 𝜓 ↔ ∃!𝑦 ∈ 𝐶 𝜒)) | ||
Theorem | reuf1od 43664* | There is exactly one element in each of two isomorphic sets. (Contributed by AV, 19-Mar-2023.) |
⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐵) & ⊢ ((𝜑 ∧ 𝑥 = (𝐹‘𝑦)) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃!𝑥 ∈ 𝐵 𝜓 ↔ ∃!𝑦 ∈ 𝐶 𝜒)) | ||
Theorem | euoreqb 43665* | There is a set which is equal to one of two other sets iff the other sets are equal. (Contributed by AV, 24-Jan-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (∃!𝑥 ∈ 𝑉 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | 2reu3 43666* | Double restricted existential uniqueness, analogous to 2eu3 2715. (Contributed by Alexander van der Vekens, 29-Jun-2017.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (∃*𝑥 ∈ 𝐴 𝜑 ∨ ∃*𝑦 ∈ 𝐵 𝜑) → ((∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝜑) ↔ (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑))) | ||
Theorem | 2reu7 43667* | Two equivalent expressions for double restricted existential uniqueness, analogous to 2eu7 2720. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
⊢ ((∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ ∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜑)) | ||
Theorem | 2reu8 43668* | Two equivalent expressions for double restricted existential uniqueness, analogous to 2eu8 2721. Curiously, we can put ∃! on either of the internal conjuncts but not both. We can also commute ∃!𝑥 ∈ 𝐴∃!𝑦 ∈ 𝐵 using 2reu7 43667. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
⊢ (∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜑) ↔ ∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 (∃!𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜑)) | ||
Theorem | 2reu8i 43669* | Implication of a double restricted existential uniqueness in terms of restricted existential quantification and restricted universal quantification, see also 2reu8 43668. The involved wffs depend on the setvar variables as follows: ph(x,y), ta(v,y), ch(x,w), th(v,w), et(x,b), ps(a,b), ze(a,w). (Contributed by AV, 1-Apr-2023.) |
⊢ (𝑥 = 𝑣 → (𝜑 ↔ 𝜏)) & ⊢ (𝑥 = 𝑣 → (𝜒 ↔ 𝜃)) & ⊢ (𝑦 = 𝑤 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝑏 → (𝜑 ↔ 𝜂)) & ⊢ (𝑥 = 𝑎 → (𝜒 ↔ 𝜁)) & ⊢ (((𝜒 → 𝑦 = 𝑤) ∧ 𝜁) → 𝑦 = 𝑤) & ⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥))))) | ||
Theorem | 2reuimp0 43670* | Implication of a double restricted existential uniqueness in terms of restricted existential quantification and restricted universal quantification. The involved wffs depend on the setvar variables as follows: ph(a,b), th(a,c), ch(d,b), ta(d,c), et(a,e), ps(a,f) (Contributed by AV, 13-Mar-2023.) |
⊢ (𝑏 = 𝑐 → (𝜑 ↔ 𝜃)) & ⊢ (𝑎 = 𝑑 → (𝜑 ↔ 𝜒)) & ⊢ (𝑎 = 𝑑 → (𝜃 ↔ 𝜏)) & ⊢ (𝑏 = 𝑒 → (𝜑 ↔ 𝜂)) & ⊢ (𝑐 = 𝑓 → (𝜃 ↔ 𝜓)) ⇒ ⊢ (∃!𝑎 ∈ 𝑉 ∃!𝑏 ∈ 𝑉 𝜑 → ∃𝑎 ∈ 𝑉 ∀𝑑 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ∃𝑒 ∈ 𝑉 ∀𝑓 ∈ 𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓 → 𝑒 = 𝑓))) | ||
Theorem | 2reuimp 43671* | Implication of a double restricted existential uniqueness in terms of restricted existential quantification and restricted universal quantification if the class of the quantified elements is not empty. (Contributed by AV, 13-Mar-2023.) |
⊢ (𝑏 = 𝑐 → (𝜑 ↔ 𝜃)) & ⊢ (𝑎 = 𝑑 → (𝜑 ↔ 𝜒)) & ⊢ (𝑎 = 𝑑 → (𝜃 ↔ 𝜏)) & ⊢ (𝑏 = 𝑒 → (𝜑 ↔ 𝜂)) & ⊢ (𝑐 = 𝑓 → (𝜃 ↔ 𝜓)) ⇒ ⊢ ((𝑉 ≠ ∅ ∧ ∃!𝑎 ∈ 𝑉 ∃!𝑏 ∈ 𝑉 𝜑) → ∃𝑎 ∈ 𝑉 ∀𝑑 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ∃𝑒 ∈ 𝑉 ∀𝑓 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ((𝜒 ∧ (𝜏 → 𝑏 = 𝑐)) → (𝜓 → (𝜂 ∧ (𝑎 = 𝑑 ∧ 𝑒 = 𝑓))))) | ||
The current definition of the value (𝐹‘𝐴) of a function 𝐹 at an argument 𝐴 (see df-fv 6332) assures that this value is always a set, see fex 6966. This is because this definition can be applied to any classes 𝐹 and 𝐴, and evaluates to the empty set when it is not meaningful (as shown by ndmfv 6675 and fvprc 6638). Although it is very convenient for many theorems on functions and their proofs, there are some cases in which from (𝐹‘𝐴) = ∅ alone it cannot be decided/derived whether (𝐹‘𝐴) is meaningful (𝐹 is actually a function which is defined for 𝐴 and really has the function value ∅ at 𝐴) or not. Therefore, additional assumptions are required, such as ∅ ∉ ran 𝐹, ∅ ∈ ran 𝐹 or Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 (see, for example, ndmfvrcl 6676). To avoid such an ambiguity, an alternative definition (𝐹'''𝐴) (see df-afv 43676) would be possible which evaluates to the universal class ((𝐹'''𝐴) = V) if it is not meaningful (see afvnfundmuv 43695, ndmafv 43696, afvprc 43700 and nfunsnafv 43698), and which corresponds to the current definition ((𝐹‘𝐴) = (𝐹'''𝐴)) if it is (see afvfundmfveq 43694). That means (𝐹'''𝐴) = V → (𝐹‘𝐴) = ∅ (see afvpcfv0 43702), but (𝐹‘𝐴) = ∅ → (𝐹'''𝐴) = V is not generally valid. In the theory of partial functions, it is a common case that 𝐹 is not defined at 𝐴, which also would result in (𝐹'''𝐴) = V. In this context we say (𝐹'''𝐴) "is not defined" instead of "is not meaningful". With this definition the following intuitive equivalence holds: (𝐹'''𝐴) ∈ V <-> "(𝐹'''𝐴) is meaningful/defined". An interesting question would be if (𝐹‘𝐴) could be replaced by (𝐹'''𝐴) in most of the theorems based on function values. If we look at the (currently 19) proofs using the definition df-fv 6332 of (𝐹‘𝐴), we see that analogues for the following 8 theorems can be proven using the alternative definition: fveq1 6644-> afveq1 43690, fveq2 6645-> afveq2 43691, nffv 6655-> nfafv 43692, csbfv12 6688-> csbafv12g , fvres 6664-> afvres 43728, rlimdm 14900-> rlimdmafv 43733, tz6.12-1 6667-> tz6.12-1-afv 43730, fveu 6636-> afveu 43709. Three theorems proved by directly using df-fv 6332 are within a mathbox (fvsb 41156) or not used (isumclim3 15106, avril1 28248). However, the remaining 8 theorems proved by directly using df-fv 6332 are used more or less often: * fvex 6658: used in about 1750 proofs. * tz6.12-1 6667: root theorem of many theorems which have not a strict analogue, and which are used many times: fvprc 6638 (used in about 127 proofs), tz6.12i 6671 (used - indirectly via fvbr0 6672 and fvrn0 6673- in 18 proofs, and in fvclss 6979 used in fvclex 7642 used in fvresex 7643, which is not used!), dcomex 9858 (used in 4 proofs), ndmfv 6675 (used in 86 proofs) and nfunsn 6682 (used by dffv2 6733 which is not used). * fv2 6640: only used by elfv 6643, which is only used by fv3 6663, which is not used. * dffv3 6641: used by dffv4 6642 (the previous "df-fv"), which now is only used in deprecated (usage discouraged) theorems or within mathboxes (csbfv12gALTVD 41605), by shftval 14425 (itself used in 9 proofs), by dffv5 33498 (mathbox) and by fvco2 6735, which has the analogue afvco2 43732. * fvopab5 6777: used only by ajval 28644 (not used) and by adjval 29673 (used - indirectly - in 9 proofs). * zsum 15067: used (via isum 15068, sum0 15070 and fsumsers 15077) in more than 90 proofs. * isumshft 15186: used in pserdv2 25025 and (via logtayl 25251) 4 other proofs. * ovtpos 7890: used in 14 proofs. As a result of this analysis we can say that the current definition of a function value is crucial for Metamath and cannot be exchanged easily with an alternative definition. While fv2 6640, dffv3 6641, fvopab5 6777, zsum 15067, isumshft 15186 and ovtpos 7890 are not critical or are, hopefully, also valid for the alternative definition, fvex 6658 and tz6.12-1 6667 (and the theorems based on them) are essential for the current definition of function values. With the same arguments, an alternative definition of operation values ((𝐴𝑂𝐵)) could be meaningful to avoid ambiguities, see df-aov 43677. For additional details, see https://groups.google.com/g/metamath/c/cteNUppB6A4 43677. | ||
Syntax | wdfat 43672 | Extend the definition of a wff to include the "defined at" predicate. Read: "(the function) 𝐹 is defined at (the argument) 𝐴". In a previous version, the token "def@" was used. However, since the @ is used (informally) as a replacement for $ in commented out sections that may be deleted some day. While there is no violation of any standard to use the @ in a token, it could make the search for such commented-out sections slightly more difficult. (See remark of Norman Megill at https://groups.google.com/g/metamath/c/cteNUppB6A4). |
wff 𝐹 defAt 𝐴 | ||
Syntax | cafv 43673 | Extend the definition of a class to include the value of a function. Read: "the value of 𝐹 at 𝐴 " or "𝐹 of 𝐴". In a previous version, the symbol " ' " was used. However, since the similarity with the symbol ‘ used for the current definition of a function's value (see df-fv 6332), which, by the way, was intended to visualize that in many cases ‘ and " ' " are exchangeable, makes reading the theorems, especially those which uses both definitions as dfafv2 43688, very difficult, 3 apostrophes ''' are used now so that it's easier to distinguish from df-fv 6332 and df-ima 5532. And not three backticks ( three times ‘) since that would be annoying to escape in a comment. (See remark of Norman Megill and Gerard Lang at https://groups.google.com/g/metamath/c/cteNUppB6A4 5532). |
class (𝐹'''𝐴) | ||
Syntax | caov 43674 | Extend class notation to include the value of an operation 𝐹 (such as +) for two arguments 𝐴 and 𝐵. Note that the syntax is simply three class symbols in a row surrounded by a pair of parentheses in contrast to the current definition, see df-ov 7138. |
class ((𝐴𝐹𝐵)) | ||
Definition | df-dfat 43675 | Definition of the predicate that determines if some class 𝐹 is defined as function for an argument 𝐴 or, in other words, if the function value for some class 𝐹 for an argument 𝐴 is defined. We say that 𝐹 is defined at 𝐴 if a 𝐹 is a function restricted to the member 𝐴 of its domain. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ (𝐹 defAt 𝐴 ↔ (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴}))) | ||
Definition | df-afv 43676* | Alternative definition of the value of a function, (𝐹'''𝐴), also known as function application. In contrast to (𝐹‘𝐴) = ∅ (see df-fv 6332 and ndmfv 6675), (𝐹'''𝐴) = V if F is not defined for A! (Contributed by Alexander van der Vekens, 25-May-2017.) (Revised by BJ/AV, 25-Aug-2022.) |
⊢ (𝐹'''𝐴) = (℩'𝑥𝐴𝐹𝑥) | ||
Definition | df-aov 43677 | Define the value of an operation. In contrast to df-ov 7138, the alternative definition for a function value (see df-afv 43676) is used. By this, the value of the operation applied to two arguments is the universal class if the operation is not defined for these two arguments. There are still no restrictions of any kind on what those class expressions may be, although only certain kinds of class expressions - a binary operation 𝐹 and its arguments 𝐴 and 𝐵- will be useful for proving meaningful theorems. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ ((𝐴𝐹𝐵)) = (𝐹'''〈𝐴, 𝐵〉) | ||
Theorem | ralbinrald 43678* | Elemination of a restricted universal quantification under certain conditions. (Contributed by Alexander van der Vekens, 2-Aug-2017.) |
⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝑥 ∈ 𝐴 → 𝑥 = 𝑋) & ⊢ (𝑥 = 𝑋 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ 𝜃)) | ||
Theorem | nvelim 43679 | If a class is the universal class it doesn't belong to any class, generalization of nvel 5184. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ (𝐴 = V → ¬ 𝐴 ∈ 𝐵) | ||
Theorem | alneu 43680 | If a statement holds for all sets, there is not a unique set for which the statement holds. (Contributed by Alexander van der Vekens, 28-Nov-2017.) |
⊢ (∀𝑥𝜑 → ¬ ∃!𝑥𝜑) | ||
Theorem | eu2ndop1stv 43681* | If there is a unique second component in an ordered pair contained in a given set, the first component must be a set. (Contributed by Alexander van der Vekens, 29-Nov-2017.) |
⊢ (∃!𝑦〈𝐴, 𝑦〉 ∈ 𝑉 → 𝐴 ∈ V) | ||
Theorem | dfateq12d 43682 | Equality deduction for "defined at". (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ (𝜑 → 𝐹 = 𝐺) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐹 defAt 𝐴 ↔ 𝐺 defAt 𝐵)) | ||
Theorem | nfdfat 43683 | Bound-variable hypothesis builder for "defined at". To prove a deduction version of this theorem is not easily possible because many deduction versions for bound-variable hypothesis builder for constructs the definition of "defined at" is based on are not available (e.g., for Fun/Rel, dom, ⊆, etc.). (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝐹 defAt 𝐴 | ||
Theorem | dfdfat2 43684* | Alternate definition of the predicate "defined at" not using the Fun predicate. (Contributed by Alexander van der Vekens, 22-Jul-2017.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
⊢ (𝐹 defAt 𝐴 ↔ (𝐴 ∈ dom 𝐹 ∧ ∃!𝑦 𝐴𝐹𝑦)) | ||
Theorem | fundmdfat 43685 | A function is defined at any element of its domain. (Contributed by AV, 2-Sep-2022.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → 𝐹 defAt 𝐴) | ||
Theorem | dfatprc 43686 | A function is not defined at a proper class. (Contributed by AV, 1-Sep-2022.) |
⊢ (¬ 𝐴 ∈ V → ¬ 𝐹 defAt 𝐴) | ||
Theorem | dfatelrn 43687 | The value of a function 𝐹 at a set 𝐴 is in the range of the function 𝐹 if 𝐹 is defined at 𝐴. (Contributed by AV, 1-Sep-2022.) |
⊢ (𝐹 defAt 𝐴 → (𝐹‘𝐴) ∈ ran 𝐹) | ||
Theorem | dfafv2 43688 | Alternative definition of (𝐹'''𝐴) using (𝐹‘𝐴) directly. (Contributed by Alexander van der Vekens, 22-Jul-2017.) (Revised by AV, 25-Aug-2022.) |
⊢ (𝐹'''𝐴) = if(𝐹 defAt 𝐴, (𝐹‘𝐴), V) | ||
Theorem | afveq12d 43689 | Equality deduction for function value, analogous to fveq12d 6652. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ (𝜑 → 𝐹 = 𝐺) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐹'''𝐴) = (𝐺'''𝐵)) | ||
Theorem | afveq1 43690 | Equality theorem for function value, analogous to fveq1 6644. (Contributed by Alexander van der Vekens, 22-Jul-2017.) |
⊢ (𝐹 = 𝐺 → (𝐹'''𝐴) = (𝐺'''𝐴)) | ||
Theorem | afveq2 43691 | Equality theorem for function value, analogous to fveq1 6644. (Contributed by Alexander van der Vekens, 22-Jul-2017.) |
⊢ (𝐴 = 𝐵 → (𝐹'''𝐴) = (𝐹'''𝐵)) | ||
Theorem | nfafv 43692 | Bound-variable hypothesis builder for function value, analogous to nffv 6655. To prove a deduction version of this analogous to nffvd 6657 is not easily possible because a deduction version of nfdfat 43683 cannot be shown easily. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥(𝐹'''𝐴) | ||
Theorem | csbafv12g 43693 | Move class substitution in and out of a function value, analogous to csbfv12 6688, with a direct proof proposed by Mario Carneiro, analogous to csbov123 7177. (Contributed by Alexander van der Vekens, 23-Jul-2017.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐹'''𝐵) = (⦋𝐴 / 𝑥⦌𝐹'''⦋𝐴 / 𝑥⦌𝐵)) | ||
Theorem | afvfundmfveq 43694 | If a class is a function restricted to a member of its domain, then the function value for this member is equal for both definitions. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ (𝐹 defAt 𝐴 → (𝐹'''𝐴) = (𝐹‘𝐴)) | ||
Theorem | afvnfundmuv 43695 | If a set is not in the domain of a class or the class is not a function restricted to the set, then the function value for this set is the universe. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ (¬ 𝐹 defAt 𝐴 → (𝐹'''𝐴) = V) | ||
Theorem | ndmafv 43696 | The value of a class outside its domain is the universe, compare with ndmfv 6675. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ (¬ 𝐴 ∈ dom 𝐹 → (𝐹'''𝐴) = V) | ||
Theorem | afvvdm 43697 | If the function value of a class for an argument is a set, the argument is contained in the domain of the class. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((𝐹'''𝐴) ∈ 𝐵 → 𝐴 ∈ dom 𝐹) | ||
Theorem | nfunsnafv 43698 | If the restriction of a class to a singleton is not a function, its value is the universe, compare with nfunsn 6682. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ (¬ Fun (𝐹 ↾ {𝐴}) → (𝐹'''𝐴) = V) | ||
Theorem | afvvfunressn 43699 | If the function value of a class for an argument is a set, the class restricted to the singleton of the argument is a function. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((𝐹'''𝐴) ∈ 𝐵 → Fun (𝐹 ↾ {𝐴})) | ||
Theorem | afvprc 43700 | A function's value at a proper class is the universe, compare with fvprc 6638. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ (¬ 𝐴 ∈ V → (𝐹'''𝐴) = V) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |