Home | Metamath
Proof Explorer Theorem List (p. 50 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dtrucor2 4901 | The theorem form of the deduction dtrucor 4900 leads to a contradiction, as mentioned in the "Wrong!" example at mmdeduction.html#bad. (Contributed by NM, 20-Oct-2007.) |
Theorem | dvdemo1 4902* | Demonstration of a theorem (scheme) that requires (meta)variables and to be distinct, but no others. It bundles the theorem schemes and . Compare dvdemo2 4903. ("Bundles" is a term introduced by Raph Levien.) (Contributed by NM, 1-Dec-2006.) |
Theorem | dvdemo2 4903* | Demonstration of a theorem (scheme) that requires (meta)variables and to be distinct, but no others. It bundles the theorem schemes and . Compare dvdemo1 4902. (Contributed by NM, 1-Dec-2006.) |
Theorem | zfpair 4904 |
The Axiom of Pairing of Zermelo-Fraenkel set theory. Axiom 2 of
[TakeutiZaring] p. 15. In some
textbooks this is stated as a separate
axiom; here we show it is redundant since it can be derived from the
other axioms.
This theorem should not be referenced by any proof other than axpr 4905. Instead, use zfpair2 4907 below so that the uses of the Axiom of Pairing can be more easily identified. (Contributed by NM, 18-Oct-1995.) (New usage is discouraged.) |
Theorem | axpr 4905* |
Unabbreviated version of the Axiom of Pairing of ZF set theory, derived
as a theorem from the other axioms.
This theorem should not be referenced by any proof. Instead, use ax-pr 4906 below so that the uses of the Axiom of Pairing can be more easily identified. (Contributed by NM, 14-Nov-2006.) (New usage is discouraged.) |
Axiom | ax-pr 4906* | The Axiom of Pairing of ZF set theory. It was derived as theorem axpr 4905 above and is therefore redundant, but we state it as a separate axiom here so that its uses can be identified more easily. (Contributed by NM, 14-Nov-2006.) |
Theorem | zfpair2 4907 | Derive the abbreviated version of the Axiom of Pairing from ax-pr 4906. See zfpair 4904 for its derivation from the other axioms. (Contributed by NM, 14-Nov-2006.) |
Theorem | snex 4908 | A singleton is a set. Theorem 7.12 of [Quine] p. 51, proved using Extensionality, Separation, Null Set, and Pairing. See also snexALT 4852. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 19-May-2013.) (Proof modification is discouraged.) |
Theorem | prex 4909 | The Axiom of Pairing using class variables. Theorem 7.13 of [Quine] p. 51. By virtue of its definition, an unordered pair remains a set (even though no longer a pair) even when its components are proper classes (see prprc 4302), so we can dispense with hypotheses requiring them to be sets. (Contributed by NM, 15-Jul-1993.) |
Theorem | elALT 4910* | Alternate proof of el 4847, shorter but requiring more axioms. (Contributed by NM, 4-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | dtruALT2 4911* | Alternate proof of dtru 4857 using ax-pr 4906 instead of ax-pow 4843. (Contributed by Mario Carneiro, 31-Aug-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | snelpwi 4912 | A singleton of a set belongs to the power class of a class containing the set. (Contributed by Alan Sare, 25-Aug-2011.) |
Theorem | snelpw 4913 | A singleton of a set belongs to the power class of a class containing the set. (Contributed by NM, 1-Apr-1998.) |
Theorem | prelpw 4914 | A pair of two sets belongs to the power class of a class containing those two sets and vice versa. (Contributed by AV, 8-Jan-2020.) |
Theorem | prelpwi 4915 | A pair of two sets belongs to the power class of a class containing those two sets. (Contributed by Thierry Arnoux, 10-Mar-2017.) (Proof shortened by AV, 23-Oct-2021.) |
Theorem | rext 4916* | A theorem similar to extensionality, requiring the existence of a singleton. Exercise 8 of [TakeutiZaring] p. 16. (Contributed by NM, 10-Aug-1993.) |
Theorem | sspwb 4917 | Classes are subclasses if and only if their power classes are subclasses. Exercise 18 of [TakeutiZaring] p. 18. (Contributed by NM, 13-Oct-1996.) |
Theorem | unipw 4918 | 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.) |
Theorem | univ 4919 | The union of the universe is the universe. Exercise 4.12(c) of [Mendelson] p. 235. (Contributed by NM, 14-Sep-2003.) |
Theorem | pwel 4920 | Membership of a power class. Exercise 10 of [Enderton] p. 26. (Contributed by NM, 13-Jan-2007.) |
Theorem | pwtr 4921 | A class is transitive iff its power class is transitive. (Contributed by Alan Sare, 25-Aug-2011.) (Revised by Mario Carneiro, 15-Jun-2014.) |
Theorem | ssextss 4922* | An extensionality-like principle defining subclass in terms of subsets. (Contributed by NM, 30-Jun-2004.) |
Theorem | ssext 4923* | 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.) |
Theorem | nssss 4924* | Negation of subclass relationship. Compare nss 3663. (Contributed by NM, 30-Jun-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
Theorem | pweqb 4925 | Classes are equal if and only if their power classes are equal. Exercise 19 of [TakeutiZaring] p. 18. (Contributed by NM, 13-Oct-1996.) |
Theorem | intid 4926* | The intersection of all sets to which a set belongs is the singleton of that set. (Contributed by NM, 5-Jun-2009.) |
Theorem | moabex 4927 | "At most one" existence implies a class abstraction exists. (Contributed by NM, 30-Dec-1996.) |
Theorem | rmorabex 4928 | Restricted "at most one" existence implies a restricted class abstraction exists. (Contributed by NM, 17-Jun-2017.) |
Theorem | euabex 4929 | The abstraction of a wff with existential uniqueness exists. (Contributed by NM, 25-Nov-1994.) |
Theorem | nnullss 4930* | A nonempty class (even if proper) has a nonempty subset. (Contributed by NM, 23-Aug-2003.) |
Theorem | exss 4931* | Restricted existence in a class (even if proper) implies restricted existence in a subset. (Contributed by NM, 23-Aug-2003.) |
Theorem | opex 4932 | An ordered pair of classes is a set. Exercise 7 of [TakeutiZaring] p. 16. (Contributed by NM, 18-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | otex 4933 | An ordered triple of classes is a set. (Contributed by NM, 3-Apr-2015.) |
Theorem | elopg 4934 | Characterization of the elements of an ordered pair. Closed form of elop 4935. (Contributed by BJ, 22-Jun-2019.) (Avoid depending on this detail.) |
Theorem | elop 4935 | Characterization of the elements of an ordered pair. Exercise 3 of [TakeutiZaring] p. 15. (Contributed by NM, 15-Jul-1993.) (Revised by Mario Carneiro, 26-Apr-2015.) Remove an extraneous hypothesis. (Revised by BJ, 25-Dec-2020.) (Avoid depending on this detail.) |
Theorem | elopOLD 4936 | Obsolete version of elop 4935, with one extraneous hypothesis. Obsolete as of 25-Dec-2020 . (Contributed by NM, 15-Jul-1993.) (Revised by Mario Carneiro, 26-Apr-2015.) (Avoid depending on this detail.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | opi1 4937 | One of the two elements in an ordered pair. (Contributed by NM, 15-Jul-1993.) (Revised by Mario Carneiro, 26-Apr-2015.) (Avoid depending on this detail.) |
Theorem | opi2 4938 | One of the two elements of an ordered pair. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.) (Avoid depending on this detail.) |
Theorem | opeluu 4939 | Each member of an ordered pair belongs to the union of the union of a class to which the ordered pair belongs. Lemma 3D of [Enderton] p. 41. (Contributed by NM, 31-Mar-1995.) (Revised by Mario Carneiro, 27-Feb-2016.) |
Theorem | op1stb 4940 | Extract the first member of an ordered pair. Theorem 73 of [Suppes] p. 42. (See op2ndb 5619 to extract the second member, op1sta 5617 for an alternate version, and op1st 7176 for the preferred version.) (Contributed by NM, 25-Nov-2003.) |
Theorem | brv 4941 | Two classes are always in relation by . This is simply equivalent to , and does not imply that is a relation: see nrelv 5244. (Contributed by Scott Fenton, 11-Apr-2012.) |
Theorem | opnz 4942 | An ordered pair is nonempty iff the arguments are sets. (Contributed by NM, 24-Jan-2004.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | opnzi 4943 | An ordered pair is nonempty if the arguments are sets. (Contributed by Mario Carneiro, 26-Apr-2015.) |
Theorem | opth1 4944 | Equality of the first members of equal ordered pairs. (Contributed by NM, 28-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | opth 4945 | 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 and are not required to be sets due our specific ordered pair definition. (Contributed by NM, 28-May-1995.) |
Theorem | opthg 4946 | Ordered pair theorem. and 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.) |
Theorem | opth1g 4947 | Equality of the first members of equal ordered pairs. Closed form of opth1 4944. (Contributed by AV, 14-Oct-2018.) |
Theorem | opthg2 4948 | Ordered pair theorem. (Contributed by NM, 14-Oct-2005.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | opth2 4949 | Ordered pair theorem. (Contributed by NM, 21-Sep-2014.) |
Theorem | opthneg 4950 | Two ordered pairs are not equal iff their first components or their second components are not equal. (Contributed by AV, 13-Dec-2018.) |
Theorem | opthne 4951 | Two ordered pairs are not equal iff their first components or their second components are not equal. (Contributed by AV, 13-Dec-2018.) |
Theorem | otth2 4952 | Ordered triple theorem, with triple expressed with ordered pairs. (Contributed by NM, 1-May-1995.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | otth 4953 | Ordered triple theorem. (Contributed by NM, 25-Sep-2014.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | otthg 4954 | Ordered triple theorem, closed form. (Contributed by Alexander van der Vekens, 10-Mar-2018.) |
Theorem | eqvinop 4955* | A variable introduction law for ordered pairs. Analogue of Lemma 15 of [Monk2] p. 109. (Contributed by NM, 28-May-1995.) |
Theorem | copsexg 4956* | Substitution of class for ordered pair . (Contributed by NM, 27-Dec-1996.) (Revised by Andrew Salmon, 11-Jul-2011.) (Proof shortened by Wolf Lammen, 25-Aug-2019.) |
Theorem | copsex2t 4957* | Closed theorem form of copsex2g 4958. (Contributed by NM, 17-Feb-2013.) |
Theorem | copsex2g 4958* | Implicit substitution inference for ordered pairs. (Contributed by NM, 28-May-1995.) |
Theorem | copsex4g 4959* | An implicit substitution inference for 2 ordered pairs. (Contributed by NM, 5-Aug-1995.) |
Theorem | 0nelop 4960 | A property of ordered pairs. (Contributed by Mario Carneiro, 26-Apr-2015.) |
Theorem | opwo0id 4961 | An ordered pair is equal to the ordered pair without the empty set. This is because no ordered pair contains the empty set. (Contributed by AV, 15-Nov-2021.) |
Theorem | opeqex 4962 | Equivalence of existence implied by equality of ordered pairs. (Contributed by NM, 28-May-2008.) |
Theorem | oteqex2 4963 | Equivalence of existence implied by equality of ordered triples. (Contributed by NM, 26-Apr-2015.) |
Theorem | oteqex 4964 | Equivalence of existence implied by equality of ordered triples. (Contributed by NM, 28-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | opcom 4965 | An ordered pair commutes iff its members are equal. (Contributed by NM, 28-May-2009.) |
Theorem | moop2 4966* | "At most one" property of an ordered pair. (Contributed by NM, 11-Apr-2004.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | opeqsn 4967 | Equivalence for an ordered pair equal to a singleton. (Contributed by NM, 3-Jun-2008.) |
Theorem | opeqpr 4968 | Equivalence for an ordered pair equal to an unordered pair. (Contributed by NM, 3-Jun-2008.) (Avoid depending on this detail.) |
Theorem | snopeqop 4969 | Equivalence for an ordered pair equal to a singleton of an ordered pair. (Contributed by AV, 18-Sep-2020.) |
Theorem | propeqop 4970 | Equivalence for an ordered pair equal to a pair of ordered pairs. (Contributed by AV, 18-Sep-2020.) |
Theorem | propssopi 4971 | If a pair of ordered pairs is a subset of an ordered pair, their first components are equal. (Contributed by AV, 20-Sep-2020.) |
Theorem | mosubopt 4972* | "At most one" remains true inside ordered pair quantification. (Contributed by NM, 28-Aug-2007.) |
Theorem | mosubop 4973* | "At most one" remains true inside ordered pair quantification. (Contributed by NM, 28-May-1995.) |
Theorem | euop2 4974* | Transfer existential uniqueness to second member of an ordered pair. (Contributed by NM, 10-Apr-2004.) |
Theorem | euotd 4975* | Prove existential uniqueness for an ordered triple. (Contributed by Mario Carneiro, 20-May-2015.) |
Theorem | opthwiener 4976 | Justification theorem for the ordered pair definition in Norbert Wiener, "A simplification of the logic of relations," Proc. of the Cambridge Philos. Soc., 1914, vol. 17, pp.387-390. It is also shown as a definition in [Enderton] p. 36 and as Exercise 4.8(b) of [Mendelson] p. 230. It is meaningful only for classes that exist as sets (i.e. are not proper classes). See df-op 4184 for other ordered pair definitions. (Contributed by NM, 28-Sep-2003.) |
Theorem | uniop 4977 | 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.) |
Theorem | uniopel 4978 | Ordered pair membership is inherited by class union. (Contributed by NM, 13-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | otsndisj 4979* | The singletons consisting of ordered triples which have distinct third components are disjoint. (Contributed by Alexander van der Vekens, 10-Mar-2018.) |
Disj | ||
Theorem | otiunsndisj 4980* | The union of singletons consisting of ordered triples which have distinct first and third components are disjoint. (Contributed by Alexander van der Vekens, 10-Mar-2018.) |
Disj | ||
Theorem | iunopeqop 4981* | Implication of an ordered pair being equal to an indexed union of singletons of ordered pairs. (Contributed by AV, 20-Sep-2020.) |
Theorem | opabid 4982 | 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.) |
Theorem | elopab 4983* | Membership in a class abstraction of pairs. (Contributed by NM, 24-Mar-1998.) |
Theorem | opelopabsbALT 4984* | The law of concretion in terms of substitutions. Less general than opelopabsb 4985, 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.) |
Theorem | opelopabsb 4985* | The law of concretion in terms of substitutions. (Contributed by NM, 30-Sep-2002.) (Revised by Mario Carneiro, 18-Nov-2016.) |
Theorem | brabsb 4986* | The law of concretion in terms of substitutions. (Contributed by NM, 17-Mar-2008.) |
Theorem | opelopabt 4987* | Closed theorem form of opelopab 4997. (Contributed by NM, 19-Feb-2013.) |
Theorem | opelopabga 4988* | The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 19-Dec-2013.) |
Theorem | brabga 4989* | The law of concretion for a binary relation. (Contributed by Mario Carneiro, 19-Dec-2013.) |
Theorem | opelopab2a 4990* | Ordered pair membership in an ordered pair class abstraction. (Contributed by Mario Carneiro, 19-Dec-2013.) |
Theorem | opelopaba 4991* | The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 19-Dec-2013.) |
Theorem | braba 4992* | The law of concretion for a binary relation. (Contributed by NM, 19-Dec-2013.) |
Theorem | opelopabg 4993* | The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro, 19-Dec-2013.) |
Theorem | brabg 4994* | The law of concretion for a binary relation. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 19-Dec-2013.) |
Theorem | opelopabgf 4995* | The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopabg 4993 uses bound-variable hypotheses in place of distinct variable conditions. (Contributed by Alexander van der Vekens, 8-Jul-2018.) |
Theorem | opelopab2 4996* | Ordered pair membership in an ordered pair class abstraction. (Contributed by NM, 14-Oct-2007.) (Revised by Mario Carneiro, 19-Dec-2013.) |
Theorem | opelopab 4997* | The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by NM, 16-May-1995.) |
Theorem | brab 4998* | The law of concretion for a binary relation. (Contributed by NM, 16-Aug-1999.) |
Theorem | opelopabaf 4999* | The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopab 4997 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.) |
Theorem | opelopabf 5000* | The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopab 4997 uses bound-variable hypotheses in place of distinct variable conditions." (Contributed by NM, 19-Dec-2008.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |