Home New Foundations ExplorerTheorem List (p. 56 of 64) < Previous  Next > Browser slow? Try the Unicode version. Mirrors  >  Metamath Home Page  >  NFE Home Page  >  Theorem List Contents       This page: Page List

Theorem List for New Foundations Explorer - 5501-5600   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremopbr1st 5501 Binary relationship of an ordered pair over . (Contributed by SF, 6-Feb-2015.)

Theoremopbr2nd 5502 Binary relationship of an ordered pair over . (Contributed by SF, 6-Feb-2015.)

Theoremdfid4 5503 Alternate definition of the identity relationship. (Contributed by SF, 11-Feb-2015.)
S S

Theoremidex 5504 The identity relationship is a set. (Contributed by SF, 11-Feb-2015.)

Theorem1stfo 5505 is a mapping from the universe onto the universe. (Contributed by SF, 12-Feb-2015.) (Revised by Scott Fenton, 17-Apr-2021.)

Theorem2ndfo 5506 is a mapping from the universe onto the universe. (Contributed by SF, 12-Feb-2015.) (Revised by Scott Fenton, 17-Apr-2021.)

Theoremdfdm4 5507 Alternate definition of domain. (Contributed by SF, 23-Feb-2015.)

Theoremdfrn5 5508 Alternate definition of range. (Contributed by SF, 23-Feb-2015.)

Theorembrswap 5509* Binary relationship of Swap . (Contributed by SF, 23-Feb-2015.)
Swap

Theoremcnvswap 5510 The converse of Swap is Swap . (Contributed by SF, 23-Feb-2015.)
Swap Swap

Theoremswapf1o 5511 Swap is a bijection over the universe. (Contributed by SF, 23-Feb-2015.) (Revised by Scott Fenton, 17-Apr-2021.)
Swap

Theoremswapres 5512 Bijection law for restrictions of Swap . (Contributed by SF, 23-Feb-2015.) (Modified by Scott Fenton, 17-Apr-2021.)
Swap

Theoremxpnedisj 5513 Cross products with non-equal singletons are disjoint. (Contributed by SF, 23-Feb-2015.)

Theoremopfv1st 5514 The value of the function on an ordered pair. (Contributed by SF, 23-Feb-2015.)

Theoremopfv2nd 5515 The value of the function on an ordered pair. (Contributed by SF, 23-Feb-2015.)

Theorem1st2nd2 5516 Reconstruction of a member of a cross product in terms of its ordered pair components. (Contributed by SF, 20-Oct-2013.)

Theoremfununiq 5517 Implicational form of part of the definition of a function. (Contributed by SF, 24-Feb-2015.)

Theoremcnvsi 5518 Calculate the converse of a singleton image. (Contributed by SF, 26-Feb-2015.)
SI SI

Theoremdmsi 5519 Calculate the domain of a singleton image. Theorem X.4.29.I of [Rosser] p. 301. (Contributed by SF, 26-Feb-2015.)
SI 1

Theoremfunsi 5520 The singleton image of a function is a function. (Contributed by SF, 26-Feb-2015.)
SI

Theoremrnsi 5521 Calculate the range of a singleton image. Theorem X.4.29.II of [Rosser] p. 302. (Contributed by SF, 26-Feb-2015.)
SI 1

Theoremop1std 5522 Extract the first member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.)

Theoremop2ndd 5523 Extract the second member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.)

Theoremdmep 5524 The domain of the epsilon relationship. (Contributed by Scott Fenton, 20-Apr-2021.)

2.3.8  Operations

Syntaxco 5525 Extend class notation to include the value of an operation 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.

Definitiondf-ov 5526 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. This definition is well-defined, although not very meaningful, when classes and/or are proper classes (i.e. are not sets). On the other hand, we often find uses for this definition when is a proper class. is normally equal to a class of nested ordered pairs of the form defined by df-oprab 5528. (Contributed by SF, 5-Jan-2015.)

Syntaxcoprab 5527 Extend class notation to include class abstraction (class builder) of nested ordered pairs.

Definitiondf-oprab 5528* 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 5526 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 the most common operation class builder is given by ov2 in set.mm. (Contributed by SF, 5-Jan-2015.)

Theoremoveq 5529 Equality theorem for operation value. (Contributed by set.mm contributors, 28-Feb-1995.)

Theoremoveq1 5530 Equality theorem for operation value. (Contributed by set.mm contributors, 28-Feb-1995.)

Theoremoveq2 5531 Equality theorem for operation value. (Contributed by set.mm contributors, 28-Feb-1995.)

Theoremoveq12 5532 Equality theorem for operation value. (Contributed by set.mm contributors, 16-Jul-1995.)

Theoremoveq1i 5533 Equality inference for operation value. (Contributed by set.mm contributors, 28-Feb-1995.)

Theoremoveq2i 5534 Equality inference for operation value. (Contributed by set.mm contributors, 28-Feb-1995.)

Theoremoveq12i 5535 Equality inference for operation value. (The proof was shortened by Andrew Salmon, 22-Oct-2011.) (Contributed by set.mm contributors, 28-Feb-1995.) (Revised by set.mm contributors, 22-Oct-2011.)

Theoremoveqi 5536 Equality inference for operation value. (Contributed by set.mm contributors, 24-Nov-2007.)

Theoremoveq1d 5537 Equality deduction for operation value. (Contributed by set.mm contributors, 13-Mar-1995.)

Theoremoveq2d 5538 Equality deduction for operation value. (Contributed by set.mm contributors, 13-Mar-1995.)

Theoremoveqd 5539 Equality deduction for operation value. (Contributed by set.mm contributors, 9-Sep-2006.)

Theoremoveq12d 5540 Equality deduction for operation value. (The proof was shortened by Andrew Salmon, 22-Oct-2011.) (Contributed by set.mm contributors, 13-Mar-1995.) (Revised by set.mm contributors, 22-Oct-2011.)

Theoremoveqan12d 5541 Equality deduction for operation value. (Contributed by set.mm contributors, 10-Aug-1995.)

Theoremoveqan12rd 5542 Equality deduction for operation value. (Contributed by set.mm contributors, 10-Aug-1995.)

Theoremoveq123d 5543 Equality deduction for operation value. (Contributed by FL, 22-Dec-2008.)

Theoremnfovd 5544 Deduction version of bound-variable hypothesis builder nfov 5545. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)

Theoremnfov 5545 Bound-variable hypothesis builder for operation value. (Contributed by NM, 4-May-2004.)

Theoremnfoprab1 5546 The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 25-Apr-1995.) (Revised by David Abernethy, 19-Jun-2012.)

Theoremnfoprab2 5547 The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 25-Apr-1995.) (Revised by David Abernethy, 30-Jul-2012.)

Theoremnfoprab3 5548 The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 22-Aug-2013.)

Theoremnfoprab 5549* Bound-variable hypothesis builder for an operation class abstraction. (Contributed by NM, 22-Aug-2013.)

Theoremoprabid 5550 The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 20-Mar-2013.)

Theoremovex 5551 The result of an operation is a set. (Contributed by set.mm contributors, 13-Mar-1995.)

Theoremcsbovg 5552 Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.) (Proof shortened by Mario Carneiro, 5-Dec-2016.)

Theoremcsbov12g 5553* Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.)

Theoremcsbov1g 5554* Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.)

Theoremcsbov2g 5555* Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.)

Theoremrspceov 5556* A frequently used special case of rspc2ev 2963 for operation values. (Contributed by set.mm contributors, 21-Mar-2007.)

Theoremfnopovb 5557 Equivalence of operation value and ordered triple membership, analogous to fnopfvb 5359. (Contributed by set.mm contributors, 17-Dec-2008.)

Theoremdfoprab2 5558* Class abstraction for operations in terms of class abstraction of ordered pairs. (Contributed by set.mm contributors, 12-Mar-1995.)

Theoremhboprab1 5559* The abstraction variables in an operation class abstraction are not free. (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Contributed by set.mm contributors, 25-Apr-1995.) (Revised by set.mm contributors, 24-Jul-2012.)

Theoremhboprab2 5560* The abstraction variables in an operation class abstraction are not free. (Unnecessary distinct variable restrictions were removed by David Abernethy, 30-Jul-2012.) (Contributed by set.mm contributors, 25-Apr-1995.) (Revised by set.mm contributors, 31-Jul-2012.)

Theoremhboprab3 5561* The abstraction variables in an operation class abstraction are not free. (Contributed by set.mm contributors, 22-Aug-2013.)

Theoremhboprab 5562* Bound-variable hypothesis builder for an operation class abstraction. (Contributed by set.mm contributors, 22-Aug-2013.)

Theoremoprabbid 5563* Equivalent wff's yield equal operation class abstractions (deduction rule). (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro, 24-Jun-2014.)

Theoremoprabbidv 5564* Equivalent wff's yield equal operation class abstractions (deduction rule). (Contributed by NM, 21-Feb-2004.)

Theoremoprabbii 5565* Equivalent wff's yield equal operation class abstractions. (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Contributed by set.mm contributors, 28-May-1995.) (Revised by set.mm contributors, 24-Jul-2012.)

Theoremoprab4 5566* Two ways to state the domain of an operation. (Contributed by FL, 24-Jan-2010.)

Theoremcbvoprab1 5567* 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.)

Theoremcbvoprab2 5568* Change the second bound variable in an operation abstraction. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 11-Dec-2016.)

Theoremcbvoprab12 5569* 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.)

Theoremcbvoprab12v 5570* Rule used to change first two bound variables in an operation abstraction, using implicit substitution. (Contributed by set.mm contributors, 8-Oct-2004.)

Theoremcbvoprab3 5571* Rule used to change the third bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 22-Aug-2013.)

Theoremcbvoprab3v 5572* Rule used to change the third bound variable in an operation abstraction, using implicit substitution. (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Contributed by set.mm contributors, 8-Oct-2004.) (Revised by set.mm contributors, 24-Jul-2012.)

Theoremelimdelov 5573 Eliminate a hypothesis which is a predicate expressing membership in the result of an operator (deduction version). (Contributed by Paul Chapman, 25-Mar-2008.)

Theoremdmoprab 5574* The domain of an operation class abstraction. (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Contributed by set.mm contributors, 17-Mar-1995.) (Revised by set.mm contributors, 24-Jul-2012.)

Theoremdmoprabss 5575* The domain of an operation class abstraction. (Contributed by set.mm contributors, 24-Aug-1995.)

Theoremrnoprab 5576* The range of an operation class abstraction. (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Apr-2013.) (Contributed by set.mm contributors, 30-Aug-2004.) (Revised by set.mm contributors, 19-Apr-2013.)

Theoremrnoprab2 5577* The range of a restricted operation class abstraction. (Contributed by Scott Fenton, 21-Mar-2012.)

Theoremeloprabga 5578* The law of concretion for operation class abstraction. Compare elopab 4696. (Contributed by set.mm contributors, 17-Dec-2013.) (Revised by David Abernethy, 18-Jun-2012.) Removed unnecessary distinct variable requirements. (Revised by Mario Carneiro, 19-Dec-2013.)

Theoremeloprabg 5579* The law of concretion for operation class abstraction. Compare elopab 4696. (Contributed by set.mm contributors, 14-Sep-1999.) (Revised by David Abernethy, 19-Jun-2012.) Removed unnecessary distinct variable requirements. (Revised by set.mm contributors, 19-Dec-2013.)

Theoremssoprab2i 5580* Inference of operation class abstraction subclass from implication. (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Contributed by set.mm contributors, 11-Nov-1995.) (Revised by set.mm contributors, 24-Jul-2012.)

Theoremresoprab 5581* Restriction of an operation class abstraction. (Contributed by set.mm contributors, 10-Feb-2007.)

Theoremresoprab2 5582* Restriction of an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.)

Theoremfunoprabg 5583* "At most one" is a sufficient condition for an operation class abstraction to be a function. (Contributed by set.mm contributors, 28-Aug-2007.)

Theoremfunoprab 5584* "At most one" is a sufficient condition for an operation class abstraction to be a function. (Contributed by set.mm contributors, 17-Mar-1995.)

Theoremfnoprabg 5585* Functionality and domain of an operation class abstraction. (Contributed by set.mm contributors, 28-Aug-2007.)

Theoremfnoprab 5586* Functionality and domain of an operation class abstraction. (Contributed by set.mm contributors, 15-May-1995.)

Theoremffnov 5587* An operation maps to a class to which all values belong. (Contributed by set.mm contributors, 7-Feb-2004.)

Theoremfovcl 5588 Closure law for an operation. (Contributed by set.mm contributors, 19-Apr-2007.)

Theoremeqfnov 5589* Equality of two operations is determined by their values. (Contributed by set.mm contributors, 1-Sep-2005.)

Theoremeqfnov2 5590* 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.)

Theoremfnov 5591* Representation of an operation class abstraction in terms of its values. (Contributed by set.mm contributors, 7-Feb-2004.)

Theoremfov 5592* Representation of an operation class abstraction in terms of its values. (Contributed by set.mm contributors, 7-Feb-2004.)

Theoremovidig 5593* The value of an operation class abstraction. Compare ovidi 5594. The condition is been removed. (Contributed by Mario Carneiro, 29-Dec-2014.)

Theoremovidi 5594* The value of an operation class abstraction (weak version). (Contributed by Mario Carneiro, 29-Dec-2014.)

Theoremov 5595* The value of an operation class abstraction. (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Contributed by set.mm contributors, 16-May-1995.) (Revised by set.mm contributors, 24-Jul-2012.)

Theoremovigg 5596* The value of an operation class abstraction. Compare ovig 5597. The condition is been removed. (Contributed by FL, 24-Mar-2007.)

Theoremovig 5597* The value of an operation class abstraction (weak version). (Contributed by set.mm contributors, 14-Sep-1999.) (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Revised by Mario Carneiro, 19-Dec-2013.)

Theoremov2ag 5598* The value of an operation class abstraction. Special case. (Contributed by Mario Carneiro, 19-Dec-2013.)

Theoremov3 5599* The value of an operation class abstraction. Special case. (Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro, 29-Dec-2014.)

Theoremov6g 5600* The value of an operation class abstraction. Special case. (Contributed by set.mm contributors, 13-Nov-2006.)

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6337
 Copyright terms: Public domain < Previous  Next >