HomeHome Intuitionistic Logic Explorer
Theorem List (p. 40 of 102)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 3901-4000   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremrabex 3901* Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 19-Jul-1996.)
 |-  A  e.  _V   =>    |-  { x  e.  A  |  ph }  e.  _V
 
Theoremelssabg 3902* Membership in a class abstraction involving a subset. Unlike elabg 2688,  A does not have to be a set. (Contributed by NM, 29-Aug-2006.)
 |-  ( x  =  A  ->  ( ph  <->  ps ) )   =>    |-  ( B  e.  V  ->  ( A  e.  { x  |  ( x 
 C_  B  /\  ph ) } 
 <->  ( A  C_  B  /\  ps ) ) )
 
Theoreminteximm 3903* The intersection of an inhabited class exists. (Contributed by Jim Kingdon, 27-Aug-2018.)
 |-  ( E. x  x  e.  A  ->  |^| A  e.  _V )
 
Theoremintexr 3904 If the intersection of a class exists, the class is non-empty. (Contributed by Jim Kingdon, 27-Aug-2018.)
 |-  ( |^| A  e.  _V 
 ->  A  =/=  (/) )
 
Theoremintnexr 3905 If a class intersection is the universe, it is not a set. In classical logic this would be an equivalence. (Contributed by Jim Kingdon, 27-Aug-2018.)
 |-  ( |^| A  =  _V  ->  -.  |^| A  e.  _V )
 
Theoremintexabim 3906 The intersection of an inhabited class abstraction exists. (Contributed by Jim Kingdon, 27-Aug-2018.)
 |-  ( E. x ph  -> 
 |^| { x  |  ph }  e.  _V )
 
Theoremintexrabim 3907 The intersection of an inhabited restricted class abstraction exists. (Contributed by Jim Kingdon, 27-Aug-2018.)
 |-  ( E. x  e.  A  ph  ->  |^| { x  e.  A  |  ph }  e.  _V )
 
Theoremiinexgm 3908* The existence of an indexed union. 
x is normally a free-variable parameter in  B, which should be read  B ( x ). (Contributed by Jim Kingdon, 28-Aug-2018.)
 |-  ( ( E. x  x  e.  A  /\  A. x  e.  A  B  e.  C )  ->  |^|_ x  e.  A  B  e.  _V )
 
Theoreminuni 3909* The intersection of a union  U. A with a class  B is equal to the union of the intersections of each element of  A with  B. (Contributed by FL, 24-Mar-2007.)
 |-  ( U. A  i^i  B )  =  U. { x  |  E. y  e.  A  x  =  ( y  i^i  B ) }
 
Theoremelpw2g 3910 Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 7-Aug-2000.)
 |-  ( B  e.  V  ->  ( A  e.  ~P B 
 <->  A  C_  B )
 )
 
Theoremelpw2 3911 Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 11-Oct-2007.)
 |-  B  e.  _V   =>    |-  ( A  e.  ~P B  <->  A  C_  B )
 
Theorempwnss 3912 The power set of a set is never a subset. (Contributed by Stefan O'Rear, 22-Feb-2015.)
 |-  ( A  e.  V  ->  -.  ~P A  C_  A )
 
Theorempwne 3913 No set equals its power set. The sethood antecedent is necessary; compare pwv 3579. (Contributed by NM, 17-Nov-2008.) (Proof shortened by Mario Carneiro, 23-Dec-2016.)
 |-  ( A  e.  V  ->  ~P A  =/=  A )
 
Theoremrepizf2lem 3914 Lemma for repizf2 3915. If we have a function-like proposition which provides at most one value of  y for each  x in a set  w, we can change "at most one" to "exactly one" by restricting the values of  x to those values for which the proposition provides a value of  y. (Contributed by Jim Kingdon, 7-Sep-2018.)
 |-  ( A. x  e.  w  E* y ph  <->  A. x  e.  { x  e.  w  |  E. y ph } E! y ph )
 
Theoremrepizf2 3915* Replacement. This version of replacement is stronger than repizf 3873 in the sense that  ph does not need to map all values of  x in  w to a value of  y. The resulting set contains those elements for which there is a value of  y and in that sense, this theorem combines repizf 3873 with ax-sep 3875. Another variation would be  A. x  e.  w E* y ph  ->  { y  |  E. x ( x  e.  w  /\  ph ) }  e.  _V but we don't have a proof of that yet. (Contributed by Jim Kingdon, 7-Sep-2018.)
 |- 
 F/ z ph   =>    |-  ( A. x  e.  w  E* y ph  ->  E. z A. x  e.  { x  e.  w  |  E. y ph } E. y  e.  z  ph )
 
2.2.5  Theorems requiring empty set existence
 
Theoremclass2seteq 3916* Equality theorem for classes and sets . (Contributed by NM, 13-Dec-2005.) (Proof shortened by Raph Levien, 30-Jun-2006.)
 |-  ( A  e.  V  ->  { x  e.  A  |  A  e.  _V }  =  A )
 
Theorem0elpw 3917 Every power class contains the empty set. (Contributed by NM, 25-Oct-2007.)
 |-  (/)  e.  ~P A
 
Theorem0nep0 3918 The empty set and its power set are not equal. (Contributed by NM, 23-Dec-1993.)
 |-  (/)  =/=  { (/) }
 
Theorem0inp0 3919 Something cannot be equal to both the null set and the power set of the null set. (Contributed by NM, 30-Sep-2003.)
 |-  ( A  =  (/)  ->  -.  A  =  { (/) } )
 
Theoremunidif0 3920 The removal of the empty set from a class does not affect its union. (Contributed by NM, 22-Mar-2004.)
 |- 
 U. ( A  \  { (/) } )  = 
 U. A
 
Theoremiin0imm 3921* An indexed intersection of the empty set, with an inhabited index set, is empty. (Contributed by Jim Kingdon, 29-Aug-2018.)
 |-  ( E. y  y  e.  A  ->  |^|_ x  e.  A  (/)  =  (/) )
 
Theoremiin0r 3922* If an indexed intersection of the empty set is empty, the index set is non-empty. (Contributed by Jim Kingdon, 29-Aug-2018.)
 |-  ( |^|_ x  e.  A  (/) 
 =  (/)  ->  A  =/=  (/) )
 
Theoremintv 3923 The intersection of the universal class is empty. (Contributed by NM, 11-Sep-2008.)
 |- 
 |^| _V  =  (/)
 
Theoremaxpweq 3924* Two equivalent ways to express the Power Set Axiom. Note that ax-pow 3927 is not used by the proof. (Contributed by NM, 22-Jun-2009.)
 |-  A  e.  _V   =>    |-  ( ~P A  e.  _V  <->  E. x A. y
 ( A. z ( z  e.  y  ->  z  e.  A )  ->  y  e.  x ) )
 
2.2.6  Collection principle
 
Theorembnd 3925* A very strong generalization of the Axiom of Replacement (compare zfrep6 3874). Its strength lies in the rather profound fact that  ph ( x ,  y ) does not have to be a "function-like" wff, as it does in the standard Axiom of Replacement. This theorem is sometimes called the Boundedness Axiom. In the context of IZF, it is just a slight variation of ax-coll 3872. (Contributed by NM, 17-Oct-2004.)
 |-  ( A. x  e.  z  E. y ph  ->  E. w A. x  e.  z  E. y  e.  w  ph )
 
Theorembnd2 3926* A variant of the Boundedness Axiom bnd 3925 that picks a subset  z out of a possibly proper class 
B in which a property is true. (Contributed by NM, 4-Feb-2004.)
 |-  A  e.  _V   =>    |-  ( A. x  e.  A  E. y  e.  B  ph  ->  E. z
 ( z  C_  B  /\  A. x  e.  A  E. y  e.  z  ph ) )
 
2.3  IZF Set Theory - add the Axioms of Power Sets and Pairing
 
2.3.1  Introduce the Axiom of Power Sets
 
Axiomax-pow 3927* Axiom of Power Sets. An axiom of Intuitionistic Zermelo-Fraenkel set theory. It states that a set 
y exists that includes the power set of a given set  x i.e. contains every subset of  x. This is Axiom 8 of [Crosilla] p. "Axioms of CZF and IZF" except (a) unnecessary quantifiers are removed, and (b) Crosilla has a biconditional rather than an implication (but the two are equivalent by bm1.3ii 3878).

The variant axpow2 3929 uses explicit subset notation. A version using class notation is pwex 3932. (Contributed by NM, 5-Aug-1993.)

 |- 
 E. y A. z
 ( A. w ( w  e.  z  ->  w  e.  x )  ->  z  e.  y )
 
Theoremzfpow 3928* Axiom of Power Sets expressed with the fewest number of different variables. (Contributed by NM, 14-Aug-2003.)
 |- 
 E. x A. y
 ( A. x ( x  e.  y  ->  x  e.  z )  ->  y  e.  x )
 
Theoremaxpow2 3929* A variant of the Axiom of Power Sets ax-pow 3927 using subset notation. Problem in {BellMachover] p. 466. (Contributed by NM, 4-Jun-2006.)
 |- 
 E. y A. z
 ( z  C_  x  ->  z  e.  y )
 
Theoremaxpow3 3930* A variant of the Axiom of Power Sets ax-pow 3927. For any set  x, there exists a set  y whose members are exactly the subsets of  x i.e. the power set of  x. Axiom Pow of [BellMachover] p. 466. (Contributed by NM, 4-Jun-2006.)
 |- 
 E. y A. z
 ( z  C_  x  <->  z  e.  y )
 
Theoremel 3931* Every set is an element of some other set. (Contributed by NM, 4-Jan-2002.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
 |- 
 E. y  x  e.  y
 
Theorempwex 3932 Power set axiom expressed in class notation. Axiom 4 of [TakeutiZaring] p. 17. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
 |-  A  e.  _V   =>    |-  ~P A  e.  _V
 
Theorempwexg 3933 Power set axiom expressed in class notation, with the sethood requirement as an antecedent. Axiom 4 of [TakeutiZaring] p. 17. (Contributed by NM, 30-Oct-2003.)
 |-  ( A  e.  V  ->  ~P A  e.  _V )
 
Theoremabssexg 3934* Existence of a class of subsets. (Contributed by NM, 15-Jul-2006.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
 |-  ( A  e.  V  ->  { x  |  ( x  C_  A  /\  ph ) }  e.  _V )
 
TheoremsnexgOLD 3935 A singleton whose element exists is a set. The  A  e.  _V case of Theorem 7.12 of [Quine] p. 51, proved using only Extensionality, Power Set, and Separation. Replacement is not needed. This is a special case of snexg 3936 and new proofs should use snexg 3936 instead. (Contributed by Jim Kingdon, 26-Jan-2019.) (New usage is discouraged.) (Proof modification is discouraged.) TODO: replace its uses by uses of snexg 3936 and then remove it.
 |-  ( A  e.  _V  ->  { A }  e.  _V )
 
Theoremsnexg 3936 A singleton whose element exists is a set. The  A  e.  _V case of Theorem 7.12 of [Quine] p. 51, proved using only Extensionality, Power Set, and Separation. Replacement is not needed. (Contributed by Jim Kingdon, 1-Sep-2018.)
 |-  ( A  e.  V  ->  { A }  e.  _V )
 
Theoremsnex 3937 A singleton whose element exists is a set. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 24-May-2019.)
 |-  A  e.  _V   =>    |-  { A }  e.  _V
 
Theoremsnexprc 3938 A singleton whose element is a proper class is a set. The  -.  A  e.  _V case of Theorem 7.12 of [Quine] p. 51, proved using only Extensionality, Power Set, and Separation. Replacement is not needed. (Contributed by Jim Kingdon, 1-Sep-2018.)
 |-  ( -.  A  e.  _V 
 ->  { A }  e.  _V )
 
Theoremp0ex 3939 The power set of the empty set (the ordinal 1) is a set. (Contributed by NM, 23-Dec-1993.)
 |- 
 { (/) }  e.  _V
 
Theorempp0ex 3940  { (/) ,  { (/)
} } (the ordinal 2) is a set. (Contributed by NM, 5-Aug-1993.)
 |- 
 { (/) ,  { (/) } }  e.  _V
 
Theoremord3ex 3941 The ordinal number 3 is a set, proved without the Axiom of Union. (Contributed by NM, 2-May-2009.)
 |- 
 { (/) ,  { (/) } ,  { (/) ,  { (/) } } }  e.  _V
 
Theoremdtruarb 3942* At least two sets exist (or in terms of first-order logic, the universe of discourse has two or more objects). This theorem asserts the existence of two sets which do not equal each other; compare with dtruex 4283 in which we are given a set  y and go from there to a set  x which is not equal to it. (Contributed by Jim Kingdon, 2-Sep-2018.)
 |- 
 E. x E. y  -.  x  =  y
 
Theorempwuni 3943 A class is a subclass of the power class of its union. Exercise 6(b) of [Enderton] p. 38. (Contributed by NM, 14-Oct-1996.)
 |-  A  C_  ~P U. A
 
2.3.2  Axiom of Pairing
 
Axiomax-pr 3944* The Axiom of Pairing of IZF set theory. Axiom 2 of [Crosilla] p. "Axioms of CZF and IZF", except (a) unnecessary quantifiers are removed, and (b) Crosilla has a biconditional rather than an implication (but the two are equivalent by bm1.3ii 3878). (Contributed by NM, 14-Nov-2006.)
 |- 
 E. z A. w ( ( w  =  x  \/  w  =  y )  ->  w  e.  z )
 
Theoremzfpair2 3945 Derive the abbreviated version of the Axiom of Pairing from ax-pr 3944. (Contributed by NM, 14-Nov-2006.)
 |- 
 { x ,  y }  e.  _V
 
TheoremprexgOLD 3946 The Axiom of Pairing using class variables. Theorem 7.13 of [Quine] p. 51, but restricted to classes which exist. For proper classes, see prprc 3480, prprc1 3478, and prprc2 3479. This is a special case of prexg 3947 and new proofs should use prexg 3947 instead. (Contributed by Jim Kingdon, 25-Jul-2019.) (New usage is discouraged.) (Proof modification is discouraged.) TODO: replace its uses by uses of prexg 3947 and then remove it.
 |-  ( ( A  e.  _V 
 /\  B  e.  _V )  ->  { A ,  B }  e.  _V )
 
Theoremprexg 3947 The Axiom of Pairing using class variables. Theorem 7.13 of [Quine] p. 51, but restricted to classes which exist. For proper classes, see prprc 3480, prprc1 3478, and prprc2 3479. (Contributed by Jim Kingdon, 16-Sep-2018.)
 |-  ( ( A  e.  V  /\  B  e.  W )  ->  { A ,  B }  e.  _V )
 
Theoremsnelpwi 3948 A singleton of a set belongs to the power class of a class containing the set. (Contributed by Alan Sare, 25-Aug-2011.)
 |-  ( A  e.  B  ->  { A }  e.  ~P B )
 
Theoremsnelpw 3949 A singleton of a set belongs to the power class of a class containing the set. (Contributed by NM, 1-Apr-1998.)
 |-  A  e.  _V   =>    |-  ( A  e.  B 
 <->  { A }  e.  ~P B )
 
Theoremprelpwi 3950 A pair of two sets belongs to the power class of a class containing those two sets. (Contributed by Thierry Arnoux, 10-Mar-2017.)
 |-  ( ( A  e.  C  /\  B  e.  C )  ->  { A ,  B }  e.  ~P C )
 
Theoremrext 3951* A theorem similar to extensionality, requiring the existence of a singleton. Exercise 8 of [TakeutiZaring] p. 16. (Contributed by NM, 10-Aug-1993.)
 |-  ( A. z ( x  e.  z  ->  y  e.  z )  ->  x  =  y )
 
Theoremsspwb 3952 Classes are subclasses if and only if their power classes are subclasses. Exercise 18 of [TakeutiZaring] p. 18. (Contributed by NM, 13-Oct-1996.)
 |-  ( A  C_  B  <->  ~P A  C_  ~P B )
 
Theoremunipw 3953 A class equals the union of its power class. Exercise 6(a) of [Enderton] p. 38. (Contributed by NM, 14-Oct-1996.) (Proof shortened by Alan Sare, 28-Dec-2008.)
 |- 
 U. ~P A  =  A
 
Theorempwel 3954 Membership of a power class. Exercise 10 of [Enderton] p. 26. (Contributed by NM, 13-Jan-2007.)
 |-  ( A  e.  B  ->  ~P A  e.  ~P ~P U. B )
 
Theorempwtr 3955 A class is transitive iff its power class is transitive. (Contributed by Alan Sare, 25-Aug-2011.) (Revised by Mario Carneiro, 15-Jun-2014.)
 |-  ( Tr  A  <->  Tr  ~P A )
 
Theoremssextss 3956* An extensionality-like principle defining subclass in terms of subsets. (Contributed by NM, 30-Jun-2004.)
 |-  ( A  C_  B  <->  A. x ( x  C_  A  ->  x  C_  B ) )
 
Theoremssext 3957* An extensionality-like principle that uses the subset instead of the membership relation: two classes are equal iff they have the same subsets. (Contributed by NM, 30-Jun-2004.)
 |-  ( A  =  B  <->  A. x ( x  C_  A 
 <->  x  C_  B )
 )
 
Theoremnssssr 3958* Negation of subclass relationship. Compare nssr 3003. (Contributed by Jim Kingdon, 17-Sep-2018.)
 |-  ( E. x ( x  C_  A  /\  -.  x  C_  B )  ->  -.  A  C_  B )
 
Theorempweqb 3959 Classes are equal if and only if their power classes are equal. Exercise 19 of [TakeutiZaring] p. 18. (Contributed by NM, 13-Oct-1996.)
 |-  ( A  =  B  <->  ~P A  =  ~P B )
 
Theoremintid 3960* The intersection of all sets to which a set belongs is the singleton of that set. (Contributed by NM, 5-Jun-2009.)
 |-  A  e.  _V   =>    |-  |^| { x  |  A  e.  x }  =  { A }
 
Theoremeuabex 3961 The abstraction of a wff with existential uniqueness exists. (Contributed by NM, 25-Nov-1994.)
 |-  ( E! x ph  ->  { x  |  ph }  e.  _V )
 
Theoremmss 3962* An inhabited class (even if proper) has an inhabited subset. (Contributed by Jim Kingdon, 17-Sep-2018.)
 |-  ( E. y  y  e.  A  ->  E. x ( x  C_  A  /\  E. z  z  e.  x ) )
 
Theoremexss 3963* Restricted existence in a class (even if proper) implies restricted existence in a subset. (Contributed by NM, 23-Aug-2003.)
 |-  ( E. x  e.  A  ph  ->  E. y
 ( y  C_  A  /\  E. x  e.  y  ph ) )
 
Theoremopexg 3964 An ordered pair of sets is a set. (Contributed by Jim Kingdon, 11-Jan-2019.)
 |-  ( ( A  e.  V  /\  B  e.  W )  ->  <. A ,  B >.  e.  _V )
 
TheoremopexgOLD 3965 An ordered pair of sets is a set. This is a special case of opexg 3964 and new proofs should use opexg 3964 instead. (Contributed by Jim Kingdon, 19-Sep-2018.) (New usage is discouraged.) (Proof modification is discouraged.) TODO: replace its uses by uses of opexg 3964 and then remove it.
 |-  ( ( A  e.  _V 
 /\  B  e.  _V )  ->  <. A ,  B >.  e.  _V )
 
Theoremopex 3966 An ordered pair of sets is a set. (Contributed by Jim Kingdon, 24-Sep-2018.) (Revised by Mario Carneiro, 24-May-2019.)
 |-  A  e.  _V   &    |-  B  e.  _V   =>    |- 
 <. A ,  B >.  e. 
 _V
 
Theoremotexg 3967 An ordered triple of sets is a set. (Contributed by Jim Kingdon, 19-Sep-2018.)
 |-  ( ( A  e.  U  /\  B  e.  V  /\  C  e.  W ) 
 ->  <. A ,  B ,  C >.  e.  _V )
 
Theoremelop 3968 An ordered pair has two elements. Exercise 3 of [TakeutiZaring] p. 15. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.)
 |-  A  e.  _V   &    |-  B  e.  _V   &    |-  C  e.  _V   =>    |-  ( A  e.  <. B ,  C >. 
 <->  ( A  =  { B }  \/  A  =  { B ,  C } ) )
 
Theoremopi1 3969 One of the two elements in an ordered pair. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.)
 |-  A  e.  _V   &    |-  B  e.  _V   =>    |- 
 { A }  e.  <. A ,  B >.
 
Theoremopi2 3970 One of the two elements of an ordered pair. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.)
 |-  A  e.  _V   &    |-  B  e.  _V   =>    |- 
 { A ,  B }  e.  <. A ,  B >.
 
2.3.3  Ordered pair theorem
 
Theoremopm 3971* An ordered pair is inhabited iff the arguments are sets. (Contributed by Jim Kingdon, 21-Sep-2018.)
 |-  ( E. x  x  e.  <. A ,  B >.  <-> 
 ( A  e.  _V  /\  B  e.  _V )
 )
 
Theoremopnzi 3972 An ordered pair is nonempty if the arguments are sets (it is also inhabited; see opm 3971). (Contributed by Mario Carneiro, 26-Apr-2015.)
 |-  A  e.  _V   &    |-  B  e.  _V   =>    |- 
 <. A ,  B >.  =/=  (/)
 
Theoremopth1 3973 Equality of the first members of equal ordered pairs. (Contributed by NM, 28-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.)
 |-  A  e.  _V   &    |-  B  e.  _V   =>    |-  ( <. A ,  B >.  =  <. C ,  D >.  ->  A  =  C )
 
Theoremopth 3974 The ordered pair theorem. If two ordered pairs are equal, their first elements are equal and their second elements are equal. Exercise 6 of [TakeutiZaring] p. 16. Note that  C and  D are not required to be sets due our specific ordered pair definition. (Contributed by NM, 28-May-1995.)
 |-  A  e.  _V   &    |-  B  e.  _V   =>    |-  ( <. A ,  B >.  =  <. C ,  D >.  <-> 
 ( A  =  C  /\  B  =  D ) )
 
Theoremopthg 3975 Ordered pair theorem.  C and  D are not required to be sets under our specific ordered pair definition. (Contributed by NM, 14-Oct-2005.) (Revised by Mario Carneiro, 26-Apr-2015.)
 |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( <. A ,  B >.  =  <. C ,  D >. 
 <->  ( A  =  C  /\  B  =  D ) ) )
 
Theoremopthg2 3976 Ordered pair theorem. (Contributed by NM, 14-Oct-2005.) (Revised by Mario Carneiro, 26-Apr-2015.)
 |-  ( ( C  e.  V  /\  D  e.  W )  ->  ( <. A ,  B >.  =  <. C ,  D >. 
 <->  ( A  =  C  /\  B  =  D ) ) )
 
Theoremopth2 3977 Ordered pair theorem. (Contributed by NM, 21-Sep-2014.)
 |-  C  e.  _V   &    |-  D  e.  _V   =>    |-  ( <. A ,  B >.  =  <. C ,  D >.  <-> 
 ( A  =  C  /\  B  =  D ) )
 
Theoremotth2 3978 Ordered triple theorem, with triple express with ordered pairs. (Contributed by NM, 1-May-1995.) (Revised by Mario Carneiro, 26-Apr-2015.)
 |-  A  e.  _V   &    |-  B  e.  _V   &    |-  R  e.  _V   =>    |-  ( <.
 <. A ,  B >. ,  R >.  =  <. <. C ,  D >. ,  S >.  <->  ( A  =  C  /\  B  =  D  /\  R  =  S ) )
 
Theoremotth 3979 Ordered triple theorem. (Contributed by NM, 25-Sep-2014.) (Revised by Mario Carneiro, 26-Apr-2015.)
 |-  A  e.  _V   &    |-  B  e.  _V   &    |-  R  e.  _V   =>    |-  ( <. A ,  B ,  R >.  =  <. C ,  D ,  S >.  <->  ( A  =  C  /\  B  =  D  /\  R  =  S )
 )
 
Theoremeqvinop 3980* A variable introduction law for ordered pairs. Analog of Lemma 15 of [Monk2] p. 109. (Contributed by NM, 28-May-1995.)
 |-  B  e.  _V   &    |-  C  e.  _V   =>    |-  ( A  =  <. B ,  C >.  <->  E. x E. y
 ( A  =  <. x ,  y >.  /\  <. x ,  y >.  =  <. B ,  C >. ) )
 
Theoremcopsexg 3981* Substitution of class  A for ordered pair  <. x ,  y
>.. (Contributed by NM, 27-Dec-1996.) (Revised by Andrew Salmon, 11-Jul-2011.)
 |-  ( A  =  <. x ,  y >.  ->  ( ph 
 <-> 
 E. x E. y
 ( A  =  <. x ,  y >.  /\  ph )
 ) )
 
Theoremcopsex2t 3982* Closed theorem form of copsex2g 3983. (Contributed by NM, 17-Feb-2013.)
 |-  ( ( A. x A. y ( ( x  =  A  /\  y  =  B )  ->  ( ph 
 <->  ps ) )  /\  ( A  e.  V  /\  B  e.  W ) )  ->  ( E. x E. y ( <. A ,  B >.  =  <. x ,  y >.  /\  ph )  <->  ps ) )
 
Theoremcopsex2g 3983* Implicit substitution inference for ordered pairs. (Contributed by NM, 28-May-1995.)
 |-  ( ( x  =  A  /\  y  =  B )  ->  ( ph 
 <->  ps ) )   =>    |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( E. x E. y (
 <. A ,  B >.  = 
 <. x ,  y >.  /\  ph )  <->  ps ) )
 
Theoremcopsex4g 3984* An implicit substitution inference for 2 ordered pairs. (Contributed by NM, 5-Aug-1995.)
 |-  ( ( ( x  =  A  /\  y  =  B )  /\  (
 z  =  C  /\  w  =  D )
 )  ->  ( ph  <->  ps ) )   =>    |-  ( ( ( A  e.  R  /\  B  e.  S )  /\  ( C  e.  R  /\  D  e.  S )
 )  ->  ( E. x E. y E. z E. w ( ( <. A ,  B >.  =  <. x ,  y >.  /\  <. C ,  D >.  =  <. z ,  w >. )  /\  ph )  <->  ps ) )
 
Theorem0nelop 3985 A property of ordered pairs. (Contributed by Mario Carneiro, 26-Apr-2015.)
 |- 
 -.  (/)  e.  <. A ,  B >.
 
Theoremopeqex 3986 Equivalence of existence implied by equality of ordered pairs. (Contributed by NM, 28-May-2008.)
 |-  ( <. A ,  B >.  =  <. C ,  D >.  ->  ( ( A  e.  _V  /\  B  e.  _V )  <->  ( C  e.  _V 
 /\  D  e.  _V ) ) )
 
Theoremopcom 3987 An ordered pair commutes iff its members are equal. (Contributed by NM, 28-May-2009.)
 |-  A  e.  _V   &    |-  B  e.  _V   =>    |-  ( <. A ,  B >.  =  <. B ,  A >.  <->  A  =  B )
 
Theoremmoop2 3988* "At most one" property of an ordered pair. (Contributed by NM, 11-Apr-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
 |-  B  e.  _V   =>    |-  E* x  A  =  <. B ,  x >.
 
Theoremopeqsn 3989 Equivalence for an ordered pair equal to a singleton. (Contributed by NM, 3-Jun-2008.)
 |-  A  e.  _V   &    |-  B  e.  _V   &    |-  C  e.  _V   =>    |-  ( <. A ,  B >.  =  { C }  <->  ( A  =  B  /\  C  =  { A } ) )
 
Theoremopeqpr 3990 Equivalence for an ordered pair equal to an unordered pair. (Contributed by NM, 3-Jun-2008.)
 |-  A  e.  _V   &    |-  B  e.  _V   &    |-  C  e.  _V   &    |-  D  e.  _V   =>    |-  ( <. A ,  B >.  =  { C ,  D }  <->  ( ( C  =  { A }  /\  D  =  { A ,  B } )  \/  ( C  =  { A ,  B }  /\  D  =  { A } ) ) )
 
Theoremeuotd 3991* Prove existential uniqueness for an ordered triple. (Contributed by Mario Carneiro, 20-May-2015.)
 |-  ( ph  ->  A  e.  _V )   &    |-  ( ph  ->  B  e.  _V )   &    |-  ( ph  ->  C  e.  _V )   &    |-  ( ph  ->  ( ps 
 <->  ( a  =  A  /\  b  =  B  /\  c  =  C ) ) )   =>    |-  ( ph  ->  E! x E. a E. b E. c ( x  =  <. a ,  b ,  c >.  /\  ps )
 )
 
Theoremuniop 3992 The union of an ordered pair. Theorem 65 of [Suppes] p. 39. (Contributed by NM, 17-Aug-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
 |-  A  e.  _V   &    |-  B  e.  _V   =>    |- 
 U. <. A ,  B >.  =  { A ,  B }
 
Theoremuniopel 3993 Ordered pair membership is inherited by class union. (Contributed by NM, 13-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.)
 |-  A  e.  _V   &    |-  B  e.  _V   =>    |-  ( <. A ,  B >.  e.  C  ->  U. <. A ,  B >.  e.  U. C )
 
2.3.4  Ordered-pair class abstractions (cont.)
 
Theoremopabid 3994 The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. (Contributed by NM, 14-Apr-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
 |-  ( <. x ,  y >.  e.  { <. x ,  y >.  |  ph }  <->  ph )
 
Theoremelopab 3995* Membership in a class abstraction of pairs. (Contributed by NM, 24-Mar-1998.)
 |-  ( A  e.  { <. x ,  y >.  | 
 ph }  <->  E. x E. y
 ( A  =  <. x ,  y >.  /\  ph )
 )
 
TheoremopelopabsbALT 3996* The law of concretion in terms of substitutions. Less general than opelopabsb 3997, but having a much shorter proof. (Contributed by NM, 30-Sep-2002.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) (New usage is discouraged.) (Proof modification is discouraged.)
 |-  ( <. z ,  w >.  e.  { <. x ,  y >.  |  ph }  <->  [ w  /  y ] [ z  /  x ] ph )
 
Theoremopelopabsb 3997* The law of concretion in terms of substitutions. (Contributed by NM, 30-Sep-2002.) (Revised by Mario Carneiro, 18-Nov-2016.)
 |-  ( <. A ,  B >.  e.  { <. x ,  y >.  |  ph }  <->  [. A  /  x ].
 [. B  /  y ]. ph )
 
Theorembrabsb 3998* The law of concretion in terms of substitutions. (Contributed by NM, 17-Mar-2008.)
 |-  R  =  { <. x ,  y >.  |  ph }   =>    |-  ( A R B  <->  [. A  /  x ].
 [. B  /  y ]. ph )
 
Theoremopelopabt 3999* Closed theorem form of opelopab 4008. (Contributed by NM, 19-Feb-2013.)
 |-  ( ( A. x A. y ( x  =  A  ->  ( ph  <->  ps ) )  /\  A. x A. y ( y  =  B  ->  ( ps  <->  ch ) )  /\  ( A  e.  V  /\  B  e.  W ) )  ->  ( <. A ,  B >.  e.  { <. x ,  y >.  |  ph }  <->  ch ) )
 
Theoremopelopabga 4000* The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 19-Dec-2013.)
 |-  ( ( x  =  A  /\  y  =  B )  ->  ( ph 
 <->  ps ) )   =>    |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( <. A ,  B >.  e. 
 { <. x ,  y >.  |  ph }  <->  ps ) )
    < 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-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10124
  Copyright terms: Public domain < Previous  Next >