HomeHome New Foundations Explorer
Theorem List (p. 48 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 - 4701-4800   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theorembrabga 4701* The law of concretion for a binary relation. (Contributed by Mario Carneiro, 19-Dec-2013.)
   &       =>   
 
Theoremopelopab2a 4702* Ordered pair membership in an ordered pair class abstraction. (Contributed by Mario Carneiro, 19-Dec-2013.)
   =>   
 
Theoremopelopaba 4703* The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 19-Dec-2013.)
   &       &       =>   
 
Theorembraba 4704* The law of concretion for a binary relation. (Contributed by NM, 19-Dec-2013.)
   &       &       &       =>   
 
Theoremopelopabg 4705* The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by NM, 28-May-1995.) (Revised by set.mm contributors, 19-Dec-2013.)
   &       =>   
 
Theorembrabg 4706* The law of concretion for a binary relation. (Contributed by NM, 16-Aug-1999.) (Revised by set.mm contributors, 19-Dec-2013.)
   &       &       =>   
 
Theoremopelopab2 4707* Ordered pair membership in an ordered pair class abstraction. (Contributed by NM, 14-Oct-2007.) (Revised by set.mm contributors, 19-Dec-2013.)
   &       =>   
 
Theoremopelopab 4708* The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by NM, 16-May-1995.)
   &       &       &       =>   
 
Theorembrab 4709* The law of concretion for a binary relation. (Contributed by NM, 16-Aug-1999.)
   &       &       &       &       =>   
 
Theoremopelopabaf 4710* The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopab 4708 uses bound-variable hypotheses in place of distinct variable conditions." (Contributed by Mario Carneiro, 19-Dec-2013.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)

 F/   &     F/   &       &       &       =>   
 
Theoremopelopabf 4711* The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopab 4708 uses bound-variable hypotheses in place of distinct variable conditions." (Contributed by NM, 19-Dec-2008.)

 F/   &     F/   &       &       &       &       =>   
 
Theoremssopab2 4712 Equivalence of ordered pair abstraction subclass and implication. (Contributed by NM, 27-Dec-1996.) (Revised by Mario Carneiro, 19-May-2013.)
 
Theoremssopab2b 4713 Equivalence of ordered pair abstraction subclass and implication. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
 
Theoremssopab2i 4714 Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 5-Apr-1995.)
   =>   
 
Theoremssopab2dv 4715* Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 19-Jan-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
   =>   
 
Theoremopabn0 4716 Non-empty ordered pair class abstraction. (Contributed by NM, 10-Oct-2007.)
 
2.3.5  Set construction functions
 
Syntaxc1st 4717 Extend the definition of a class to include the first member an ordered pair function.
 
Syntaxcswap 4718 Extend the definition of a class to include the swap function.
Swap
 
Syntaxcsset 4719 Extend the definition of a class to include the subset relationship.
S
 
Syntaxcsi 4720 Extend the definition of a class to include the singleton image.
SI
 
Syntaxccom 4721 Extend the definition of a class to include the composition of two classes.
 
Syntaxcima 4722 Extend the definition of a class to include the image of one class under another.
 
Definitiondf-1st 4723* Define a function that extracts the first member, or abscissa, of an ordered pair. (Contributed by SF, 5-Jan-2015.)
 
Definitiondf-swap 4724* Define a function that swaps the two elements of an ordered pair. (Contributed by SF, 5-Jan-2015.)
Swap
 
Definitiondf-sset 4725* Define a relationship that holds between subsets. (Contributed by SF, 5-Jan-2015.)
S
 
Definitiondf-co 4726* Define the composition of two classes. (Contributed by SF, 5-Jan-2015.)
 
Definitiondf-ima 4727* Define the image of one class under another. (Contributed by SF, 5-Jan-2015.)
 
Definitiondf-si 4728* Define the singleton image of a class. (Contributed by SF, 5-Jan-2015.)
SI
 
Theoremel1st 4729* Membership in . (Contributed by SF, 5-Jan-2015.)
 
Theorembr1stg 4730 The binary relationship over the function. (Contributed by SF, 5-Jan-2015.)
 
Theoremsetconslem1 4731* Lemma for the set construction theorems. (Contributed by SF, 6-Jan-2015.)
   &       =>    Sk k SIk kImagekImagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k Nn k Phi
 
Theoremsetconslem2 4732* Lemma for the set construction theorems. (Contributed by SF, 6-Jan-2015.)
   &       =>    Ins2k Sk Ins3k SIk Ins2k Sk Ins3k kImagekImagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k Nn k k Sk 0c k k1 1 1ck1 1 1c Phi 0c
 
Theoremsetconslem3 4733 Lemma for set construction functions. Set up a mapping between Kuratowski and Quine ordered pairs. (Contributed by SF, 7-Jan-2015.)
   &       &       =>    Ins3k SIk SIk Sk Ins2k Ins3k Sk k SIk kImagekImagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins2k Ins2k Sk Ins3k SIk Ins2k Sk Ins3k kImagekImagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k Nn k k Sk 0c k k1 1 1ck1 1 1ck1 1 1 1 1c
 
Theoremsetconslem4 4734* Lemma for set construction functions. Create a mapping between the two types of ordered pair abstractions. (Contributed by SF, 7-Jan-2015.)
11 k k k Ins3k SIk SIk Sk Ins2k Ins3k Sk k SIk kImagekImagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins2k Ins2k Sk Ins3k SIk Ins2k Sk Ins3k kImagekImagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k Nn k k Sk 0c k k1 1 1ck1 1 1ck1 1 1 1 1ck
 
Theoremsetconslem5 4735 Lemma for set construction theorems. The big expression in the middle of setconslem4 4734 forms a set. (Contributed by SF, 7-Jan-2015.)
Ins3k SIk SIk Sk Ins2k Ins3k Sk k SIk kImagekImagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins2k Ins2k Sk Ins3k SIk Ins2k Sk Ins3k kImagekImagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k Nn k k Sk 0c k k1 1 1ck1 1 1ck1 1 1 1 1c
 
Theoremsetconslem6 4736* Lemma for the set construction functions. Invert the expression from setconslem4 4734. (Contributed by SF, 7-Jan-2015.)
k k Ins3k SIk SIk Sk Ins2k Ins3k Sk k SIk kImagekImagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins2k Ins2k Sk Ins3k SIk Ins2k Sk Ins3k kImagekImagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k Nn k k Sk 0c k k1 1 1ck1 1 1ck1 1 1 1 1ck1 1
 
Theoremsetconslem7 4737 Lemma for the set construction theorems. Reorganized version of setconslem3 4733. (Contributed by SF, 4-Feb-2015.)
   &       &       =>    Ins2k Ins3k Sk Ins2k Ins2k Sk k SIk kImagekImagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins3k SIk SIk Ins2k Sk Ins3k SIk Ins2k Sk Ins3k kImagekImagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k Nn k k Sk 0c k k1 1 1ck1 1 1ck1 1 1 1 1c
 
Theoremdf1st2 4738 Express the function via the set construction functions. (Contributed by SF, 4-Feb-2015.)
11 k k k Ins3k SIk SIk Sk Ins2k Ins3k Sk k SIk kImagekImagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins2k Ins2k Sk Ins3k SIk Ins2k Sk Ins3k kImagekImagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k Nn k k Sk 0c k k1 1 1ck1 1 1ck1 1 1 1 1ck Ins2k Ins3k Sk Ins2k Ins2k Sk k SIk kImagekImagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins3k SIk SIk Ins2k Sk Ins3k SIk Ins2k Sk Ins3k kImagekImagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k Nn k k Sk 0c k k1 1 1ck1 1 1ck1 1 1 1 1ck1 1c
 
Theorem1stex 4739 The function is a set. (Contributed by SF, 6-Jan-2015.)
 
Theoremelswap 4740* Membership in the Swap function. (Contributed by SF, 6-Jan-2015.)
Swap
 
Theoremdfswap2 4741 Express the Swap function via set construction operators. (Contributed by SF, 6-Jan-2015.)
Swap Ins2k Ins2k Sk Ins2k Ins2k Ins3k Sk k SIk kImagekImagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins3k SIk SIk Ins2k Sk Ins3k SIk Ins2k Sk Ins3k kImagekImagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k Nn k k Sk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk ImagekImagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k Nn k k1 1 1 1 1 1 1c Ins2k Ins3k SIk SIk Sk k SIk kImagekImagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins2k Ins3k Ins2k Sk Ins3k SIk Ins2k Sk Ins3k kImagekImagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k Nn k k Sk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk Ins2k Sk Ins3k kImagekImagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k Nn k k Sk 0c k k1 1 1ck1 1 1 1 1 1 1ck1 1 1 1 1ck1 1ck
 
Theoremswapex 4742 The Swap function is a set. (Contributed by SF, 6-Jan-2015.)
Swap
 
Theoremdfsset2 4743 Express the S relationship via the set construction functors. (Contributed by SF, 7-Jan-2015.)
S 11 k k k Ins3k SIk SIk Sk Ins2k Ins3k Sk k SIk kImagekImagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins2k Ins2k Sk Ins3k SIk Ins2k Sk Ins3k kImagekImagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k Nn k k Sk 0c k k1 1 1ck1 1 1ck1 1 1 1 1ck Sk
 
Theoremssetex 4744 The subset relationship is a set. (Contributed by SF, 6-Jan-2015.)
S
 
Theoremdfima2 4745 Express the image functor in terms of the set construction functions. (Contributed by SF, 7-Jan-2015.)
k k Ins3k SIk SIk Sk Ins2k Ins3k Sk k SIk kImagekImagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins2k Ins2k Sk Ins3k SIk Ins2k Sk Ins3k kImagekImagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k Nn k k Sk 0c k k1 1 1ck1 1 1ck1 1 1 1 1ck1 1 k
 
Theoremimaexg 4746 The image of a set under a set is a set. (Contributed by SF, 7-Jan-2015.)
 
Theoremimaex 4747 The image of a set under a set is a set. (Contributed by SF, 7-Jan-2015.)
   &       =>   
 
Theoremdfco1 4748 Express Quine composition via Kuratowski composition. (Contributed by SF, 7-Jan-2015.)
11 k k k Ins3k SIk SIk Sk Ins2k Ins3k Sk k SIk kImagekImagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins2k Ins2k Sk Ins3k SIk Ins2k Sk Ins3k kImagekImagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k Nn k k Sk 0c k k1 1 1ck1 1 1ck1 1 1 1 1ck k k Ins3k SIk SIk Sk Ins2k Ins3k Sk k SIk kImagekImagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins2k Ins2k Sk Ins3k SIk Ins2k Sk Ins3k kImagekImagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k Nn k k Sk 0c k k1 1 1ck1 1 1ck1 1 1 1 1ck1 1 k k k Ins3k SIk SIk Sk Ins2k Ins3k Sk k SIk kImagekImagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins2k Ins2k Sk Ins3k SIk Ins2k Sk Ins3k kImagekImagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k Nn k k Sk 0c k k1 1 1ck1 1 1ck1 1 1 1 1ck1 1
 
Theoremcoexg 4749 The composition of two sets is a set. (Contributed by SF, 7-Jan-2015.)
 
Theoremcoex 4750 The composition of two sets is a set. (Contributed by SF, 7-Jan-2015.)
   &       =>   
 
Theoremdfsi2 4751 Express singleton image in terms of the Kuratowski singleton image. (Contributed by SF, 7-Jan-2015.)
SI 11 k k k Ins3k SIk SIk Sk Ins2k Ins3k Sk k SIk kImagekImagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins2k Ins2k Sk Ins3k SIk Ins2k Sk Ins3k kImagekImagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k Nn k k Sk 0c k k1 1 1ck1 1 1ck1 1 1 1 1ck SIk k k Ins3k SIk SIk Sk Ins2k Ins3k Sk k SIk kImagekImagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins2k Ins2k Sk Ins3k SIk Ins2k Sk Ins3k kImagekImagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k Nn k k Sk 0c k k1 1 1ck1 1 1ck1 1 1 1 1ck1 1
 
Theoremsiexg 4752 The singleton image of a set is a set. (Contributed by SF, 7-Jan-2015.)
SI
 
Theoremsiex 4753 The singleton image of a set is a set. (Contributed by SF, 7-Jan-2015.)
   =>    SI
 
Theoremelima 4754* Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by SF, 19-Apr-2004.)
 
Theoremelima2 4755* Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by SF, 11-Aug-2004.)
 
Theoremelima3 4756* Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by SF, 14-Aug-1994.)
 
Theorembrssetg 4757 Binary relationship form of the subset relationship. (Contributed by SF, 11-Feb-2015.)
S
 
Theorembrsset 4758 Binary relationship form of the subset relationship. (Contributed by SF, 11-Feb-2015.)
   &       =>    S
 
Theorembrssetsn 4759 Set membership in terms of the subset relationship. (Contributed by SF, 11-Feb-2015.)
   &       =>    S
 
Theoremopelssetsn 4760 Set membership in terms of the subset relationship. (Contributed by SF, 11-Feb-2015.)
   &       =>    S
 
Theorembrsi 4761* Binary relationship over a singleton image. (Contributed by SF, 11-Feb-2015.)
SI
 
2.3.6  Epsilon and identity relations
 
Syntaxcep 4762 Extend class notation to include the epsilon relation.
 
Syntaxcid 4763 Extend the definition of a class to include identity relation.
 
Definitiondf-eprel 4764* Define the epsilon relation. Similar to Definition 6.22 of [TakeutiZaring] p. 30. (Contributed by SF, 5-Jan-2015.)
 
Theoremepelc 4765 The epsilon relation and the membership relation are the same. (Contributed by NM, 13-Aug-1995.)
   =>   
 
Theoremepel 4766 The epsilon relation and the membership relation are the same. (Contributed by NM, 13-Aug-1995.)
 
Definitiondf-id 4767* Define the identity relation. Definition 9.15 of [Quine] p. 64. (Contributed by SF, 5-Jan-2015.)
 
Theoremdfid3 4768 A stronger version of df-id 4767 that doesn't require and to be distinct. Ordinarily, we wouldn't use this as a definition, since non-distinct dummy variables would make soundness verification more difficult (as the proof here shows). The proof can be instructive in showing how distinct variable requirements may be eliminated, a task that is not necessarily obvious. (Contributed by NM, 5-Feb-2008.) (Revised by Mario Carneiro, 18-Nov-2016.)
 
Theoremdfid2 4769 Alternate definition of the identity relation. (Contributed by NM, 15-Mar-2007.)
 
2.3.7  Functions and relations
 
Syntaxcxp 4770 Extend the definition of a class to include the cross product.
 
Syntaxccnv 4771 Extend the definition of a class to include the converse of a class.
 
Syntaxcdm 4772 Extend the definition of a class to include the domain of a class.
 
Syntaxcrn 4773 Extend the definition of a class to include the range of a class.
 
Syntaxcres 4774 Extend the definition of a class to include the restriction of a class. (Read: The restriction of to .)
 
Syntaxwfun 4775 Extend the definition of a wff to include the function predicate. (Read: is a function.)
 
Syntaxwfn 4776 Extend the definition of a wff to include the function predicate with a domain. (Read: is a function on .)
 
Syntaxwf 4777 Extend the definition of a wff to include the function predicate with domain and codomain. (Read: maps into .)
 
Syntaxwf1 4778 Extend the definition of a wff to include one-to-one functions. (Read: maps one-to-one into .) The notation ("1-1" above the arrow) is from Definition 6.15(5) of [TakeutiZaring] p. 27.
 
Syntaxwfo 4779 Extend the definition of a wff to include onto functions. (Read: maps onto .) The notation ("onto" below the arrow) is from Definition 6.15(4) of [TakeutiZaring] p. 27.
 
Syntaxwf1o 4780 Extend the definition of a wff to include one-to-one onto functions. (Read: maps one-to-one onto .) The notation ("1-1" above the arrow and "onto" below the arrow) is from Definition 6.15(6) of [TakeutiZaring] p. 27.
 
Syntaxcfv 4781 Extend the definition of a class to include the value of a function. (Read: The value of at , or " of .")
 
Syntaxwiso 4782 Extend the definition of a wff to include the isomorphism property. (Read: is an , isomorphism of onto .)
 
Syntaxc2nd 4783 Extend the definition of a class to include the second function.
 
Definitiondf-xp 4784* Define the cross product of two classes. Definition 9.11 of [Quine] p. 64. (Contributed by SF, 5-Jan-2015.)
 
Definitiondf-cnv 4785* Define the converse of a class. Definition 9.12 of [Quine] p. 64. We use Quine's breve accent (smile) notation. Like Quine, we use it as a prefix, which eliminates the need for parentheses. Many authors use the postfix superscript "to the minus one." "Converse" is Quine's terminology; some authors call it "inverse," especially when the argument is a function. (Contributed by SF, 5-Jan-2015.)
 
Definitiondf-rn 4786 Define the range of a class. The notation " " is used by Enderton; other authors sometimes use script R or script W. (Contributed by SF, 5-Jan-2015.)
 
Definitiondf-dm 4787 Define the domain of a class. The notation " " is used by Enderton; other authors sometimes use script D. (Contributed by SF, 5-Jan-2015.)
 
Definitiondf-res 4788 Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. (Contributed by SF, 5-Jan-2015.)
 
Definitiondf-fun 4789 Define a function. Definition 10.1 of [Quine] p. 65. For alternate definitions, see dffun2 5119, dffun3 5120, dffun4 5121, dffun5 5122, dffun6 5124, dffun7 5133, dffun8 5134, and dffun9 5135. (Contributed by SF, 5-Jan-2015.) (Revised by Scott Fenton, 14-Apr-2021.)
 
Definitiondf-fn 4790 Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 5224, dffn3 5229, dffn4 5275, and dffn5 5363. (Contributed by SF, 5-Jan-2015.)
 
Definitiondf-f 4791 Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. For alternate definitions, see dff2 5419, dff3 5420, and dff4 5421. (Contributed by SF, 5-Jan-2015.)
 
Definitiondf-f1 4792 Define a one-to-one function. For equivalent definitions see dff12 5257 and dff13 5471. Compare Definition 6.15(5) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow). (Contributed by SF, 5-Jan-2015.)
 
Definitiondf-fo 4793 Define an onto function. Definition 6.15(4) of [TakeutiZaring] p. 27. We use their notation ("onto" under the arrow). For alternate definitions, see dffo2 5273, dffo3 5422, dffo4 5423, and dffo5 5424. (Contributed by SF, 5-Jan-2015.)
 
Definitiondf-f1o 4794 Define a one-to-one onto function. For equivalent definitions see dff1o2 5291, dff1o3 5292, dff1o4 5294, and dff1o5 5295. Compare Definition 6.15(6) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow and "onto" below the arrow). (Contributed by SF, 5-Jan-2015.)
 
Definitiondf-fv 4795* Define the value of a function. (Contributed by SF, 5-Jan-2015.)
 
Definitiondf-iso 4796* Define the isomorphism predicate. We read this as " is an , isomorphism of onto ." Normally, and are ordering relations on and respectively. Definition 6.28 of [TakeutiZaring] p. 32, whose notation is the same as ours except that and are subscripts. (Contributed by SF, 5-Jan-2015.)
 
Definitiondf-2nd 4797* Define the function. This function extracts the second member of an ordered pair. (Contributed by SF, 5-Jan-2015.)
 
Theoremxpeq1 4798 Equality theorem for cross product. (Contributed by NM, 4-Jul-1994.)
 
Theoremxpeq2 4799 Equality theorem for cross product. (Contributed by NM, 5-Jul-1994.)
 
Theoremelxpi 4800* Membership in a cross product. Uses fewer axioms than elxp 4801. (Contributed by NM, 4-Jul-1994.)
    < Previous  Next >

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-6329
  Copyright terms: Public domain < Previous  Next >