Type | Label | Description |
Statement |
|
Theorem | oveqi 5901 |
Equality inference for operation value. (Contributed by NM,
24-Nov-2007.)
|
โข ๐ด = ๐ต โ โข (๐ถ๐ด๐ท) = (๐ถ๐ต๐ท) |
|
Theorem | oveq123i 5902 |
Equality inference for operation value. (Contributed by FL,
11-Jul-2010.)
|
โข ๐ด = ๐ถ
& โข ๐ต = ๐ท
& โข ๐น = ๐บ โ โข (๐ด๐น๐ต) = (๐ถ๐บ๐ท) |
|
Theorem | oveq1d 5903 |
Equality deduction for operation value. (Contributed by NM,
13-Mar-1995.)
|
โข (๐ โ ๐ด = ๐ต) โ โข (๐ โ (๐ด๐น๐ถ) = (๐ต๐น๐ถ)) |
|
Theorem | oveq2d 5904 |
Equality deduction for operation value. (Contributed by NM,
13-Mar-1995.)
|
โข (๐ โ ๐ด = ๐ต) โ โข (๐ โ (๐ถ๐น๐ด) = (๐ถ๐น๐ต)) |
|
Theorem | oveqd 5905 |
Equality deduction for operation value. (Contributed by NM,
9-Sep-2006.)
|
โข (๐ โ ๐ด = ๐ต) โ โข (๐ โ (๐ถ๐ด๐ท) = (๐ถ๐ต๐ท)) |
|
Theorem | oveq12d 5906 |
Equality deduction for operation value. (Contributed by NM,
13-Mar-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|
โข (๐ โ ๐ด = ๐ต)
& โข (๐ โ ๐ถ = ๐ท) โ โข (๐ โ (๐ด๐น๐ถ) = (๐ต๐น๐ท)) |
|
Theorem | oveqan12d 5907 |
Equality deduction for operation value. (Contributed by NM,
10-Aug-1995.)
|
โข (๐ โ ๐ด = ๐ต)
& โข (๐ โ ๐ถ = ๐ท) โ โข ((๐ โง ๐) โ (๐ด๐น๐ถ) = (๐ต๐น๐ท)) |
|
Theorem | oveqan12rd 5908 |
Equality deduction for operation value. (Contributed by NM,
10-Aug-1995.)
|
โข (๐ โ ๐ด = ๐ต)
& โข (๐ โ ๐ถ = ๐ท) โ โข ((๐ โง ๐) โ (๐ด๐น๐ถ) = (๐ต๐น๐ท)) |
|
Theorem | oveq123d 5909 |
Equality deduction for operation value. (Contributed by FL,
22-Dec-2008.)
|
โข (๐ โ ๐น = ๐บ)
& โข (๐ โ ๐ด = ๐ต)
& โข (๐ โ ๐ถ = ๐ท) โ โข (๐ โ (๐ด๐น๐ถ) = (๐ต๐บ๐ท)) |
|
Theorem | fvoveq1d 5910 |
Equality deduction for nested function and operation value.
(Contributed by AV, 23-Jul-2022.)
|
โข (๐ โ ๐ด = ๐ต) โ โข (๐ โ (๐นโ(๐ด๐๐ถ)) = (๐นโ(๐ต๐๐ถ))) |
|
Theorem | fvoveq1 5911 |
Equality theorem for nested function and operation value. Closed form of
fvoveq1d 5910. (Contributed by AV, 23-Jul-2022.)
|
โข (๐ด = ๐ต โ (๐นโ(๐ด๐๐ถ)) = (๐นโ(๐ต๐๐ถ))) |
|
Theorem | ovanraleqv 5912* |
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 5913 |
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 5914* |
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 5915* |
Restricted specialization of operands, using implicit substitution.
(Contributed by Mario Carneiro, 6-Dec-2014.)
|
โข ((๐ โง (๐ฅ โ ๐ด โง ๐ฆ โ ๐ต)) โ (๐ฅ๐น๐ฆ) = (๐ฅ๐บ๐ฆ)) โ โข ((๐ โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ (๐๐น๐) = (๐๐บ๐)) |
|
Theorem | oveqdr 5916 |
Equality of two operations for any two operands. Useful in proofs using
*propd theorems. (Contributed by Mario Carneiro, 29-Jun-2015.)
|
โข (๐ โ ๐น = ๐บ) โ โข ((๐ โง ๐) โ (๐ฅ๐น๐ฆ) = (๐ฅ๐บ๐ฆ)) |
|
Theorem | nfovd 5917 |
Deduction version of bound-variable hypothesis builder nfov 5918.
(Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon,
22-Oct-2011.)
|
โข (๐ โ โฒ๐ฅ๐ด)
& โข (๐ โ โฒ๐ฅ๐น)
& โข (๐ โ โฒ๐ฅ๐ต) โ โข (๐ โ โฒ๐ฅ(๐ด๐น๐ต)) |
|
Theorem | nfov 5918 |
Bound-variable hypothesis builder for operation value. (Contributed by
NM, 4-May-2004.)
|
โข โฒ๐ฅ๐ด
& โข โฒ๐ฅ๐น
& โข โฒ๐ฅ๐ต โ โข โฒ๐ฅ(๐ด๐น๐ต) |
|
Theorem | oprabidlem 5919* |
Slight elaboration of exdistrfor 1810. A lemma for oprabid 5920.
(Contributed by Jim Kingdon, 15-Jan-2019.)
|
โข (โ๐ฅโ๐ฆ(๐ฅ = ๐ง โง ๐) โ โ๐ฅ(๐ฅ = ๐ง โง โ๐ฆ๐)) |
|
Theorem | oprabid 5920 |
The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61.
Although this theorem would be useful with a distinct variable condition
between ๐ฅ, ๐ฆ, and ๐ง, we use ax-bndl 1519 to eliminate that
constraint. (Contributed by Mario Carneiro, 20-Mar-2013.)
|
โข (โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โ {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} โ ๐) |
|
Theorem | fnovex 5921 |
The result of an operation is a set. (Contributed by Jim Kingdon,
15-Jan-2019.)
|
โข ((๐น Fn (๐ถ ร ๐ท) โง ๐ด โ ๐ถ โง ๐ต โ ๐ท) โ (๐ด๐น๐ต) โ V) |
|
Theorem | ovexg 5922 |
Evaluating a set operation at two sets gives a set. (Contributed by Jim
Kingdon, 19-Aug-2021.)
|
โข ((๐ด โ ๐ โง ๐น โ ๐ โง ๐ต โ ๐) โ (๐ด๐น๐ต) โ V) |
|
Theorem | ovprc 5923 |
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 5924 |
The value of an operation when the first argument is a proper class.
(Contributed by NM, 16-Jun-2004.)
|
โข Rel dom ๐น โ โข (ยฌ ๐ด โ V โ (๐ด๐น๐ต) = โ
) |
|
Theorem | ovprc2 5925 |
The value of an operation when the second argument is a proper class.
(Contributed by Mario Carneiro, 26-Apr-2015.)
|
โข Rel dom ๐น โ โข (ยฌ ๐ต โ V โ (๐ด๐น๐ต) = โ
) |
|
Theorem | csbov123g 5926 |
Move class substitution in and out of an operation. (Contributed by NM,
12-Nov-2005.) (Proof shortened by Mario Carneiro, 5-Dec-2016.)
|
โข (๐ด โ ๐ท โ โฆ๐ด / ๐ฅโฆ(๐ต๐น๐ถ) = (โฆ๐ด / ๐ฅโฆ๐ตโฆ๐ด / ๐ฅโฆ๐นโฆ๐ด / ๐ฅโฆ๐ถ)) |
|
Theorem | csbov12g 5927* |
Move class substitution in and out of an operation. (Contributed by NM,
12-Nov-2005.)
|
โข (๐ด โ ๐ โ โฆ๐ด / ๐ฅโฆ(๐ต๐น๐ถ) = (โฆ๐ด / ๐ฅโฆ๐ต๐นโฆ๐ด / ๐ฅโฆ๐ถ)) |
|
Theorem | csbov1g 5928* |
Move class substitution in and out of an operation. (Contributed by NM,
12-Nov-2005.)
|
โข (๐ด โ ๐ โ โฆ๐ด / ๐ฅโฆ(๐ต๐น๐ถ) = (โฆ๐ด / ๐ฅโฆ๐ต๐น๐ถ)) |
|
Theorem | csbov2g 5929* |
Move class substitution in and out of an operation. (Contributed by NM,
12-Nov-2005.)
|
โข (๐ด โ ๐ โ โฆ๐ด / ๐ฅโฆ(๐ต๐น๐ถ) = (๐ต๐นโฆ๐ด / ๐ฅโฆ๐ถ)) |
|
Theorem | rspceov 5930* |
A frequently used special case of rspc2ev 2868 for operation values.
(Contributed by NM, 21-Mar-2007.)
|
โข ((๐ถ โ ๐ด โง ๐ท โ ๐ต โง ๐ = (๐ถ๐น๐ท)) โ โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ = (๐ฅ๐น๐ฆ)) |
|
Theorem | fnotovb 5931 |
Equivalence of operation value and ordered triple membership, analogous to
fnopfvb 5570. (Contributed by NM, 17-Dec-2008.) (Revised
by Mario
Carneiro, 28-Apr-2015.)
|
โข ((๐น Fn (๐ด ร ๐ต) โง ๐ถ โ ๐ด โง ๐ท โ ๐ต) โ ((๐ถ๐น๐ท) = ๐
โ โจ๐ถ, ๐ท, ๐
โฉ โ ๐น)) |
|
Theorem | opabbrex 5932* |
A collection of ordered pairs with an extension of a binary relation is
a set. (Contributed by Alexander van der Vekens, 1-Nov-2017.)
|
โข ((๐ โ V โง ๐ธ โ V) โ (๐(๐๐๐ธ)๐ โ ๐)) & โข ((๐ โ V โง ๐ธ โ V) โ {โจ๐, ๐โฉ โฃ ๐} โ V) โ โข ((๐ โ V โง ๐ธ โ V) โ {โจ๐, ๐โฉ โฃ (๐(๐๐๐ธ)๐ โง ๐)} โ V) |
|
Theorem | 0neqopab 5933 |
The empty set is never an element in an ordered-pair class abstraction.
(Contributed by Alexander van der Vekens, 5-Nov-2017.)
|
โข ยฌ โ
โ {โจ๐ฅ, ๐ฆโฉ โฃ ๐} |
|
Theorem | brabvv 5934* |
If two classes are in a relationship given by an ordered-pair class
abstraction, the classes are sets. (Contributed by Jim Kingdon,
16-Jan-2019.)
|
โข (๐{โจ๐ฅ, ๐ฆโฉ โฃ ๐}๐ โ (๐ โ V โง ๐ โ V)) |
|
Theorem | dfoprab2 5935* |
Class abstraction for operations in terms of class abstraction of
ordered pairs. (Contributed by NM, 12-Mar-1995.)
|
โข {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} = {โจ๐ค, ๐งโฉ โฃ โ๐ฅโ๐ฆ(๐ค = โจ๐ฅ, ๐ฆโฉ โง ๐)} |
|
Theorem | reloprab 5936* |
An operation class abstraction is a relation. (Contributed by NM,
16-Jun-2004.)
|
โข Rel {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} |
|
Theorem | nfoprab1 5937 |
The abstraction variables in an operation class abstraction are not
free. (Contributed by NM, 25-Apr-1995.) (Revised by David Abernethy,
19-Jun-2012.)
|
โข โฒ๐ฅ{โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} |
|
Theorem | nfoprab2 5938 |
The abstraction variables in an operation class abstraction are not
free. (Contributed by NM, 25-Apr-1995.) (Revised by David Abernethy,
30-Jul-2012.)
|
โข โฒ๐ฆ{โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} |
|
Theorem | nfoprab3 5939 |
The abstraction variables in an operation class abstraction are not
free. (Contributed by NM, 22-Aug-2013.)
|
โข โฒ๐ง{โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} |
|
Theorem | nfoprab 5940* |
Bound-variable hypothesis builder for an operation class abstraction.
(Contributed by NM, 22-Aug-2013.)
|
โข โฒ๐ค๐ โ โข โฒ๐ค{โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} |
|
Theorem | oprabbid 5941* |
Equivalent wff's yield equal operation class abstractions (deduction
form). (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro,
24-Jun-2014.)
|
โข โฒ๐ฅ๐
& โข โฒ๐ฆ๐
& โข โฒ๐ง๐
& โข (๐ โ (๐ โ ๐)) โ โข (๐ โ {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} = {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐}) |
|
Theorem | oprabbidv 5942* |
Equivalent wff's yield equal operation class abstractions (deduction
form). (Contributed by NM, 21-Feb-2004.)
|
โข (๐ โ (๐ โ ๐)) โ โข (๐ โ {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} = {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐}) |
|
Theorem | oprabbii 5943* |
Equivalent wff's yield equal operation class abstractions. (Contributed
by NM, 28-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)
|
โข (๐ โ ๐) โ โข {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} = {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} |
|
Theorem | ssoprab2 5944 |
Equivalence of ordered pair abstraction subclass and implication.
Compare ssopab2 4287. (Contributed by FL, 6-Nov-2013.) (Proof
shortened
by Mario Carneiro, 11-Dec-2016.)
|
โข (โ๐ฅโ๐ฆโ๐ง(๐ โ ๐) โ {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} โ {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐}) |
|
Theorem | ssoprab2b 5945 |
Equivalence of ordered pair abstraction subclass and implication. Compare
ssopab2b 4288. (Contributed by FL, 6-Nov-2013.) (Proof
shortened by Mario
Carneiro, 11-Dec-2016.)
|
โข ({โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} โ {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} โ โ๐ฅโ๐ฆโ๐ง(๐ โ ๐)) |
|
Theorem | eqoprab2b 5946 |
Equivalence of ordered pair abstraction subclass and biconditional.
Compare eqopab2b 4291. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
โข ({โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} = {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} โ โ๐ฅโ๐ฆโ๐ง(๐ โ ๐)) |
|
Theorem | mpoeq123 5947* |
An equality theorem for the maps-to notation. (Contributed by Mario
Carneiro, 16-Dec-2013.) (Revised by Mario Carneiro, 19-Mar-2015.)
|
โข ((๐ด = ๐ท โง โ๐ฅ โ ๐ด (๐ต = ๐ธ โง โ๐ฆ โ ๐ต ๐ถ = ๐น)) โ (๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ถ) = (๐ฅ โ ๐ท, ๐ฆ โ ๐ธ โฆ ๐น)) |
|
Theorem | mpoeq12 5948* |
An equality theorem for the maps-to notation. (Contributed by Mario
Carneiro, 16-Dec-2013.)
|
โข ((๐ด = ๐ถ โง ๐ต = ๐ท) โ (๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ธ) = (๐ฅ โ ๐ถ, ๐ฆ โ ๐ท โฆ ๐ธ)) |
|
Theorem | mpoeq123dva 5949* |
An equality deduction for the maps-to notation. (Contributed by Mario
Carneiro, 26-Jan-2017.)
|
โข (๐ โ ๐ด = ๐ท)
& โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต = ๐ธ)
& โข ((๐ โง (๐ฅ โ ๐ด โง ๐ฆ โ ๐ต)) โ ๐ถ = ๐น) โ โข (๐ โ (๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ถ) = (๐ฅ โ ๐ท, ๐ฆ โ ๐ธ โฆ ๐น)) |
|
Theorem | mpoeq123dv 5950* |
An equality deduction for the maps-to notation. (Contributed by NM,
12-Sep-2011.)
|
โข (๐ โ ๐ด = ๐ท)
& โข (๐ โ ๐ต = ๐ธ)
& โข (๐ โ ๐ถ = ๐น) โ โข (๐ โ (๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ถ) = (๐ฅ โ ๐ท, ๐ฆ โ ๐ธ โฆ ๐น)) |
|
Theorem | mpoeq123i 5951 |
An equality inference for the maps-to notation. (Contributed by NM,
15-Jul-2013.)
|
โข ๐ด = ๐ท
& โข ๐ต = ๐ธ
& โข ๐ถ = ๐น โ โข (๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ถ) = (๐ฅ โ ๐ท, ๐ฆ โ ๐ธ โฆ ๐น) |
|
Theorem | mpoeq3dva 5952* |
Slightly more general equality inference for the maps-to notation.
(Contributed by NM, 17-Oct-2013.)
|
โข ((๐ โง ๐ฅ โ ๐ด โง ๐ฆ โ ๐ต) โ ๐ถ = ๐ท) โ โข (๐ โ (๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ถ) = (๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ท)) |
|
Theorem | mpoeq3ia 5953 |
An equality inference for the maps-to notation. (Contributed by Mario
Carneiro, 16-Dec-2013.)
|
โข ((๐ฅ โ ๐ด โง ๐ฆ โ ๐ต) โ ๐ถ = ๐ท) โ โข (๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ถ) = (๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ท) |
|
Theorem | mpoeq3dv 5954* |
An equality deduction for the maps-to notation restricted to the value
of the operation. (Contributed by SO, 16-Jul-2018.)
|
โข (๐ โ ๐ถ = ๐ท) โ โข (๐ โ (๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ถ) = (๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ท)) |
|
Theorem | nfmpo1 5955 |
Bound-variable hypothesis builder for an operation in maps-to notation.
(Contributed by NM, 27-Aug-2013.)
|
โข โฒ๐ฅ(๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ถ) |
|
Theorem | nfmpo2 5956 |
Bound-variable hypothesis builder for an operation in maps-to notation.
(Contributed by NM, 27-Aug-2013.)
|
โข โฒ๐ฆ(๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ถ) |
|
Theorem | nfmpo 5957* |
Bound-variable hypothesis builder for the maps-to notation.
(Contributed by NM, 20-Feb-2013.)
|
โข โฒ๐ง๐ด
& โข โฒ๐ง๐ต
& โข โฒ๐ง๐ถ โ โข โฒ๐ง(๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ถ) |
|
Theorem | mpo0 5958 |
A mapping operation with empty domain. (Contributed by Stefan O'Rear,
29-Jan-2015.) (Revised by Mario Carneiro, 15-May-2015.)
|
โข (๐ฅ โ โ
, ๐ฆ โ ๐ต โฆ ๐ถ) = โ
|
|
Theorem | oprab4 5959* |
Two ways to state the domain of an operation. (Contributed by FL,
24-Jan-2010.)
|
โข {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ (โจ๐ฅ, ๐ฆโฉ โ (๐ด ร ๐ต) โง ๐)} = {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ((๐ฅ โ ๐ด โง ๐ฆ โ ๐ต) โง ๐)} |
|
Theorem | cbvoprab1 5960* |
Rule used to change first bound variable in an operation abstraction,
using implicit substitution. (Contributed by NM, 20-Dec-2008.)
(Revised by Mario Carneiro, 5-Dec-2016.)
|
โข โฒ๐ค๐
& โข โฒ๐ฅ๐
& โข (๐ฅ = ๐ค โ (๐ โ ๐)) โ โข {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} = {โจโจ๐ค, ๐ฆโฉ, ๐งโฉ โฃ ๐} |
|
Theorem | cbvoprab2 5961* |
Change the second bound variable in an operation abstraction.
(Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro,
11-Dec-2016.)
|
โข โฒ๐ค๐
& โข โฒ๐ฆ๐
& โข (๐ฆ = ๐ค โ (๐ โ ๐)) โ โข {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} = {โจโจ๐ฅ, ๐คโฉ, ๐งโฉ โฃ ๐} |
|
Theorem | cbvoprab12 5962* |
Rule used to change first two bound variables in an operation
abstraction, using implicit substitution. (Contributed by NM,
21-Feb-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|
โข โฒ๐ค๐
& โข โฒ๐ฃ๐
& โข โฒ๐ฅ๐
& โข โฒ๐ฆ๐
& โข ((๐ฅ = ๐ค โง ๐ฆ = ๐ฃ) โ (๐ โ ๐)) โ โข {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} = {โจโจ๐ค, ๐ฃโฉ, ๐งโฉ โฃ ๐} |
|
Theorem | cbvoprab12v 5963* |
Rule used to change first two bound variables in an operation
abstraction, using implicit substitution. (Contributed by NM,
8-Oct-2004.)
|
โข ((๐ฅ = ๐ค โง ๐ฆ = ๐ฃ) โ (๐ โ ๐)) โ โข {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} = {โจโจ๐ค, ๐ฃโฉ, ๐งโฉ โฃ ๐} |
|
Theorem | cbvoprab3 5964* |
Rule used to change the third bound variable in an operation
abstraction, using implicit substitution. (Contributed by NM,
22-Aug-2013.)
|
โข โฒ๐ค๐
& โข โฒ๐ง๐
& โข (๐ง = ๐ค โ (๐ โ ๐)) โ โข {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} = {โจโจ๐ฅ, ๐ฆโฉ, ๐คโฉ โฃ ๐} |
|
Theorem | cbvoprab3v 5965* |
Rule used to change the third bound variable in an operation
abstraction, using implicit substitution. (Contributed by NM,
8-Oct-2004.) (Revised by David Abernethy, 19-Jun-2012.)
|
โข (๐ง = ๐ค โ (๐ โ ๐)) โ โข {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} = {โจโจ๐ฅ, ๐ฆโฉ, ๐คโฉ โฃ ๐} |
|
Theorem | cbvmpox 5966* |
Rule to change the bound variable in a maps-to function, using implicit
substitution. This version of cbvmpo 5967 allows ๐ต to be a function of
๐ฅ. (Contributed by NM, 29-Dec-2014.)
|
โข โฒ๐ง๐ต
& โข โฒ๐ฅ๐ท
& โข โฒ๐ง๐ถ
& โข โฒ๐ค๐ถ
& โข โฒ๐ฅ๐ธ
& โข โฒ๐ฆ๐ธ
& โข (๐ฅ = ๐ง โ ๐ต = ๐ท)
& โข ((๐ฅ = ๐ง โง ๐ฆ = ๐ค) โ ๐ถ = ๐ธ) โ โข (๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ถ) = (๐ง โ ๐ด, ๐ค โ ๐ท โฆ ๐ธ) |
|
Theorem | cbvmpo 5967* |
Rule to change the bound variable in a maps-to function, using implicit
substitution. (Contributed by NM, 17-Dec-2013.)
|
โข โฒ๐ง๐ถ
& โข โฒ๐ค๐ถ
& โข โฒ๐ฅ๐ท
& โข โฒ๐ฆ๐ท
& โข ((๐ฅ = ๐ง โง ๐ฆ = ๐ค) โ ๐ถ = ๐ท) โ โข (๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ถ) = (๐ง โ ๐ด, ๐ค โ ๐ต โฆ ๐ท) |
|
Theorem | cbvmpov 5968* |
Rule to change the bound variable in a maps-to function, using implicit
substitution. With a longer proof analogous to cbvmpt 4110, some distinct
variable requirements could be eliminated. (Contributed by NM,
11-Jun-2013.)
|
โข (๐ฅ = ๐ง โ ๐ถ = ๐ธ)
& โข (๐ฆ = ๐ค โ ๐ธ = ๐ท) โ โข (๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ถ) = (๐ง โ ๐ด, ๐ค โ ๐ต โฆ ๐ท) |
|
Theorem | dmoprab 5969* |
The domain of an operation class abstraction. (Contributed by NM,
17-Mar-1995.) (Revised by David Abernethy, 19-Jun-2012.)
|
โข dom {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} = {โจ๐ฅ, ๐ฆโฉ โฃ โ๐ง๐} |
|
Theorem | dmoprabss 5970* |
The domain of an operation class abstraction. (Contributed by NM,
24-Aug-1995.)
|
โข dom {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ((๐ฅ โ ๐ด โง ๐ฆ โ ๐ต) โง ๐)} โ (๐ด ร ๐ต) |
|
Theorem | rnoprab 5971* |
The range of an operation class abstraction. (Contributed by NM,
30-Aug-2004.) (Revised by David Abernethy, 19-Apr-2013.)
|
โข ran {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} = {๐ง โฃ โ๐ฅโ๐ฆ๐} |
|
Theorem | rnoprab2 5972* |
The range of a restricted operation class abstraction. (Contributed by
Scott Fenton, 21-Mar-2012.)
|
โข ran {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ((๐ฅ โ ๐ด โง ๐ฆ โ ๐ต) โง ๐)} = {๐ง โฃ โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐} |
|
Theorem | reldmoprab 5973* |
The domain of an operation class abstraction is a relation.
(Contributed by NM, 17-Mar-1995.)
|
โข Rel dom {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} |
|
Theorem | oprabss 5974* |
Structure of an operation class abstraction. (Contributed by NM,
28-Nov-2006.)
|
โข {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} โ ((V ร V) ร
V) |
|
Theorem | eloprabga 5975* |
The law of concretion for operation class abstraction. Compare
elopab 4270. (Contributed by NM, 14-Sep-1999.)
(Unnecessary distinct
variable restrictions were removed by David Abernethy, 19-Jun-2012.)
(Revised by Mario Carneiro, 19-Dec-2013.)
|
โข ((๐ฅ = ๐ด โง ๐ฆ = ๐ต โง ๐ง = ๐ถ) โ (๐ โ ๐)) โ โข ((๐ด โ ๐ โง ๐ต โ ๐ โง ๐ถ โ ๐) โ (โจโจ๐ด, ๐ตโฉ, ๐ถโฉ โ {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} โ ๐)) |
|
Theorem | eloprabg 5976* |
The law of concretion for operation class abstraction. Compare
elopab 4270. (Contributed by NM, 14-Sep-1999.) (Revised
by David
Abernethy, 19-Jun-2012.)
|
โข (๐ฅ = ๐ด โ (๐ โ ๐)) & โข (๐ฆ = ๐ต โ (๐ โ ๐)) & โข (๐ง = ๐ถ โ (๐ โ ๐)) โ โข ((๐ด โ ๐ โง ๐ต โ ๐ โง ๐ถ โ ๐) โ (โจโจ๐ด, ๐ตโฉ, ๐ถโฉ โ {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} โ ๐)) |
|
Theorem | ssoprab2i 5977* |
Inference of operation class abstraction subclass from implication.
(Contributed by NM, 11-Nov-1995.) (Revised by David Abernethy,
19-Jun-2012.)
|
โข (๐ โ ๐) โ โข {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} โ {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} |
|
Theorem | mpov 5978* |
Operation with universal domain in maps-to notation. (Contributed by
NM, 16-Aug-2013.)
|
โข (๐ฅ โ V, ๐ฆ โ V โฆ ๐ถ) = {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐ง = ๐ถ} |
|
Theorem | mpomptx 5979* |
Express a two-argument function as a one-argument function, or
vice-versa. In this version ๐ต(๐ฅ) is not assumed to be constant
w.r.t ๐ฅ. (Contributed by Mario Carneiro,
29-Dec-2014.)
|
โข (๐ง = โจ๐ฅ, ๐ฆโฉ โ ๐ถ = ๐ท) โ โข (๐ง โ โช
๐ฅ โ ๐ด ({๐ฅ} ร ๐ต) โฆ ๐ถ) = (๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ท) |
|
Theorem | mpompt 5980* |
Express a two-argument function as a one-argument function, or
vice-versa. (Contributed by Mario Carneiro, 17-Dec-2013.) (Revised by
Mario Carneiro, 29-Dec-2014.)
|
โข (๐ง = โจ๐ฅ, ๐ฆโฉ โ ๐ถ = ๐ท) โ โข (๐ง โ (๐ด ร ๐ต) โฆ ๐ถ) = (๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ท) |
|
Theorem | mpodifsnif 5981 |
A mapping with two arguments with the first argument from a difference set
with a singleton and a conditional as result. (Contributed by AV,
13-Feb-2019.)
|
โข (๐ โ (๐ด โ {๐}), ๐ โ ๐ต โฆ if(๐ = ๐, ๐ถ, ๐ท)) = (๐ โ (๐ด โ {๐}), ๐ โ ๐ต โฆ ๐ท) |
|
Theorem | mposnif 5982 |
A mapping with two arguments with the first argument from a singleton and
a conditional as result. (Contributed by AV, 14-Feb-2019.)
|
โข (๐ โ {๐}, ๐ โ ๐ต โฆ if(๐ = ๐, ๐ถ, ๐ท)) = (๐ โ {๐}, ๐ โ ๐ต โฆ ๐ถ) |
|
Theorem | fconstmpo 5983* |
Representation of a constant operation using the mapping operation.
(Contributed by SO, 11-Jul-2018.)
|
โข ((๐ด ร ๐ต) ร {๐ถ}) = (๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ถ) |
|
Theorem | resoprab 5984* |
Restriction of an operation class abstraction. (Contributed by NM,
10-Feb-2007.)
|
โข ({โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} โพ (๐ด ร ๐ต)) = {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ((๐ฅ โ ๐ด โง ๐ฆ โ ๐ต) โง ๐)} |
|
Theorem | resoprab2 5985* |
Restriction of an operator abstraction. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
โข ((๐ถ โ ๐ด โง ๐ท โ ๐ต) โ ({โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ((๐ฅ โ ๐ด โง ๐ฆ โ ๐ต) โง ๐)} โพ (๐ถ ร ๐ท)) = {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ((๐ฅ โ ๐ถ โง ๐ฆ โ ๐ท) โง ๐)}) |
|
Theorem | resmpo 5986* |
Restriction of the mapping operation. (Contributed by Mario Carneiro,
17-Dec-2013.)
|
โข ((๐ถ โ ๐ด โง ๐ท โ ๐ต) โ ((๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ธ) โพ (๐ถ ร ๐ท)) = (๐ฅ โ ๐ถ, ๐ฆ โ ๐ท โฆ ๐ธ)) |
|
Theorem | funoprabg 5987* |
"At most one" is a sufficient condition for an operation class
abstraction to be a function. (Contributed by NM, 28-Aug-2007.)
|
โข (โ๐ฅโ๐ฆโ*๐ง๐ โ Fun {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐}) |
|
Theorem | funoprab 5988* |
"At most one" is a sufficient condition for an operation class
abstraction to be a function. (Contributed by NM, 17-Mar-1995.)
|
โข โ*๐ง๐ โ โข Fun {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} |
|
Theorem | fnoprabg 5989* |
Functionality and domain of an operation class abstraction.
(Contributed by NM, 28-Aug-2007.)
|
โข (โ๐ฅโ๐ฆ(๐ โ โ!๐ง๐) โ {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ (๐ โง ๐)} Fn {โจ๐ฅ, ๐ฆโฉ โฃ ๐}) |
|
Theorem | mpofun 5990* |
The maps-to notation for an operation is always a function.
(Contributed by Scott Fenton, 21-Mar-2012.)
|
โข ๐น = (๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ถ) โ โข Fun ๐น |
|
Theorem | fnoprab 5991* |
Functionality and domain of an operation class abstraction.
(Contributed by NM, 15-May-1995.)
|
โข (๐ โ โ!๐ง๐) โ โข {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ (๐ โง ๐)} Fn {โจ๐ฅ, ๐ฆโฉ โฃ ๐} |
|
Theorem | ffnov 5992* |
An operation maps to a class to which all values belong. (Contributed
by NM, 7-Feb-2004.)
|
โข (๐น:(๐ด ร ๐ต)โถ๐ถ โ (๐น Fn (๐ด ร ๐ต) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต (๐ฅ๐น๐ฆ) โ ๐ถ)) |
|
Theorem | fovcl 5993 |
Closure law for an operation. (Contributed by NM, 19-Apr-2007.)
|
โข ๐น:(๐
ร ๐)โถ๐ถ โ โข ((๐ด โ ๐
โง ๐ต โ ๐) โ (๐ด๐น๐ต) โ ๐ถ) |
|
Theorem | eqfnov 5994* |
Equality of two operations is determined by their values. (Contributed
by NM, 1-Sep-2005.)
|
โข ((๐น Fn (๐ด ร ๐ต) โง ๐บ Fn (๐ถ ร ๐ท)) โ (๐น = ๐บ โ ((๐ด ร ๐ต) = (๐ถ ร ๐ท) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต (๐ฅ๐น๐ฆ) = (๐ฅ๐บ๐ฆ)))) |
|
Theorem | eqfnov2 5995* |
Two operators with the same domain are equal iff their values at each
point in the domain are equal. (Contributed by Jeff Madsen,
7-Jun-2010.)
|
โข ((๐น Fn (๐ด ร ๐ต) โง ๐บ Fn (๐ด ร ๐ต)) โ (๐น = ๐บ โ โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต (๐ฅ๐น๐ฆ) = (๐ฅ๐บ๐ฆ))) |
|
Theorem | fnovim 5996* |
Representation of a function in terms of its values. (Contributed by
Jim Kingdon, 16-Jan-2019.)
|
โข (๐น Fn (๐ด ร ๐ต) โ ๐น = (๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ (๐ฅ๐น๐ฆ))) |
|
Theorem | mpo2eqb 5997* |
Bidirectional equality theorem for a mapping abstraction. Equivalent to
eqfnov2 5995. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
โข (โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ถ โ ๐ โ ((๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ถ) = (๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ท) โ โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ถ = ๐ท)) |
|
Theorem | rnmpo 5998* |
The range of an operation given by the maps-to notation. (Contributed
by FL, 20-Jun-2011.)
|
โข ๐น = (๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ถ) โ โข ran ๐น = {๐ง โฃ โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ง = ๐ถ} |
|
Theorem | reldmmpo 5999* |
The domain of an operation defined by maps-to notation is a relation.
(Contributed by Stefan O'Rear, 27-Nov-2014.)
|
โข ๐น = (๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ถ) โ โข Rel dom ๐น |
|
Theorem | elrnmpog 6000* |
Membership in the range of an operation class abstraction. (Contributed
by NM, 27-Aug-2007.) (Revised by Mario Carneiro, 31-Aug-2015.)
|
โข ๐น = (๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ถ) โ โข (๐ท โ ๐ โ (๐ท โ ran ๐น โ โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ท = ๐ถ)) |