Home | Metamath
Proof Explorer Theorem List (p. 74 of 470) | < 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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | eqfunressuc 7301 | Law for equality of restriction to successors. This is primarily useful when š is an ordinal, but it does not require that. (Contributed by Scott Fenton, 6-Dec-2021.) |
ā¢ (((Fun š¹ ā§ Fun šŗ) ā§ (š¹ ā¾ š) = (šŗ ā¾ š) ā§ (š ā dom š¹ ā§ š ā dom šŗ ā§ (š¹āš) = (šŗāš))) ā (š¹ ā¾ suc š) = (šŗ ā¾ suc š)) | ||
Theorem | fnssintima 7302* | Condition for subset of an intersection of an image. (Contributed by Scott Fenton, 16-Aug-2024.) |
ā¢ ((š¹ Fn š“ ā§ šµ ā š“) ā (š¶ ā ā© (š¹ ā šµ) ā āš„ ā šµ š¶ ā (š¹āš„))) | ||
Theorem | canth 7303 | No set š“ is equinumerous to its power set (Cantor's theorem), i.e., no function can map š“ onto its power set. Compare Theorem 6B(b) of [Enderton] p. 132. For the equinumerosity version, see canth2 9008. Note that š“ must be a set: this theorem does not hold when š“ is too large to be a set; see ncanth 7304 for a counterexample. (Use nex 1803 if you want the form Ā¬ āšš:š“āontoāš« š“.) (Contributed by NM, 7-Aug-1994.) (Proof shortened by Mario Carneiro, 7-Jun-2016.) |
ā¢ š“ ā V ā ā¢ Ā¬ š¹:š“āontoāš« š“ | ||
Theorem | ncanth 7304 |
Cantor's theorem fails for the universal class (which is not a set but a
proper class by vprc 5271). Specifically, the identity function maps
the
universe onto its power class. Compare canth 7303 that works for sets.
This failure comes from a limitation of the collection principle (which is necessary to avoid Russell's paradox ru 3737): š« V, being a class, cannot contain proper classes, so it is no larger than V, which is why the identity function "succeeds" in being surjective onto š« V (see pwv 4861). See also the remark in ru 3737 about NF, in which Cantor's theorem fails for sets that are "too large". This theorem gives some intuition behind that failure: in NF the universal class is a set, and it equals its own power set. (Contributed by NM, 29-Jun-2004.) (Proof shortened by BJ, 29-Dec-2023.) |
ā¢ I :Vāontoāš« V | ||
Syntax | crio 7305 | Extend class notation with restricted description binder. |
class (ā©š„ ā š“ š) | ||
Definition | df-riota 7306 | Define restricted description binder. In case there is no unique š„ such that (š„ ā š“ ā§ š) holds, it evaluates to the empty set. See also comments for df-iota 6444. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) (Revised by NM, 2-Sep-2018.) |
ā¢ (ā©š„ ā š“ š) = (ā©š„(š„ ā š“ ā§ š)) | ||
Theorem | riotaeqdv 7307* | Formula-building deduction for iota. (Contributed by NM, 15-Sep-2011.) |
ā¢ (š ā š“ = šµ) ā ā¢ (š ā (ā©š„ ā š“ š) = (ā©š„ ā šµ š)) | ||
Theorem | riotabidv 7308* | Formula-building deduction for restricted iota. (Contributed by NM, 15-Sep-2011.) |
ā¢ (š ā (š ā š)) ā ā¢ (š ā (ā©š„ ā š“ š) = (ā©š„ ā š“ š)) | ||
Theorem | riotaeqbidv 7309* | Equality deduction for restricted universal quantifier. (Contributed by NM, 15-Sep-2011.) |
ā¢ (š ā š“ = šµ) & ā¢ (š ā (š ā š)) ā ā¢ (š ā (ā©š„ ā š“ š) = (ā©š„ ā šµ š)) | ||
Theorem | riotaex 7310 | Restricted iota is a set. (Contributed by NM, 15-Sep-2011.) |
ā¢ (ā©š„ ā š“ š) ā V | ||
Theorem | riotav 7311 | An iota restricted to the universe is unrestricted. (Contributed by NM, 18-Sep-2011.) |
ā¢ (ā©š„ ā V š) = (ā©š„š) | ||
Theorem | riotauni 7312 | Restricted iota in terms of class union. (Contributed by NM, 11-Oct-2011.) |
ā¢ (ā!š„ ā š“ š ā (ā©š„ ā š“ š) = āŖ {š„ ā š“ ā£ š}) | ||
Theorem | nfriota1 7313* | The abstraction variable in a restricted iota descriptor isn't free. (Contributed by NM, 12-Oct-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) |
ā¢ ā²š„(ā©š„ ā š“ š) | ||
Theorem | nfriotadw 7314* | Deduction version of nfriota 7319 with a disjoint variable condition, which contrary to nfriotad 7318 does not require ax-13 2372. (Contributed by NM, 18-Feb-2013.) Avoid ax-13 2372. (Revised by Gino Giotto, 26-Jan-2024.) |
ā¢ ā²š¦š & ā¢ (š ā ā²š„š) & ā¢ (š ā ā²š„š“) ā ā¢ (š ā ā²š„(ā©š¦ ā š“ š)) | ||
Theorem | cbvriotaw 7315* | Change bound variable in a restricted description binder. Version of cbvriota 7320 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by NM, 18-Mar-2013.) Avoid ax-13 2372. (Revised by Gino Giotto, 26-Jan-2024.) |
ā¢ ā²š¦š & ā¢ ā²š„š & ā¢ (š„ = š¦ ā (š ā š)) ā ā¢ (ā©š„ ā š“ š) = (ā©š¦ ā š“ š) | ||
Theorem | cbvriotavw 7316* | Change bound variable in a restricted description binder. Version of cbvriotav 7321 with a disjoint variable condition, which requires fewer axioms . (Contributed by NM, 18-Mar-2013.) (Revised by Gino Giotto, 30-Sep-2024.) |
ā¢ (š„ = š¦ ā (š ā š)) ā ā¢ (ā©š„ ā š“ š) = (ā©š¦ ā š“ š) | ||
Theorem | cbvriotavwOLD 7317* | Obsolete version of cbvriotavw 7316 as of 30-Sep-2024. (Contributed by NM, 18-Mar-2013.) (Revised by Gino Giotto, 26-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
ā¢ (š„ = š¦ ā (š ā š)) ā ā¢ (ā©š„ ā š“ š) = (ā©š¦ ā š“ š) | ||
Theorem | nfriotad 7318 | Deduction version of nfriota 7319. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker nfriotadw 7314 when possible. (Contributed by NM, 18-Feb-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) (New usage is discouraged.) |
ā¢ ā²š¦š & ā¢ (š ā ā²š„š) & ā¢ (š ā ā²š„š“) ā ā¢ (š ā ā²š„(ā©š¦ ā š“ š)) | ||
Theorem | nfriota 7319* | A variable not free in a wff remains so in a restricted iota descriptor. (Contributed by NM, 12-Oct-2011.) |
ā¢ ā²š„š & ā¢ ā²š„š“ ā ā¢ ā²š„(ā©š¦ ā š“ š) | ||
Theorem | cbvriota 7320* | Change bound variable in a restricted description binder. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker cbvriotaw 7315 when possible. (Contributed by NM, 18-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) (New usage is discouraged.) |
ā¢ ā²š¦š & ā¢ ā²š„š & ā¢ (š„ = š¦ ā (š ā š)) ā ā¢ (ā©š„ ā š“ š) = (ā©š¦ ā š“ š) | ||
Theorem | cbvriotav 7321* | Change bound variable in a restricted description binder. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker cbvriotavw 7316 when possible. (Contributed by NM, 18-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) (New usage is discouraged.) |
ā¢ (š„ = š¦ ā (š ā š)) ā ā¢ (ā©š„ ā š“ š) = (ā©š¦ ā š“ š) | ||
Theorem | csbriota 7322* | Interchange class substitution and restricted description binder. (Contributed by NM, 24-Feb-2013.) (Revised by NM, 2-Sep-2018.) |
ā¢ ā¦š“ / š„ā¦(ā©š¦ ā šµ š) = (ā©š¦ ā šµ [š“ / š„]š) | ||
Theorem | riotacl2 7323 | Membership law for "the unique element in š“ such that š". (Contributed by NM, 21-Aug-2011.) (Revised by Mario Carneiro, 23-Dec-2016.) |
ā¢ (ā!š„ ā š“ š ā (ā©š„ ā š“ š) ā {š„ ā š“ ā£ š}) | ||
Theorem | riotacl 7324* | Closure of restricted iota. (Contributed by NM, 21-Aug-2011.) |
ā¢ (ā!š„ ā š“ š ā (ā©š„ ā š“ š) ā š“) | ||
Theorem | riotasbc 7325 | Substitution law for descriptions. Compare iotasbc 42432. (Contributed by NM, 23-Aug-2011.) (Proof shortened by Mario Carneiro, 24-Dec-2016.) |
ā¢ (ā!š„ ā š“ š ā [(ā©š„ ā š“ š) / š„]š) | ||
Theorem | riotabidva 7326* | Equivalent wff's yield equal restricted class abstractions (deduction form). (rabbidva 3413 analog.) (Contributed by NM, 17-Jan-2012.) |
ā¢ ((š ā§ š„ ā š“) ā (š ā š)) ā ā¢ (š ā (ā©š„ ā š“ š) = (ā©š„ ā š“ š)) | ||
Theorem | riotabiia 7327 | Equivalent wff's yield equal restricted iotas (inference form). (rabbiia 3410 analog.) (Contributed by NM, 16-Jan-2012.) |
ā¢ (š„ ā š“ ā (š ā š)) ā ā¢ (ā©š„ ā š“ š) = (ā©š„ ā š“ š) | ||
Theorem | riota1 7328* | Property of restricted iota. Compare iota1 6469. (Contributed by Mario Carneiro, 15-Oct-2016.) |
ā¢ (ā!š„ ā š“ š ā ((š„ ā š“ ā§ š) ā (ā©š„ ā š“ š) = š„)) | ||
Theorem | riota1a 7329 | Property of iota. (Contributed by NM, 23-Aug-2011.) |
ā¢ ((š„ ā š“ ā§ ā!š„ ā š“ š) ā (š ā (ā©š„(š„ ā š“ ā§ š)) = š„)) | ||
Theorem | riota2df 7330* | A deduction version of riota2f 7331. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
ā¢ ā²š„š & ā¢ (š ā ā²š„šµ) & ā¢ (š ā ā²š„š) & ā¢ (š ā šµ ā š“) & ā¢ ((š ā§ š„ = šµ) ā (š ā š)) ā ā¢ ((š ā§ ā!š„ ā š“ š) ā (š ā (ā©š„ ā š“ š) = šµ)) | ||
Theorem | riota2f 7331* | This theorem shows a condition that allows to represent a descriptor with a class expression šµ. (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) |
ā¢ ā²š„šµ & ā¢ ā²š„š & ā¢ (š„ = šµ ā (š ā š)) ā ā¢ ((šµ ā š“ ā§ ā!š„ ā š“ š) ā (š ā (ā©š„ ā š“ š) = šµ)) | ||
Theorem | riota2 7332* | This theorem shows a condition that allows to represent a descriptor with a class expression šµ. (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 10-Dec-2016.) |
ā¢ (š„ = šµ ā (š ā š)) ā ā¢ ((šµ ā š“ ā§ ā!š„ ā š“ š) ā (š ā (ā©š„ ā š“ š) = šµ)) | ||
Theorem | riotaeqimp 7333* | If two restricted iota descriptors for an equality are equal, then the terms of the equality are equal. (Contributed by AV, 6-Dec-2020.) |
ā¢ š¼ = (ā©š ā š š = š“) & ā¢ š½ = (ā©š ā š š = š“) & ā¢ (š ā ā!š ā š š = š“) & ā¢ (š ā ā!š ā š š = š“) ā ā¢ ((š ā§ š¼ = š½) ā š = š) | ||
Theorem | riotaprop 7334* | Properties of a restricted definite description operator. (Contributed by NM, 23-Nov-2013.) |
ā¢ ā²š„š & ā¢ šµ = (ā©š„ ā š“ š) & ā¢ (š„ = šµ ā (š ā š)) ā ā¢ (ā!š„ ā š“ š ā (šµ ā š“ ā§ š)) | ||
Theorem | riota5f 7335* | A method for computing restricted iota. (Contributed by NM, 16-Apr-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
ā¢ (š ā ā²š„šµ) & ā¢ (š ā šµ ā š“) & ā¢ ((š ā§ š„ ā š“) ā (š ā š„ = šµ)) ā ā¢ (š ā (ā©š„ ā š“ š) = šµ) | ||
Theorem | riota5 7336* | A method for computing restricted iota. (Contributed by NM, 20-Oct-2011.) (Revised by Mario Carneiro, 6-Dec-2016.) |
ā¢ (š ā šµ ā š“) & ā¢ ((š ā§ š„ ā š“) ā (š ā š„ = šµ)) ā ā¢ (š ā (ā©š„ ā š“ š) = šµ) | ||
Theorem | riotass2 7337* | Restriction of a unique element to a smaller class. (Contributed by NM, 21-Aug-2011.) (Revised by NM, 22-Mar-2013.) |
ā¢ (((š“ ā šµ ā§ āš„ ā š“ (š ā š)) ā§ (āš„ ā š“ š ā§ ā!š„ ā šµ š)) ā (ā©š„ ā š“ š) = (ā©š„ ā šµ š)) | ||
Theorem | riotass 7338* | Restriction of a unique element to a smaller class. (Contributed by NM, 19-Oct-2005.) (Revised by Mario Carneiro, 24-Dec-2016.) |
ā¢ ((š“ ā šµ ā§ āš„ ā š“ š ā§ ā!š„ ā šµ š) ā (ā©š„ ā š“ š) = (ā©š„ ā šµ š)) | ||
Theorem | moriotass 7339* | Restriction of a unique element to a smaller class. (Contributed by NM, 19-Feb-2006.) (Revised by NM, 16-Jun-2017.) |
ā¢ ((š“ ā šµ ā§ āš„ ā š“ š ā§ ā*š„ ā šµ š) ā (ā©š„ ā š“ š) = (ā©š„ ā šµ š)) | ||
Theorem | snriota 7340 | A restricted class abstraction with a unique member can be expressed as a singleton. (Contributed by NM, 30-May-2006.) |
ā¢ (ā!š„ ā š“ š ā {š„ ā š“ ā£ š} = {(ā©š„ ā š“ š)}) | ||
Theorem | riotaxfrd 7341* | Change the variable š„ in the expression for "the unique š„ such that š " to another variable š¦ contained in expression šµ. Use reuhypd 5373 to eliminate the last hypothesis. (Contributed by NM, 16-Jan-2012.) (Revised by Mario Carneiro, 15-Oct-2016.) |
ā¢ ā²š¦š¶ & ā¢ ((š ā§ š¦ ā š“) ā šµ ā š“) & ā¢ ((š ā§ (ā©š¦ ā š“ š) ā š“) ā š¶ ā š“) & ā¢ (š„ = šµ ā (š ā š)) & ā¢ (š¦ = (ā©š¦ ā š“ š) ā šµ = š¶) & ā¢ ((š ā§ š„ ā š“) ā ā!š¦ ā š“ š„ = šµ) ā ā¢ ((š ā§ ā!š„ ā š“ š) ā (ā©š„ ā š“ š) = š¶) | ||
Theorem | eusvobj2 7342* | Specify the same property in two ways when class šµ(š¦) is single-valued. (Contributed by NM, 1-Nov-2010.) (Proof shortened by Mario Carneiro, 24-Dec-2016.) |
ā¢ šµ ā V ā ā¢ (ā!š„āš¦ ā š“ š„ = šµ ā (āš¦ ā š“ š„ = šµ ā āš¦ ā š“ š„ = šµ)) | ||
Theorem | eusvobj1 7343* | Specify the same object in two ways when class šµ(š¦) is single-valued. (Contributed by NM, 1-Nov-2010.) (Proof shortened by Mario Carneiro, 19-Nov-2016.) |
ā¢ šµ ā V ā ā¢ (ā!š„āš¦ ā š“ š„ = šµ ā (ā©š„āš¦ ā š“ š„ = šµ) = (ā©š„āš¦ ā š“ š„ = šµ)) | ||
Theorem | f1ofveu 7344* | There is one domain element for each value of a one-to-one onto function. (Contributed by NM, 26-May-2006.) |
ā¢ ((š¹:š“ā1-1-ontoāšµ ā§ š¶ ā šµ) ā ā!š„ ā š“ (š¹āš„) = š¶) | ||
Theorem | f1ocnvfv3 7345* | Value of the converse of a one-to-one onto function. (Contributed by NM, 26-May-2006.) (Proof shortened by Mario Carneiro, 24-Dec-2016.) |
ā¢ ((š¹:š“ā1-1-ontoāšµ ā§ š¶ ā šµ) ā (ā”š¹āš¶) = (ā©š„ ā š“ (š¹āš„) = š¶)) | ||
Theorem | riotaund 7346* | Restricted iota equals the empty set when not meaningful. (Contributed by NM, 16-Jan-2012.) (Revised by Mario Carneiro, 15-Oct-2016.) (Revised by NM, 13-Sep-2018.) |
ā¢ (Ā¬ ā!š„ ā š“ š ā (ā©š„ ā š“ š) = ā ) | ||
Theorem | riotassuni 7347* | The restricted iota class is limited in size by the base set. (Contributed by Mario Carneiro, 24-Dec-2016.) |
ā¢ (ā©š„ ā š“ š) ā (š« āŖ š“ āŖ āŖ š“) | ||
Theorem | riotaclb 7348* | Bidirectional closure of restricted iota when domain is not empty. (Contributed by NM, 28-Feb-2013.) (Revised by Mario Carneiro, 24-Dec-2016.) (Revised by NM, 13-Sep-2018.) |
ā¢ (Ā¬ ā ā š“ ā (ā!š„ ā š“ š ā (ā©š„ ā š“ š) ā š“)) | ||
Theorem | riotarab 7349* | Restricted iota of a restricted abstraction. (Contributed by Scott Fenton, 8-Aug-2024.) |
ā¢ (š„ = š¦ ā (š ā š)) ā ā¢ (ā©š„ ā {š¦ ā š“ ā£ š}š) = (ā©š„ ā š“ (š ā§ š)) | ||
Syntax | co 7350 | 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 parentheses. Since operation values are the only possible class expressions consisting of three class expressions in a row surrounded by parentheses, the syntax is unambiguous. (For an example of how syntax could become ambiguous if we are not careful, see the comment in cneg 11320.) |
class (š“š¹šµ) | ||
Syntax | coprab 7351 | Extend class notation to include class abstraction (class builder) of nested ordered pairs. |
class {āØāØš„, š¦ā©, š§ā© ā£ š} | ||
Syntax | cmpo 7352 | Extend the definition of a class to include maps-to notation for defining an operation via a rule. |
class (š„ ā š“, š¦ ā šµ ā¦ š¶) | ||
Definition | df-ov 7353 | Define the value of an operation. Definition of operation value in [Enderton] p. 79. Note that the syntax is simply three class expressions in a row bracketed by parentheses. There are 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. For example, if class š¹ is the operation + and arguments š“ and šµ are 3 and 2, the expression (3 + 2) can be proved to equal 5 (see 3p2e5 12238). This definition is well-defined, although not very meaningful, when classes š“ and/or šµ are proper classes (i.e. are not sets); see ovprc1 7389 and ovprc2 7390. On the other hand, we often find uses for this definition when š¹ is a proper class, such as +o in oav 8425. š¹ is normally equal to a class of nested ordered pairs of the form defined by df-oprab 7354. (Contributed by NM, 28-Feb-1995.) |
ā¢ (š“š¹šµ) = (š¹āāØš“, šµā©) | ||
Definition | df-oprab 7354* | Define the class abstraction (class builder) of a collection of nested ordered pairs (for use in defining operations). This is a special case of Definition 4.16 of [TakeutiZaring] p. 14. Normally š„, š¦, and š§ are distinct, although the definition doesn't strictly require it. See df-ov 7353 for the value of an operation. The brace notation is called "class abstraction" by Quine; it is also called a "class builder" in the literature. The value of an operation given by a class abstraction is given by ovmpo 7508. (Contributed by NM, 12-Mar-1995.) |
ā¢ {āØāØš„, š¦ā©, š§ā© ā£ š} = {š¤ ā£ āš„āš¦āš§(š¤ = āØāØš„, š¦ā©, š§ā© ā§ š)} | ||
Definition | df-mpo 7355* | Define maps-to notation for defining an operation via a rule. Read as "the operation defined by the map from š„, š¦ (in š“ Ć šµ) to š¶(š„, š¦)". An extension of df-mpt 5188 for two arguments. (Contributed by NM, 17-Feb-2008.) |
ā¢ (š„ ā š“, š¦ ā šµ ā¦ š¶) = {āØāØš„, š¦ā©, š§ā© ā£ ((š„ ā š“ ā§ š¦ ā šµ) ā§ š§ = š¶)} | ||
Theorem | oveq 7356 | Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.) |
ā¢ (š¹ = šŗ ā (š“š¹šµ) = (š“šŗšµ)) | ||
Theorem | oveq1 7357 | Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.) |
ā¢ (š“ = šµ ā (š“š¹š¶) = (šµš¹š¶)) | ||
Theorem | oveq2 7358 | Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.) |
ā¢ (š“ = šµ ā (š¶š¹š“) = (š¶š¹šµ)) | ||
Theorem | oveq12 7359 | Equality theorem for operation value. (Contributed by NM, 16-Jul-1995.) |
ā¢ ((š“ = šµ ā§ š¶ = š·) ā (š“š¹š¶) = (šµš¹š·)) | ||
Theorem | oveq1i 7360 | Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) |
ā¢ š“ = šµ ā ā¢ (š“š¹š¶) = (šµš¹š¶) | ||
Theorem | oveq2i 7361 | Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) |
ā¢ š“ = šµ ā ā¢ (š¶š¹š“) = (š¶š¹šµ) | ||
Theorem | oveq12i 7362 | Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
ā¢ š“ = šµ & ā¢ š¶ = š· ā ā¢ (š“š¹š¶) = (šµš¹š·) | ||
Theorem | oveqi 7363 | Equality inference for operation value. (Contributed by NM, 24-Nov-2007.) |
ā¢ š“ = šµ ā ā¢ (š¶š“š·) = (š¶šµš·) | ||
Theorem | oveq123i 7364 | Equality inference for operation value. (Contributed by FL, 11-Jul-2010.) |
ā¢ š“ = š¶ & ā¢ šµ = š· & ā¢ š¹ = šŗ ā ā¢ (š“š¹šµ) = (š¶šŗš·) | ||
Theorem | oveq1d 7365 | Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.) |
ā¢ (š ā š“ = šµ) ā ā¢ (š ā (š“š¹š¶) = (šµš¹š¶)) | ||
Theorem | oveq2d 7366 | Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.) |
ā¢ (š ā š“ = šµ) ā ā¢ (š ā (š¶š¹š“) = (š¶š¹šµ)) | ||
Theorem | oveqd 7367 | Equality deduction for operation value. (Contributed by NM, 9-Sep-2006.) |
ā¢ (š ā š“ = šµ) ā ā¢ (š ā (š¶š“š·) = (š¶šµš·)) | ||
Theorem | oveq12d 7368 | Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
ā¢ (š ā š“ = šµ) & ā¢ (š ā š¶ = š·) ā ā¢ (š ā (š“š¹š¶) = (šµš¹š·)) | ||
Theorem | oveqan12d 7369 | Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.) |
ā¢ (š ā š“ = šµ) & ā¢ (š ā š¶ = š·) ā ā¢ ((š ā§ š) ā (š“š¹š¶) = (šµš¹š·)) | ||
Theorem | oveqan12rd 7370 | Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.) |
ā¢ (š ā š“ = šµ) & ā¢ (š ā š¶ = š·) ā ā¢ ((š ā§ š) ā (š“š¹š¶) = (šµš¹š·)) | ||
Theorem | oveq123d 7371 | Equality deduction for operation value. (Contributed by FL, 22-Dec-2008.) |
ā¢ (š ā š¹ = šŗ) & ā¢ (š ā š“ = šµ) & ā¢ (š ā š¶ = š·) ā ā¢ (š ā (š“š¹š¶) = (šµšŗš·)) | ||
Theorem | fvoveq1d 7372 | Equality deduction for nested function and operation value. (Contributed by AV, 23-Jul-2022.) |
ā¢ (š ā š“ = šµ) ā ā¢ (š ā (š¹ā(š“šš¶)) = (š¹ā(šµšš¶))) | ||
Theorem | fvoveq1 7373 | Equality theorem for nested function and operation value. Closed form of fvoveq1d 7372. (Contributed by AV, 23-Jul-2022.) |
ā¢ (š“ = šµ ā (š¹ā(š“šš¶)) = (š¹ā(šµšš¶))) | ||
Theorem | ovanraleqv 7374* | Equality theorem for a conjunction with an operation values within a restricted universal quantification. Technical theorem to be used to reduce the size of a significant number of proofs. (Contributed by AV, 13-Aug-2022.) |
ā¢ (šµ = š ā (š ā š)) ā ā¢ (šµ = š ā (āš„ ā š (š ā§ (š“ Ā· šµ) = š¶) ā āš„ ā š (š ā§ (š“ Ā· š) = š¶))) | ||
Theorem | imbrov2fvoveq 7375 | Equality theorem for nested function and operation value in an implication for a binary relation. Technical theorem to be used to reduce the size of a significant number of proofs. (Contributed by AV, 17-Aug-2022.) |
ā¢ (š = š ā (š ā š)) ā ā¢ (š = š ā ((š ā (š¹ā((šŗāš) Ā· š))š š“) ā (š ā (š¹ā((šŗāš) Ā· š))š š“))) | ||
Theorem | ovrspc2v 7376* | If an operation value is element of a class for all operands of two classes, then the operation value is an element of the class for specific operands of the two classes. (Contributed by Mario Carneiro, 6-Dec-2014.) |
ā¢ (((š ā š“ ā§ š ā šµ) ā§ āš„ ā š“ āš¦ ā šµ (š„š¹š¦) ā š¶) ā (šš¹š) ā š¶) | ||
Theorem | oveqrspc2v 7377* | Restricted specialization of operands, using implicit substitution. (Contributed by Mario Carneiro, 6-Dec-2014.) |
ā¢ ((š ā§ (š„ ā š“ ā§ š¦ ā šµ)) ā (š„š¹š¦) = (š„šŗš¦)) ā ā¢ ((š ā§ (š ā š“ ā§ š ā šµ)) ā (šš¹š) = (ššŗš)) | ||
Theorem | oveqdr 7378 | Equality of two operations for any two operands. Useful in proofs using *propd theorems. (Contributed by Mario Carneiro, 29-Jun-2015.) |
ā¢ (š ā š¹ = šŗ) ā ā¢ ((š ā§ š) ā (š„š¹š¦) = (š„šŗš¦)) | ||
Theorem | nfovd 7379 | Deduction version of bound-variable hypothesis builder nfov 7380. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
ā¢ (š ā ā²š„š“) & ā¢ (š ā ā²š„š¹) & ā¢ (š ā ā²š„šµ) ā ā¢ (š ā ā²š„(š“š¹šµ)) | ||
Theorem | nfov 7380 | Bound-variable hypothesis builder for operation value. (Contributed by NM, 4-May-2004.) |
ā¢ ā²š„š“ & ā¢ ā²š„š¹ & ā¢ ā²š„šµ ā ā¢ ā²š„(š“š¹šµ) | ||
Theorem | oprabidw 7381* | The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. Version of oprabid 7382 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by Mario Carneiro, 20-Mar-2013.) Avoid ax-13 2372. (Revised by Gino Giotto, 26-Jan-2024.) |
ā¢ (āØāØš„, š¦ā©, š§ā© ā {āØāØš„, š¦ā©, š§ā© ā£ š} ā š) | ||
Theorem | oprabid 7382 | The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker oprabidw 7381 when possible. (Contributed by Mario Carneiro, 20-Mar-2013.) (New usage is discouraged.) |
ā¢ (āØāØš„, š¦ā©, š§ā© ā {āØāØš„, š¦ā©, š§ā© ā£ š} ā š) | ||
Theorem | ovex 7383 | The result of an operation is a set. (Contributed by NM, 13-Mar-1995.) |
ā¢ (š“š¹šµ) ā V | ||
Theorem | ovexi 7384 | The result of an operation is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
ā¢ š“ = (šµš¹š¶) ā ā¢ š“ ā V | ||
Theorem | ovexd 7385 | The result of an operation is a set. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
ā¢ (š ā (š“š¹šµ) ā V) | ||
Theorem | ovssunirn 7386 | The result of an operation value is always a subset of the union of the range. (Contributed by Mario Carneiro, 12-Jan-2017.) |
ā¢ (šš¹š) ā āŖ ran š¹ | ||
Theorem | 0ov 7387 | Operation value of the empty set. (Contributed by AV, 15-May-2021.) |
ā¢ (š“ā šµ) = ā | ||
Theorem | ovprc 7388 | The value of an operation when the one of the arguments is a proper class. Note: this theorem is dependent on our particular definitions of operation value, function value, and ordered pair. (Contributed by Mario Carneiro, 26-Apr-2015.) |
ā¢ Rel dom š¹ ā ā¢ (Ā¬ (š“ ā V ā§ šµ ā V) ā (š“š¹šµ) = ā ) | ||
Theorem | ovprc1 7389 | The value of an operation when the first argument is a proper class. (Contributed by NM, 16-Jun-2004.) |
ā¢ Rel dom š¹ ā ā¢ (Ā¬ š“ ā V ā (š“š¹šµ) = ā ) | ||
Theorem | ovprc2 7390 | The value of an operation when the second argument is a proper class. (Contributed by Mario Carneiro, 26-Apr-2015.) |
ā¢ Rel dom š¹ ā ā¢ (Ā¬ šµ ā V ā (š“š¹šµ) = ā ) | ||
Theorem | ovrcl 7391 | Reverse closure for an operation value. (Contributed by Mario Carneiro, 5-May-2015.) |
ā¢ Rel dom š¹ ā ā¢ (š¶ ā (š“š¹šµ) ā (š“ ā V ā§ šµ ā V)) | ||
Theorem | csbov123 7392 | Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.) (Revised by NM, 23-Aug-2018.) |
ā¢ ā¦š“ / š„ā¦(šµš¹š¶) = (ā¦š“ / š„ā¦šµā¦š“ / š„ā¦š¹ā¦š“ / š„ā¦š¶) | ||
Theorem | csbov 7393* | Move class substitution in and out of an operation. (Contributed by NM, 23-Aug-2018.) |
ā¢ ā¦š“ / š„ā¦(šµš¹š¶) = (šµā¦š“ / š„ā¦š¹š¶) | ||
Theorem | csbov12g 7394* | Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.) |
ā¢ (š“ ā š ā ā¦š“ / š„ā¦(šµš¹š¶) = (ā¦š“ / š„ā¦šµš¹ā¦š“ / š„ā¦š¶)) | ||
Theorem | csbov1g 7395* | Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.) |
ā¢ (š“ ā š ā ā¦š“ / š„ā¦(šµš¹š¶) = (ā¦š“ / š„ā¦šµš¹š¶)) | ||
Theorem | csbov2g 7396* | Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.) |
ā¢ (š“ ā š ā ā¦š“ / š„ā¦(šµš¹š¶) = (šµš¹ā¦š“ / š„ā¦š¶)) | ||
Theorem | rspceov 7397* | A frequently used special case of rspc2ev 3591 for operation values. (Contributed by NM, 21-Mar-2007.) |
ā¢ ((š¶ ā š“ ā§ š· ā šµ ā§ š = (š¶š¹š·)) ā āš„ ā š“ āš¦ ā šµ š = (š„š¹š¦)) | ||
Theorem | elovimad 7398 | Elementhood of the image set of an operation value. (Contributed by Thierry Arnoux, 13-Mar-2017.) |
ā¢ (š ā š“ ā š¶) & ā¢ (š ā šµ ā š·) & ā¢ (š ā Fun š¹) & ā¢ (š ā (š¶ Ć š·) ā dom š¹) ā ā¢ (š ā (š“š¹šµ) ā (š¹ ā (š¶ Ć š·))) | ||
Theorem | fnbrovb 7399 | Value of a binary operation expressed as a binary relation. See also fnbrfvb 6891 for functions on Cartesian products. (Contributed by BJ, 15-Feb-2022.) |
ā¢ ((š¹ Fn (š Ć š) ā§ (š“ ā š ā§ šµ ā š)) ā ((š“š¹šµ) = š¶ ā āØš“, šµā©š¹š¶)) | ||
Theorem | fnotovb 7400 | Equivalence of operation value and ordered triple membership, analogous to fnopfvb 6892. (Contributed by NM, 17-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.) (Proof shortened by BJ, 15-Feb-2022.) |
ā¢ ((š¹ Fn (š“ Ć šµ) ā§ š¶ ā š“ ā§ š· ā šµ) ā ((š¶š¹š·) = š ā āØš¶, š·, š ā© ā š¹)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |