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-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fnssintima 7301* | Condition for subset of an intersection of an image. (Contributed by Scott Fenton, 16-Aug-2024.) |
ā¢ ((š¹ Fn š“ ā§ šµ ā š“) ā (š¶ ā ā© (š¹ ā šµ) ā āš„ ā šµ š¶ ā (š¹āš„))) | ||
Theorem | canth 7302 | 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 9007. Note that š“ must be a set: this theorem does not hold when š“ is too large to be a set; see ncanth 7303 for a counterexample. (Use nex 1802 if you want the form Ā¬ āšš:š“āontoāš« š“.) (Contributed by NM, 7-Aug-1994.) (Proof shortened by Mario Carneiro, 7-Jun-2016.) |
ā¢ š“ ā V ā ā¢ Ā¬ š¹:š“āontoāš« š“ | ||
Theorem | ncanth 7303 |
Cantor's theorem fails for the universal class (which is not a set but a
proper class by vprc 5270). Specifically, the identity function maps
the
universe onto its power class. Compare canth 7302 that works for sets.
This failure comes from a limitation of the collection principle (which is necessary to avoid Russell's paradox ru 3736): š« 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 4860). See also the remark in ru 3736 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 7304 | Extend class notation with restricted description binder. |
class (ā©š„ ā š“ š) | ||
Definition | df-riota 7305 | 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 6443. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) (Revised by NM, 2-Sep-2018.) |
ā¢ (ā©š„ ā š“ š) = (ā©š„(š„ ā š“ ā§ š)) | ||
Theorem | riotaeqdv 7306* | Formula-building deduction for iota. (Contributed by NM, 15-Sep-2011.) |
ā¢ (š ā š“ = šµ) ā ā¢ (š ā (ā©š„ ā š“ š) = (ā©š„ ā šµ š)) | ||
Theorem | riotabidv 7307* | Formula-building deduction for restricted iota. (Contributed by NM, 15-Sep-2011.) |
ā¢ (š ā (š ā š)) ā ā¢ (š ā (ā©š„ ā š“ š) = (ā©š„ ā š“ š)) | ||
Theorem | riotaeqbidv 7308* | Equality deduction for restricted universal quantifier. (Contributed by NM, 15-Sep-2011.) |
ā¢ (š ā š“ = šµ) & ā¢ (š ā (š ā š)) ā ā¢ (š ā (ā©š„ ā š“ š) = (ā©š„ ā šµ š)) | ||
Theorem | riotaex 7309 | Restricted iota is a set. (Contributed by NM, 15-Sep-2011.) |
ā¢ (ā©š„ ā š“ š) ā V | ||
Theorem | riotav 7310 | An iota restricted to the universe is unrestricted. (Contributed by NM, 18-Sep-2011.) |
ā¢ (ā©š„ ā V š) = (ā©š„š) | ||
Theorem | riotauni 7311 | Restricted iota in terms of class union. (Contributed by NM, 11-Oct-2011.) |
ā¢ (ā!š„ ā š“ š ā (ā©š„ ā š“ š) = āŖ {š„ ā š“ ā£ š}) | ||
Theorem | nfriota1 7312* | 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 7313* | Deduction version of nfriota 7318 with a disjoint variable condition, which contrary to nfriotad 7317 does not require ax-13 2371. (Contributed by NM, 18-Feb-2013.) Avoid ax-13 2371. (Revised by Gino Giotto, 26-Jan-2024.) |
ā¢ ā²š¦š & ā¢ (š ā ā²š„š) & ā¢ (š ā ā²š„š“) ā ā¢ (š ā ā²š„(ā©š¦ ā š“ š)) | ||
Theorem | cbvriotaw 7314* | Change bound variable in a restricted description binder. Version of cbvriota 7319 with a disjoint variable condition, which does not require ax-13 2371. (Contributed by NM, 18-Mar-2013.) Avoid ax-13 2371. (Revised by Gino Giotto, 26-Jan-2024.) |
ā¢ ā²š¦š & ā¢ ā²š„š & ā¢ (š„ = š¦ ā (š ā š)) ā ā¢ (ā©š„ ā š“ š) = (ā©š¦ ā š“ š) | ||
Theorem | cbvriotavw 7315* | Change bound variable in a restricted description binder. Version of cbvriotav 7320 with a disjoint variable condition, which requires fewer axioms . (Contributed by NM, 18-Mar-2013.) (Revised by Gino Giotto, 30-Sep-2024.) |
ā¢ (š„ = š¦ ā (š ā š)) ā ā¢ (ā©š„ ā š“ š) = (ā©š¦ ā š“ š) | ||
Theorem | cbvriotavwOLD 7316* | Obsolete version of cbvriotavw 7315 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 7317 | Deduction version of nfriota 7318. Usage of this theorem is discouraged because it depends on ax-13 2371. Use the weaker nfriotadw 7313 when possible. (Contributed by NM, 18-Feb-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) (New usage is discouraged.) |
ā¢ ā²š¦š & ā¢ (š ā ā²š„š) & ā¢ (š ā ā²š„š“) ā ā¢ (š ā ā²š„(ā©š¦ ā š“ š)) | ||
Theorem | nfriota 7318* | A variable not free in a wff remains so in a restricted iota descriptor. (Contributed by NM, 12-Oct-2011.) |
ā¢ ā²š„š & ā¢ ā²š„š“ ā ā¢ ā²š„(ā©š¦ ā š“ š) | ||
Theorem | cbvriota 7319* | Change bound variable in a restricted description binder. Usage of this theorem is discouraged because it depends on ax-13 2371. Use the weaker cbvriotaw 7314 when possible. (Contributed by NM, 18-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) (New usage is discouraged.) |
ā¢ ā²š¦š & ā¢ ā²š„š & ā¢ (š„ = š¦ ā (š ā š)) ā ā¢ (ā©š„ ā š“ š) = (ā©š¦ ā š“ š) | ||
Theorem | cbvriotav 7320* | Change bound variable in a restricted description binder. Usage of this theorem is discouraged because it depends on ax-13 2371. Use the weaker cbvriotavw 7315 when possible. (Contributed by NM, 18-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) (New usage is discouraged.) |
ā¢ (š„ = š¦ ā (š ā š)) ā ā¢ (ā©š„ ā š“ š) = (ā©š¦ ā š“ š) | ||
Theorem | csbriota 7321* | Interchange class substitution and restricted description binder. (Contributed by NM, 24-Feb-2013.) (Revised by NM, 2-Sep-2018.) |
ā¢ ā¦š“ / š„ā¦(ā©š¦ ā šµ š) = (ā©š¦ ā šµ [š“ / š„]š) | ||
Theorem | riotacl2 7322 | Membership law for "the unique element in š“ such that š". (Contributed by NM, 21-Aug-2011.) (Revised by Mario Carneiro, 23-Dec-2016.) |
ā¢ (ā!š„ ā š“ š ā (ā©š„ ā š“ š) ā {š„ ā š“ ā£ š}) | ||
Theorem | riotacl 7323* | Closure of restricted iota. (Contributed by NM, 21-Aug-2011.) |
ā¢ (ā!š„ ā š“ š ā (ā©š„ ā š“ š) ā š“) | ||
Theorem | riotasbc 7324 | Substitution law for descriptions. Compare iotasbc 42463. (Contributed by NM, 23-Aug-2011.) (Proof shortened by Mario Carneiro, 24-Dec-2016.) |
ā¢ (ā!š„ ā š“ š ā [(ā©š„ ā š“ š) / š„]š) | ||
Theorem | riotabidva 7325* | Equivalent wff's yield equal restricted class abstractions (deduction form). (rabbidva 3412 analog.) (Contributed by NM, 17-Jan-2012.) |
ā¢ ((š ā§ š„ ā š“) ā (š ā š)) ā ā¢ (š ā (ā©š„ ā š“ š) = (ā©š„ ā š“ š)) | ||
Theorem | riotabiia 7326 | Equivalent wff's yield equal restricted iotas (inference form). (rabbiia 3409 analog.) (Contributed by NM, 16-Jan-2012.) |
ā¢ (š„ ā š“ ā (š ā š)) ā ā¢ (ā©š„ ā š“ š) = (ā©š„ ā š“ š) | ||
Theorem | riota1 7327* | Property of restricted iota. Compare iota1 6468. (Contributed by Mario Carneiro, 15-Oct-2016.) |
ā¢ (ā!š„ ā š“ š ā ((š„ ā š“ ā§ š) ā (ā©š„ ā š“ š) = š„)) | ||
Theorem | riota1a 7328 | Property of iota. (Contributed by NM, 23-Aug-2011.) |
ā¢ ((š„ ā š“ ā§ ā!š„ ā š“ š) ā (š ā (ā©š„(š„ ā š“ ā§ š)) = š„)) | ||
Theorem | riota2df 7329* | A deduction version of riota2f 7330. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
ā¢ ā²š„š & ā¢ (š ā ā²š„šµ) & ā¢ (š ā ā²š„š) & ā¢ (š ā šµ ā š“) & ā¢ ((š ā§ š„ = šµ) ā (š ā š)) ā ā¢ ((š ā§ ā!š„ ā š“ š) ā (š ā (ā©š„ ā š“ š) = šµ)) | ||
Theorem | riota2f 7330* | 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 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, 10-Dec-2016.) |
ā¢ (š„ = šµ ā (š ā š)) ā ā¢ ((šµ ā š“ ā§ ā!š„ ā š“ š) ā (š ā (ā©š„ ā š“ š) = šµ)) | ||
Theorem | riotaeqimp 7332* | 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 7333* | Properties of a restricted definite description operator. (Contributed by NM, 23-Nov-2013.) |
ā¢ ā²š„š & ā¢ šµ = (ā©š„ ā š“ š) & ā¢ (š„ = šµ ā (š ā š)) ā ā¢ (ā!š„ ā š“ š ā (šµ ā š“ ā§ š)) | ||
Theorem | riota5f 7334* | A method for computing restricted iota. (Contributed by NM, 16-Apr-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
ā¢ (š ā ā²š„šµ) & ā¢ (š ā šµ ā š“) & ā¢ ((š ā§ š„ ā š“) ā (š ā š„ = šµ)) ā ā¢ (š ā (ā©š„ ā š“ š) = šµ) | ||
Theorem | riota5 7335* | A method for computing restricted iota. (Contributed by NM, 20-Oct-2011.) (Revised by Mario Carneiro, 6-Dec-2016.) |
ā¢ (š ā šµ ā š“) & ā¢ ((š ā§ š„ ā š“) ā (š ā š„ = šµ)) ā ā¢ (š ā (ā©š„ ā š“ š) = šµ) | ||
Theorem | riotass2 7336* | Restriction of a unique element to a smaller class. (Contributed by NM, 21-Aug-2011.) (Revised by NM, 22-Mar-2013.) |
ā¢ (((š“ ā šµ ā§ āš„ ā š“ (š ā š)) ā§ (āš„ ā š“ š ā§ ā!š„ ā šµ š)) ā (ā©š„ ā š“ š) = (ā©š„ ā šµ š)) | ||
Theorem | riotass 7337* | Restriction of a unique element to a smaller class. (Contributed by NM, 19-Oct-2005.) (Revised by Mario Carneiro, 24-Dec-2016.) |
ā¢ ((š“ ā šµ ā§ āš„ ā š“ š ā§ ā!š„ ā šµ š) ā (ā©š„ ā š“ š) = (ā©š„ ā šµ š)) | ||
Theorem | moriotass 7338* | Restriction of a unique element to a smaller class. (Contributed by NM, 19-Feb-2006.) (Revised by NM, 16-Jun-2017.) |
ā¢ ((š“ ā šµ ā§ āš„ ā š“ š ā§ ā*š„ ā šµ š) ā (ā©š„ ā š“ š) = (ā©š„ ā šµ š)) | ||
Theorem | snriota 7339 | A restricted class abstraction with a unique member can be expressed as a singleton. (Contributed by NM, 30-May-2006.) |
ā¢ (ā!š„ ā š“ š ā {š„ ā š“ ā£ š} = {(ā©š„ ā š“ š)}) | ||
Theorem | riotaxfrd 7340* | Change the variable š„ in the expression for "the unique š„ such that š " to another variable š¦ contained in expression šµ. Use reuhypd 5372 to eliminate the last hypothesis. (Contributed by NM, 16-Jan-2012.) (Revised by Mario Carneiro, 15-Oct-2016.) |
ā¢ ā²š¦š¶ & ā¢ ((š ā§ š¦ ā š“) ā šµ ā š“) & ā¢ ((š ā§ (ā©š¦ ā š“ š) ā š“) ā š¶ ā š“) & ā¢ (š„ = šµ ā (š ā š)) & ā¢ (š¦ = (ā©š¦ ā š“ š) ā šµ = š¶) & ā¢ ((š ā§ š„ ā š“) ā ā!š¦ ā š“ š„ = šµ) ā ā¢ ((š ā§ ā!š„ ā š“ š) ā (ā©š„ ā š“ š) = š¶) | ||
Theorem | eusvobj2 7341* | 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 7342* | 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 7343* | 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 7344* | 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 7345* | 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 7346* | The restricted iota class is limited in size by the base set. (Contributed by Mario Carneiro, 24-Dec-2016.) |
ā¢ (ā©š„ ā š“ š) ā (š« āŖ š“ āŖ āŖ š“) | ||
Theorem | riotaclb 7347* | 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 7348* | Restricted iota of a restricted abstraction. (Contributed by Scott Fenton, 8-Aug-2024.) |
ā¢ (š„ = š¦ ā (š ā š)) ā ā¢ (ā©š„ ā {š¦ ā š“ ā£ š}š) = (ā©š„ ā š“ (š ā§ š)) | ||
Syntax | co 7349 | 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 11319.) |
class (š“š¹šµ) | ||
Syntax | coprab 7350 | Extend class notation to include class abstraction (class builder) of nested ordered pairs. |
class {āØāØš„, š¦ā©, š§ā© ā£ š} | ||
Syntax | cmpo 7351 | Extend the definition of a class to include maps-to notation for defining an operation via a rule. |
class (š„ ā š“, š¦ ā šµ ā¦ š¶) | ||
Definition | df-ov 7352 | 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 12237). This definition is well-defined, although not very meaningful, when classes š“ and/or šµ are proper classes (i.e. are not sets); see ovprc1 7388 and ovprc2 7389. On the other hand, we often find uses for this definition when š¹ is a proper class, such as +o in oav 8424. š¹ is normally equal to a class of nested ordered pairs of the form defined by df-oprab 7353. (Contributed by NM, 28-Feb-1995.) |
ā¢ (š“š¹šµ) = (š¹āāØš“, šµā©) | ||
Definition | df-oprab 7353* | 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 7352 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 7507. (Contributed by NM, 12-Mar-1995.) |
ā¢ {āØāØš„, š¦ā©, š§ā© ā£ š} = {š¤ ā£ āš„āš¦āš§(š¤ = āØāØš„, š¦ā©, š§ā© ā§ š)} | ||
Definition | df-mpo 7354* | 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 5187 for two arguments. (Contributed by NM, 17-Feb-2008.) |
ā¢ (š„ ā š“, š¦ ā šµ ā¦ š¶) = {āØāØš„, š¦ā©, š§ā© ā£ ((š„ ā š“ ā§ š¦ ā šµ) ā§ š§ = š¶)} | ||
Theorem | oveq 7355 | Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.) |
ā¢ (š¹ = šŗ ā (š“š¹šµ) = (š“šŗšµ)) | ||
Theorem | oveq1 7356 | Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.) |
ā¢ (š“ = šµ ā (š“š¹š¶) = (šµš¹š¶)) | ||
Theorem | oveq2 7357 | Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.) |
ā¢ (š“ = šµ ā (š¶š¹š“) = (š¶š¹šµ)) | ||
Theorem | oveq12 7358 | Equality theorem for operation value. (Contributed by NM, 16-Jul-1995.) |
ā¢ ((š“ = šµ ā§ š¶ = š·) ā (š“š¹š¶) = (šµš¹š·)) | ||
Theorem | oveq1i 7359 | Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) |
ā¢ š“ = šµ ā ā¢ (š“š¹š¶) = (šµš¹š¶) | ||
Theorem | oveq2i 7360 | Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) |
ā¢ š“ = šµ ā ā¢ (š¶š¹š“) = (š¶š¹šµ) | ||
Theorem | oveq12i 7361 | Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
ā¢ š“ = šµ & ā¢ š¶ = š· ā ā¢ (š“š¹š¶) = (šµš¹š·) | ||
Theorem | oveqi 7362 | Equality inference for operation value. (Contributed by NM, 24-Nov-2007.) |
ā¢ š“ = šµ ā ā¢ (š¶š“š·) = (š¶šµš·) | ||
Theorem | oveq123i 7363 | Equality inference for operation value. (Contributed by FL, 11-Jul-2010.) |
ā¢ š“ = š¶ & ā¢ šµ = š· & ā¢ š¹ = šŗ ā ā¢ (š“š¹šµ) = (š¶šŗš·) | ||
Theorem | oveq1d 7364 | Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.) |
ā¢ (š ā š“ = šµ) ā ā¢ (š ā (š“š¹š¶) = (šµš¹š¶)) | ||
Theorem | oveq2d 7365 | Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.) |
ā¢ (š ā š“ = šµ) ā ā¢ (š ā (š¶š¹š“) = (š¶š¹šµ)) | ||
Theorem | oveqd 7366 | Equality deduction for operation value. (Contributed by NM, 9-Sep-2006.) |
ā¢ (š ā š“ = šµ) ā ā¢ (š ā (š¶š“š·) = (š¶šµš·)) | ||
Theorem | oveq12d 7367 | Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
ā¢ (š ā š“ = šµ) & ā¢ (š ā š¶ = š·) ā ā¢ (š ā (š“š¹š¶) = (šµš¹š·)) | ||
Theorem | oveqan12d 7368 | Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.) |
ā¢ (š ā š“ = šµ) & ā¢ (š ā š¶ = š·) ā ā¢ ((š ā§ š) ā (š“š¹š¶) = (šµš¹š·)) | ||
Theorem | oveqan12rd 7369 | Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.) |
ā¢ (š ā š“ = šµ) & ā¢ (š ā š¶ = š·) ā ā¢ ((š ā§ š) ā (š“š¹š¶) = (šµš¹š·)) | ||
Theorem | oveq123d 7370 | Equality deduction for operation value. (Contributed by FL, 22-Dec-2008.) |
ā¢ (š ā š¹ = šŗ) & ā¢ (š ā š“ = šµ) & ā¢ (š ā š¶ = š·) ā ā¢ (š ā (š“š¹š¶) = (šµšŗš·)) | ||
Theorem | fvoveq1d 7371 | Equality deduction for nested function and operation value. (Contributed by AV, 23-Jul-2022.) |
ā¢ (š ā š“ = šµ) ā ā¢ (š ā (š¹ā(š“šš¶)) = (š¹ā(šµšš¶))) | ||
Theorem | fvoveq1 7372 | Equality theorem for nested function and operation value. Closed form of fvoveq1d 7371. (Contributed by AV, 23-Jul-2022.) |
ā¢ (š“ = šµ ā (š¹ā(š“šš¶)) = (š¹ā(šµšš¶))) | ||
Theorem | ovanraleqv 7373* | 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 7374 | 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 7375* | 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 7376* | Restricted specialization of operands, using implicit substitution. (Contributed by Mario Carneiro, 6-Dec-2014.) |
ā¢ ((š ā§ (š„ ā š“ ā§ š¦ ā šµ)) ā (š„š¹š¦) = (š„šŗš¦)) ā ā¢ ((š ā§ (š ā š“ ā§ š ā šµ)) ā (šš¹š) = (ššŗš)) | ||
Theorem | oveqdr 7377 | Equality of two operations for any two operands. Useful in proofs using *propd theorems. (Contributed by Mario Carneiro, 29-Jun-2015.) |
ā¢ (š ā š¹ = šŗ) ā ā¢ ((š ā§ š) ā (š„š¹š¦) = (š„šŗš¦)) | ||
Theorem | nfovd 7378 | Deduction version of bound-variable hypothesis builder nfov 7379. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
ā¢ (š ā ā²š„š“) & ā¢ (š ā ā²š„š¹) & ā¢ (š ā ā²š„šµ) ā ā¢ (š ā ā²š„(š“š¹šµ)) | ||
Theorem | nfov 7379 | Bound-variable hypothesis builder for operation value. (Contributed by NM, 4-May-2004.) |
ā¢ ā²š„š“ & ā¢ ā²š„š¹ & ā¢ ā²š„šµ ā ā¢ ā²š„(š“š¹šµ) | ||
Theorem | oprabidw 7380* | The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. Version of oprabid 7381 with a disjoint variable condition, which does not require ax-13 2371. (Contributed by Mario Carneiro, 20-Mar-2013.) Avoid ax-13 2371. (Revised by Gino Giotto, 26-Jan-2024.) |
ā¢ (āØāØš„, š¦ā©, š§ā© ā {āØāØš„, š¦ā©, š§ā© ā£ š} ā š) | ||
Theorem | oprabid 7381 | 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 2371. Use the weaker oprabidw 7380 when possible. (Contributed by Mario Carneiro, 20-Mar-2013.) (New usage is discouraged.) |
ā¢ (āØāØš„, š¦ā©, š§ā© ā {āØāØš„, š¦ā©, š§ā© ā£ š} ā š) | ||
Theorem | ovex 7382 | The result of an operation is a set. (Contributed by NM, 13-Mar-1995.) |
ā¢ (š“š¹šµ) ā V | ||
Theorem | ovexi 7383 | The result of an operation is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
ā¢ š“ = (šµš¹š¶) ā ā¢ š“ ā V | ||
Theorem | ovexd 7384 | The result of an operation is a set. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
ā¢ (š ā (š“š¹šµ) ā V) | ||
Theorem | ovssunirn 7385 | 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 7386 | Operation value of the empty set. (Contributed by AV, 15-May-2021.) |
ā¢ (š“ā šµ) = ā | ||
Theorem | ovprc 7387 | 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 7388 | The value of an operation when the first argument is a proper class. (Contributed by NM, 16-Jun-2004.) |
ā¢ Rel dom š¹ ā ā¢ (Ā¬ š“ ā V ā (š“š¹šµ) = ā ) | ||
Theorem | ovprc2 7389 | 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 7390 | Reverse closure for an operation value. (Contributed by Mario Carneiro, 5-May-2015.) |
ā¢ Rel dom š¹ ā ā¢ (š¶ ā (š“š¹šµ) ā (š“ ā V ā§ šµ ā V)) | ||
Theorem | csbov123 7391 | Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.) (Revised by NM, 23-Aug-2018.) |
ā¢ ā¦š“ / š„ā¦(šµš¹š¶) = (ā¦š“ / š„ā¦šµā¦š“ / š„ā¦š¹ā¦š“ / š„ā¦š¶) | ||
Theorem | csbov 7392* | Move class substitution in and out of an operation. (Contributed by NM, 23-Aug-2018.) |
ā¢ ā¦š“ / š„ā¦(šµš¹š¶) = (šµā¦š“ / š„ā¦š¹š¶) | ||
Theorem | csbov12g 7393* | Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.) |
ā¢ (š“ ā š ā ā¦š“ / š„ā¦(šµš¹š¶) = (ā¦š“ / š„ā¦šµš¹ā¦š“ / š„ā¦š¶)) | ||
Theorem | csbov1g 7394* | Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.) |
ā¢ (š“ ā š ā ā¦š“ / š„ā¦(šµš¹š¶) = (ā¦š“ / š„ā¦šµš¹š¶)) | ||
Theorem | csbov2g 7395* | Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.) |
ā¢ (š“ ā š ā ā¦š“ / š„ā¦(šµš¹š¶) = (šµš¹ā¦š“ / š„ā¦š¶)) | ||
Theorem | rspceov 7396* | A frequently used special case of rspc2ev 3590 for operation values. (Contributed by NM, 21-Mar-2007.) |
ā¢ ((š¶ ā š“ ā§ š· ā šµ ā§ š = (š¶š¹š·)) ā āš„ ā š“ āš¦ ā šµ š = (š„š¹š¦)) | ||
Theorem | elovimad 7397 | Elementhood of the image set of an operation value. (Contributed by Thierry Arnoux, 13-Mar-2017.) |
ā¢ (š ā š“ ā š¶) & ā¢ (š ā šµ ā š·) & ā¢ (š ā Fun š¹) & ā¢ (š ā (š¶ Ć š·) ā dom š¹) ā ā¢ (š ā (š“š¹šµ) ā (š¹ ā (š¶ Ć š·))) | ||
Theorem | fnbrovb 7398 | Value of a binary operation expressed as a binary relation. See also fnbrfvb 6890 for functions on Cartesian products. (Contributed by BJ, 15-Feb-2022.) |
ā¢ ((š¹ Fn (š Ć š) ā§ (š“ ā š ā§ šµ ā š)) ā ((š“š¹šµ) = š¶ ā āØš“, šµā©š¹š¶)) | ||
Theorem | fnotovb 7399 | Equivalence of operation value and ordered triple membership, analogous to fnopfvb 6891. (Contributed by NM, 17-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.) (Proof shortened by BJ, 15-Feb-2022.) |
ā¢ ((š¹ Fn (š“ Ć šµ) ā§ š¶ ā š“ ā§ š· ā šµ) ā ((š¶š¹š·) = š ā āØš¶, š·, š ā© ā š¹)) | ||
Theorem | opabbrex 7400 | A collection of ordered pairs with an extension of a binary relation is a set. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by BJ/AV, 20-Jun-2019.) (Proof shortened by OpenAI, 25-Mar-2020.) |
ā¢ ((āš„āš¦(š„š š¦ ā š) ā§ {āØš„, š¦ā© ā£ š} ā š) ā {āØš„, š¦ā© ā£ (š„š š¦ ā§ š)} ā V) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |