![]() |
Metamath
Proof Explorer Theorem List (p. 47 of 484) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30748) |
![]() (30749-32271) |
![]() (32272-48316) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | elimel 4601 | Eliminate a membership hypothesis for weak deduction theorem, when special case 𝐵 ∈ 𝐶 is provable. (Contributed by NM, 15-May-1999.) |
⊢ 𝐵 ∈ 𝐶 ⇒ ⊢ if(𝐴 ∈ 𝐶, 𝐴, 𝐵) ∈ 𝐶 | ||
Theorem | elimdhyp 4602 | Version of elimhyp 4597 where the hypothesis is deduced from the final antecedent. See divalg 16387 for an example of its use. (Contributed by Paul Chapman, 25-Mar-2008.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜒)) & ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜃 ↔ 𝜒)) & ⊢ 𝜃 ⇒ ⊢ 𝜒 | ||
Theorem | keephyp 4603 | Transform a hypothesis 𝜓 that we want to keep (but contains the same class variable 𝐴 used in the eliminated hypothesis) for use with the weak deduction theorem. (Contributed by NM, 15-May-1999.) |
⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜃)) & ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜃)) & ⊢ 𝜓 & ⊢ 𝜒 ⇒ ⊢ 𝜃 | ||
Theorem | keephyp2v 4604 | Keep a hypothesis containing 2 class variables (for use with the weak deduction theorem dedth 4590). (Contributed by NM, 16-Apr-2005.) |
⊢ (𝐴 = if(𝜑, 𝐴, 𝐶) → (𝜓 ↔ 𝜒)) & ⊢ (𝐵 = if(𝜑, 𝐵, 𝐷) → (𝜒 ↔ 𝜃)) & ⊢ (𝐶 = if(𝜑, 𝐴, 𝐶) → (𝜏 ↔ 𝜂)) & ⊢ (𝐷 = if(𝜑, 𝐵, 𝐷) → (𝜂 ↔ 𝜃)) & ⊢ 𝜓 & ⊢ 𝜏 ⇒ ⊢ 𝜃 | ||
Theorem | keephyp3v 4605 | Keep a hypothesis containing 3 class variables. (Contributed by NM, 27-Sep-1999.) |
⊢ (𝐴 = if(𝜑, 𝐴, 𝐷) → (𝜌 ↔ 𝜒)) & ⊢ (𝐵 = if(𝜑, 𝐵, 𝑅) → (𝜒 ↔ 𝜃)) & ⊢ (𝐶 = if(𝜑, 𝐶, 𝑆) → (𝜃 ↔ 𝜏)) & ⊢ (𝐷 = if(𝜑, 𝐴, 𝐷) → (𝜂 ↔ 𝜁)) & ⊢ (𝑅 = if(𝜑, 𝐵, 𝑅) → (𝜁 ↔ 𝜎)) & ⊢ (𝑆 = if(𝜑, 𝐶, 𝑆) → (𝜎 ↔ 𝜏)) & ⊢ 𝜌 & ⊢ 𝜂 ⇒ ⊢ 𝜏 | ||
Syntax | cpw 4606 | Extend class notation to include power class. (The tilde in the Metamath token is meant to suggest the calligraphic font of the P.) |
class 𝒫 𝐴 | ||
Theorem | pwjust 4607* | Soundness justification theorem for df-pw 4608. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ {𝑥 ∣ 𝑥 ⊆ 𝐴} = {𝑦 ∣ 𝑦 ⊆ 𝐴} | ||
Definition | df-pw 4608* | Define power class. Definition 5.10 of [TakeutiZaring] p. 17, but we also let it apply to proper classes, i.e. those that are not members of V. When applied to a set, this produces its power set. A power set of S is the set of all subsets of S, including the empty set and S itself. For example, if 𝐴 = {3, 5, 7}, then 𝒫 𝐴 = {∅, {3}, {5}, {7}, {3, 5}, {3, 7}, {5, 7}, {3, 5, 7}} (ex-pw 30259). We will later introduce the Axiom of Power Sets ax-pow 5369, which can be expressed in class notation per pwexg 5382. Still later we will prove, in hashpw 14435, that the size of the power set of a finite set is 2 raised to the power of the size of the set. (Contributed by NM, 24-Jun-1993.) |
⊢ 𝒫 𝐴 = {𝑥 ∣ 𝑥 ⊆ 𝐴} | ||
Theorem | elpwg 4609 | Membership in a power class. Theorem 86 of [Suppes] p. 47. See also elpw2g 5350. (Contributed by NM, 6-Aug-2000.) (Proof shortened by BJ, 31-Dec-2023.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) | ||
Theorem | elpw 4610 | Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 31-Dec-1993.) (Proof shortened by BJ, 31-Dec-2023.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵) | ||
Theorem | velpw 4611 | Setvar variable membership in a power class. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴) | ||
Theorem | elpwd 4612 | Membership in a power class. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐵) | ||
Theorem | elpwi 4613 | Subset relation implied by membership in a power class. (Contributed by NM, 17-Feb-2007.) |
⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵) | ||
Theorem | elpwb 4614 | Characterization of the elements of a power class. (Contributed by BJ, 29-Apr-2021.) |
⊢ (𝐴 ∈ 𝒫 𝐵 ↔ (𝐴 ∈ V ∧ 𝐴 ⊆ 𝐵)) | ||
Theorem | elpwid 4615 | An element of a power class is a subclass. Deduction form of elpwi 4613. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | ||
Theorem | elelpwi 4616 | If 𝐴 belongs to a part of 𝐶, then 𝐴 belongs to 𝐶. (Contributed by FL, 3-Aug-2009.) |
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝒫 𝐶) → 𝐴 ∈ 𝐶) | ||
Theorem | sspw 4617 | The powerclass preserves inclusion. See sspwb 5455 for the biconditional version. (Contributed by NM, 13-Oct-1996.) Extract forward implication of sspwb 5455 since it requires fewer axioms. (Revised by BJ, 13-Apr-2024.) |
⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵) | ||
Theorem | sspwi 4618 | The powerclass preserves inclusion (inference form). (Contributed by BJ, 13-Apr-2024.) |
⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ 𝒫 𝐴 ⊆ 𝒫 𝐵 | ||
Theorem | sspwd 4619 | The powerclass preserves inclusion (deduction form). (Contributed by BJ, 13-Apr-2024.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → 𝒫 𝐴 ⊆ 𝒫 𝐵) | ||
Theorem | pweq 4620 | Equality theorem for power class. (Contributed by NM, 21-Jun-1993.) (Proof shortened by BJ, 13-Apr-2024.) |
⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵) | ||
Theorem | pweqALT 4621 | Alternate proof of pweq 4620 directly from the definition. (Contributed by NM, 21-Jun-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵) | ||
Theorem | pweqi 4622 | Equality inference for power class. (Contributed by NM, 27-Nov-2013.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ 𝒫 𝐴 = 𝒫 𝐵 | ||
Theorem | pweqd 4623 | Equality deduction for power class. (Contributed by NM, 27-Nov-2013.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 𝒫 𝐴 = 𝒫 𝐵) | ||
Theorem | pwunss 4624 | The power class of the union of two classes includes the union of their power classes. Exercise 4.12(k) of [Mendelson] p. 235. (Contributed by NM, 23-Nov-2003.) Remove use of ax-sep 5303, ax-nul 5310, ax-pr 5433 and shorten proof. (Revised by BJ, 13-Apr-2024.) |
⊢ (𝒫 𝐴 ∪ 𝒫 𝐵) ⊆ 𝒫 (𝐴 ∪ 𝐵) | ||
Theorem | nfpw 4625 | Bound-variable hypothesis builder for power class. (Contributed by NM, 28-Oct-2003.) (Revised by Mario Carneiro, 13-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥𝒫 𝐴 | ||
Theorem | pwidg 4626 | A set is an element of its power set. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ 𝒫 𝐴) | ||
Theorem | pwidb 4627 | A class is an element of its powerclass if and only if it is a set. (Contributed by BJ, 31-Dec-2023.) |
⊢ (𝐴 ∈ V ↔ 𝐴 ∈ 𝒫 𝐴) | ||
Theorem | pwid 4628 | A set is a member of its power class. Theorem 87 of [Suppes] p. 47. (Contributed by NM, 5-Aug-1993.) |
⊢ 𝐴 ∈ V ⇒ ⊢ 𝐴 ∈ 𝒫 𝐴 | ||
Theorem | pwss 4629* | Subclass relationship for power class. (Contributed by NM, 21-Jun-2009.) |
⊢ (𝒫 𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐵)) | ||
Theorem | pwundif 4630 | Break up the power class of a union into a union of smaller classes. (Contributed by NM, 25-Mar-2007.) (Proof shortened by Thierry Arnoux, 20-Dec-2016.) Remove use of ax-sep 5303, ax-nul 5310, ax-pr 5433 and shorten proof. (Revised by BJ, 14-Apr-2024.) |
⊢ 𝒫 (𝐴 ∪ 𝐵) = ((𝒫 (𝐴 ∪ 𝐵) ∖ 𝒫 𝐴) ∪ 𝒫 𝐴) | ||
Theorem | snjust 4631* | Soundness justification theorem for df-sn 4633. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ {𝑥 ∣ 𝑥 = 𝐴} = {𝑦 ∣ 𝑦 = 𝐴} | ||
Syntax | csn 4632 | Extend class notation to include singleton. |
class {𝐴} | ||
Definition | df-sn 4633* | Define the singleton of a class. Definition 7.1 of [Quine] p. 48. For convenience, it is well-defined for proper classes, i.e., those that are not elements of V, see snprc 4726. For an alternate definition see dfsn2 4645. (Contributed by NM, 21-Jun-1993.) |
⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴} | ||
Syntax | cpr 4634 | Extend class notation to include unordered pair. |
class {𝐴, 𝐵} | ||
Definition | df-pr 4635 |
Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. For
example, 𝐴 ∈ {1, -1} → (𝐴↑2) = 1 (ex-pr 30260). They are
unordered, so {𝐴, 𝐵} = {𝐵, 𝐴} as proven by prcom 4741. For a more
traditional definition, but requiring a dummy variable, see dfpr2 4652.
{𝐴,
𝐴} is also an
unordered pair, but also a singleton because of
{𝐴} =
{𝐴, 𝐴} (see dfsn2 4645). Therefore, {𝐴, 𝐵} is called
a proper (unordered) pair iff 𝐴 ≠ 𝐵 and 𝐴 and 𝐵 are
sets.
Note: ordered pairs are a completely different object defined below in df-op 4639. When the term "pair" is used without qualifier, it generally means "unordered pair", and the context makes it clear which version is meant. (Contributed by NM, 21-Jun-1993.) |
⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵}) | ||
Syntax | ctp 4636 | Extend class notation to include unordered triple (sometimes called "unordered triplet"). |
class {𝐴, 𝐵, 𝐶} | ||
Definition | df-tp 4637 |
Define unordered triple of classes. Definition of [Enderton] p. 19.
Note: ordered triples are a completely different object defined below in df-ot 4641. As with all tuples, when the term "triple" is used without qualifier, it means "ordered triple". (Contributed by NM, 9-Apr-1994.) |
⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶}) | ||
Syntax | cop 4638 | Extend class notation to include ordered pair. |
class 〈𝐴, 𝐵〉 | ||
Definition | df-op 4639* |
Definition of an ordered pair, equivalent to Kuratowski's definition
{{𝐴}, {𝐴, 𝐵}} when the arguments are sets.
Since the
behavior of Kuratowski definition is not very useful for proper classes,
we define it to be empty in this case (see opprc1 4902, opprc2 4903, and
0nelop 5502). For Kuratowski's actual definition when
the arguments are
sets, see dfop 4877. For the justifying theorem (for sets) see
opth 5482.
See dfopif 4875 for an equivalent formulation using the if operation.
Definition 9.1 of [Quine] p. 58 defines an ordered pair unconditionally as 〈𝐴, 𝐵〉 = {{𝐴}, {𝐴, 𝐵}}, which has different behavior from our df-op 4639 when the arguments are proper classes. Ordinarily this difference is not important, since neither definition is meaningful in that case. Our df-op 4639 was chosen because it often makes proofs shorter by eliminating unnecessary sethood hypotheses. There are other ways to define ordered pairs. The basic requirement is that two ordered pairs are equal iff their respective members are equal. In 1914 Norbert Wiener gave the first successful definition 〈𝐴, 𝐵〉2 = {{{𝐴}, ∅}, {{𝐵}}}, justified by opthwiener 5520. This was simplified by Kazimierz Kuratowski in 1921 to our present definition. An even simpler definition 〈𝐴, 𝐵〉3 = {𝐴, {𝐴, 𝐵}} is justified by opthreg 9649, but it requires the Axiom of Regularity for its justification and is not commonly used. A definition that also works for proper classes is 〈𝐴, 𝐵〉4 = ((𝐴 × {∅}) ∪ (𝐵 × {{∅}})), justified by opthprc 5746. Nearly at the same time as Norbert Wiener, Felix Hausdorff proposed the following definition in "Grundzüge der Mengenlehre" ("Basics of Set Theory"), p. 32, in 1914: 〈𝐴, 𝐵〉5 = {{𝐴, 𝑂}, {𝐵, 𝑇}}. Hausdorff used 1 and 2 instead of 𝑂 and 𝑇, but actually any two different fixed sets will do (e.g., 𝑂 = ∅ and 𝑇 = {∅}, see 0nep0 5362). Furthermore, Hausdorff demanded that 𝑂 and 𝑇 are both different from 𝐴 as well as 𝐵, which is actually not necessary (at least not in full extent), see opthhausdorff0 5524 and opthhausdorff 5523. If we restrict our sets to nonnegative integers, an ordered pair definition that involves only elementary arithmetic is provided by nn0opthi 14269. An ordered pair of real numbers can also be represented by a complex number as shown by cru 12242. Kuratowski's ordered pair definition is standard for ZFC set theory, but it is very inconvenient to use in New Foundations theory because it is not type-level; a common alternate definition in New Foundations is the definition from [Rosser] p. 281. Since there are other ways to define ordered pairs, we discourage direct use of this definition so that most theorems won't depend on this particular construction; theorems will instead rely on dfopif 4875. (Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro, 26-Apr-2015.) (Avoid depending on this detail.) |
⊢ 〈𝐴, 𝐵〉 = {𝑥 ∣ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})} | ||
Syntax | cotp 4640 | Extend class notation to include ordered triple. |
class 〈𝐴, 𝐵, 𝐶〉 | ||
Definition | df-ot 4641 | Define ordered triple of classes. Definition of ordered triple in [Stoll] p. 25. (Contributed by NM, 3-Apr-2015.) |
⊢ 〈𝐴, 𝐵, 𝐶〉 = 〈〈𝐴, 𝐵〉, 𝐶〉 | ||
Theorem | sneq 4642 | Equality theorem for singletons. Part of Exercise 4 of [TakeutiZaring] p. 15. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵}) | ||
Theorem | sneqi 4643 | Equality inference for singletons. (Contributed by NM, 22-Jan-2004.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ {𝐴} = {𝐵} | ||
Theorem | sneqd 4644 | Equality deduction for singletons. (Contributed by NM, 22-Jan-2004.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → {𝐴} = {𝐵}) | ||
Theorem | dfsn2 4645 | Alternate definition of singleton. Definition 5.1 of [TakeutiZaring] p. 15. (Contributed by NM, 24-Apr-1994.) |
⊢ {𝐴} = {𝐴, 𝐴} | ||
Theorem | elsng 4646 | There is exactly one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15 (generalized). (Contributed by NM, 13-Sep-1995.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)) | ||
Theorem | elsn 4647 | There is exactly one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. (Contributed by NM, 13-Sep-1995.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵) | ||
Theorem | velsn 4648 | There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) | ||
Theorem | elsni 4649 | There is at most one element in a singleton. (Contributed by NM, 5-Jun-1994.) |
⊢ (𝐴 ∈ {𝐵} → 𝐴 = 𝐵) | ||
Theorem | rabsneq 4650* | Equality of class abstractions restricted to a singleton. (Contributed by AV, 17-May-2025.) |
⊢ (𝑁 ∈ 𝑉 → {𝑥 ∈ {𝑁} ∣ 𝜓} = {𝑥 ∈ 𝑉 ∣ (𝑥 = 𝑁 ∧ 𝜓)}) | ||
Theorem | absn 4651* | Condition for a class abstraction to be a singleton. Formerly part of proof of dfiota2 6506. (Contributed by Andrew Salmon, 30-Jun-2011.) (Revised by AV, 24-Aug-2022.) |
⊢ ({𝑥 ∣ 𝜑} = {𝑌} ↔ ∀𝑥(𝜑 ↔ 𝑥 = 𝑌)) | ||
Theorem | dfpr2 4652* | Alternate definition of a pair. Definition 5.1 of [TakeutiZaring] p. 15. (Contributed by NM, 24-Apr-1994.) |
⊢ {𝐴, 𝐵} = {𝑥 ∣ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵)} | ||
Theorem | dfsn2ALT 4653 | Alternate definition of singleton, based on the (alternate) definition of pair. Definition 5.1 of [TakeutiZaring] p. 15. (Contributed by AV, 12-Jun-2022.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ {𝐴} = {𝐴, 𝐴} | ||
Theorem | elprg 4654 | A member of a pair of classes is one or the other of them, and conversely as soon as it is a set. Exercise 1 of [TakeutiZaring] p. 15, generalized. (Contributed by NM, 13-Sep-1995.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))) | ||
Theorem | elpri 4655 | If a class is an element of a pair, then it is one of the two paired elements. (Contributed by Scott Fenton, 1-Apr-2011.) |
⊢ (𝐴 ∈ {𝐵, 𝐶} → (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)) | ||
Theorem | elpr 4656 | A member of a pair of classes is one or the other of them, and conversely as soon as it is a set. Exercise 1 of [TakeutiZaring] p. 15. (Contributed by NM, 13-Sep-1995.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)) | ||
Theorem | elpr2g 4657 | A member of a pair of sets is one or the other of them, and conversely. Exercise 1 of [TakeutiZaring] p. 15. (Contributed by NM, 14-Oct-2005.) Generalize from sethood hypothesis to sethood antecedent. (Revised by BJ, 25-May-2024.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))) | ||
Theorem | elpr2 4658 | A member of a pair of sets is one or the other of them, and conversely. Exercise 1 of [TakeutiZaring] p. 15. (Contributed by NM, 14-Oct-2005.) (Proof shortened by JJ, 23-Jul-2021.) |
⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)) | ||
Theorem | elpr2OLD 4659 | Obsolete version of elpr2 4658 as of 25-May-2024. (Contributed by NM, 14-Oct-2005.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)) | ||
Theorem | nelpr2 4660 | If a class is not an element of an unordered pair, it is not the second listed element. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝐴 ∈ {𝐵, 𝐶}) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐶) | ||
Theorem | nelpr1 4661 | If a class is not an element of an unordered pair, it is not the first listed element. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝐴 ∈ {𝐵, 𝐶}) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) | ||
Theorem | nelpri 4662 | If an element doesn't match the items in an unordered pair, it is not in the unordered pair. (Contributed by David A. Wheeler, 10-May-2015.) |
⊢ 𝐴 ≠ 𝐵 & ⊢ 𝐴 ≠ 𝐶 ⇒ ⊢ ¬ 𝐴 ∈ {𝐵, 𝐶} | ||
Theorem | prneli 4663 | If an element doesn't match the items in an unordered pair, it is not in the unordered pair, using ∉. (Contributed by David A. Wheeler, 10-May-2015.) |
⊢ 𝐴 ≠ 𝐵 & ⊢ 𝐴 ≠ 𝐶 ⇒ ⊢ 𝐴 ∉ {𝐵, 𝐶} | ||
Theorem | nelprd 4664 | If an element doesn't match the items in an unordered pair, it is not in the unordered pair, deduction version. (Contributed by Alexander van der Vekens, 25-Jan-2018.) |
⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐴 ≠ 𝐶) ⇒ ⊢ (𝜑 → ¬ 𝐴 ∈ {𝐵, 𝐶}) | ||
Theorem | eldifpr 4665 | Membership in a set with two elements removed. Similar to eldifsn 4795 and eldiftp 4695. (Contributed by Mario Carneiro, 18-Jul-2017.) |
⊢ (𝐴 ∈ (𝐵 ∖ {𝐶, 𝐷}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷)) | ||
Theorem | rexdifpr 4666 | Restricted existential quantification over a set with two elements removed. (Contributed by Alexander van der Vekens, 7-Feb-2018.) (Proof shortened by Wolf Lammen, 15-May-2025.) |
⊢ (∃𝑥 ∈ (𝐴 ∖ {𝐵, 𝐶})𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝑥 ≠ 𝐵 ∧ 𝑥 ≠ 𝐶 ∧ 𝜑)) | ||
Theorem | snidg 4667 | A set is a member of its singleton. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 28-Oct-2003.) |
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴}) | ||
Theorem | snidb 4668 | A class is a set iff it is a member of its singleton. (Contributed by NM, 5-Apr-2004.) |
⊢ (𝐴 ∈ V ↔ 𝐴 ∈ {𝐴}) | ||
Theorem | snid 4669 | A set is a member of its singleton. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 31-Dec-1993.) |
⊢ 𝐴 ∈ V ⇒ ⊢ 𝐴 ∈ {𝐴} | ||
Theorem | vsnid 4670 | A setvar variable is a member of its singleton. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 𝑥 ∈ {𝑥} | ||
Theorem | elsn2g 4671 | There is exactly one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. This variation requires only that 𝐵, rather than 𝐴, be a set. (Contributed by NM, 28-Oct-2003.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)) | ||
Theorem | elsn2 4672 | There is exactly one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. This variation requires only that 𝐵, rather than 𝐴, be a set. (Contributed by NM, 12-Jun-1994.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵) | ||
Theorem | nelsn 4673 | If a class is not equal to the class in a singleton, then it is not in the singleton. (Contributed by Glauco Siliprandi, 17-Aug-2020.) (Proof shortened by BJ, 4-May-2021.) |
⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 ∈ {𝐵}) | ||
Theorem | rabeqsn 4674* | Conditions for a restricted class abstraction to be a singleton. (Contributed by AV, 18-Apr-2019.) (Proof shortened by AV, 26-Aug-2022.) |
⊢ ({𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑋} ↔ ∀𝑥((𝑥 ∈ 𝑉 ∧ 𝜑) ↔ 𝑥 = 𝑋)) | ||
Theorem | rabsssn 4675* | Conditions for a restricted class abstraction to be a subset of a singleton, i.e. to be a singleton or the empty set. (Contributed by AV, 18-Apr-2019.) |
⊢ ({𝑥 ∈ 𝑉 ∣ 𝜑} ⊆ {𝑋} ↔ ∀𝑥 ∈ 𝑉 (𝜑 → 𝑥 = 𝑋)) | ||
Theorem | rabeqsnd 4676* | Conditions for a restricted class abstraction to be a singleton, in deduction form. (Contributed by Thierry Arnoux, 2-Dec-2021.) |
⊢ (𝑥 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ (𝜑 → 𝜒) & ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝑥 = 𝐵) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝐵}) | ||
Theorem | ralsnsg 4677* | Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.) |
⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ [𝐴 / 𝑥]𝜑)) | ||
Theorem | rexsns 4678* | Restricted existential quantification over a singleton. (Contributed by Mario Carneiro, 23-Apr-2015.) (Revised by NM, 22-Aug-2018.) |
⊢ (∃𝑥 ∈ {𝐴}𝜑 ↔ [𝐴 / 𝑥]𝜑) | ||
Theorem | rexsngf 4679* | Restricted existential quantification over a singleton. (Contributed by NM, 29-Jan-2012.) (Revised by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) | ||
Theorem | ralsngf 4680* | Restricted universal quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by AV, 3-Apr-2023.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) | ||
Theorem | reusngf 4681* | Restricted existential uniqueness over a singleton. (Contributed by AV, 3-Apr-2023.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∃!𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) | ||
Theorem | ralsng 4682* | Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.) Avoid ax-10 2129, ax-12 2166. (Revised by Gino Giotto, 30-Sep-2024.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) | ||
Theorem | rexsng 4683* | Restricted existential quantification over a singleton. (Contributed by NM, 29-Jan-2012.) Avoid ax-10 2129, ax-12 2166. (Revised by Gino Giotto, 30-Sep-2024.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) | ||
Theorem | reusng 4684* | Restricted existential uniqueness over a singleton. (Contributed by AV, 3-Apr-2023.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∃!𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) | ||
Theorem | 2ralsng 4685* | Substitution expressed in terms of two quantifications over singletons. (Contributed by AV, 22-Dec-2019.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ {𝐴}∀𝑦 ∈ {𝐵}𝜑 ↔ 𝜒)) | ||
Theorem | ralsngOLD 4686* | Obsolete version of ralsng 4682 as of 30-Sep-2024. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.) (Proof shortened by AV, 7-Apr-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) | ||
Theorem | rexsngOLD 4687* | Obsolete version of rexsng 4683 as of 30-Sep-2024. (Contributed by NM, 29-Jan-2012.) (Proof shortened by AV, 7-Apr-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) | ||
Theorem | rexreusng 4688* | Restricted existential uniqueness over a singleton is equivalent to a restricted existential quantification over a singleton. (Contributed by AV, 3-Apr-2023.) |
⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}𝜑 ↔ ∃!𝑥 ∈ {𝐴}𝜑)) | ||
Theorem | exsnrex 4689 | There is a set being the element of a singleton if and only if there is an element of the singleton. (Contributed by Alexander van der Vekens, 1-Jan-2018.) |
⊢ (∃𝑥 𝑀 = {𝑥} ↔ ∃𝑥 ∈ 𝑀 𝑀 = {𝑥}) | ||
Theorem | ralsn 4690* | Convert a universal quantification restricted to a singleton to a substitution. (Contributed by NM, 27-Apr-2009.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓) | ||
Theorem | rexsn 4691* | Convert an existential quantification restricted to a singleton to a substitution. (Contributed by Jeff Madsen, 5-Jan-2011.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓) | ||
Theorem | elpwunsn 4692 | Membership in an extension of a power class. (Contributed by NM, 26-Mar-2007.) |
⊢ (𝐴 ∈ (𝒫 (𝐵 ∪ {𝐶}) ∖ 𝒫 𝐵) → 𝐶 ∈ 𝐴) | ||
Theorem | eqoreldif 4693 | An element of a set is either equal to another element of the set or a member of the difference of the set and the singleton containing the other element. (Contributed by AV, 25-Aug-2020.) (Proof shortened by JJ, 23-Jul-2021.) |
⊢ (𝐵 ∈ 𝐶 → (𝐴 ∈ 𝐶 ↔ (𝐴 = 𝐵 ∨ 𝐴 ∈ (𝐶 ∖ {𝐵})))) | ||
Theorem | eltpg 4694 | Members of an unordered triple of classes. (Contributed by FL, 2-Feb-2014.) (Proof shortened by Mario Carneiro, 11-Feb-2015.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵, 𝐶, 𝐷} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ∨ 𝐴 = 𝐷))) | ||
Theorem | eldiftp 4695 | Membership in a set with three elements removed. Similar to eldifsn 4795 and eldifpr 4665. (Contributed by David A. Wheeler, 22-Jul-2017.) |
⊢ (𝐴 ∈ (𝐵 ∖ {𝐶, 𝐷, 𝐸}) ↔ (𝐴 ∈ 𝐵 ∧ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ∧ 𝐴 ≠ 𝐸))) | ||
Theorem | eltpi 4696 | A member of an unordered triple of classes is one of them. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ (𝐴 ∈ {𝐵, 𝐶, 𝐷} → (𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ∨ 𝐴 = 𝐷)) | ||
Theorem | eltp 4697 | A member of an unordered triple of classes is one of them. Special case of Exercise 1 of [TakeutiZaring] p. 17. (Contributed by NM, 8-Apr-1994.) (Revised by Mario Carneiro, 11-Feb-2015.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ {𝐵, 𝐶, 𝐷} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ∨ 𝐴 = 𝐷)) | ||
Theorem | dftp2 4698* | Alternate definition of unordered triple of classes. Special case of Definition 5.3 of [TakeutiZaring] p. 16. (Contributed by NM, 8-Apr-1994.) |
⊢ {𝐴, 𝐵, 𝐶} = {𝑥 ∣ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶)} | ||
Theorem | nfpr 4699 | Bound-variable hypothesis builder for unordered pairs. (Contributed by NM, 14-Nov-1995.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥{𝐴, 𝐵} | ||
Theorem | ifpr 4700 | Membership of a conditional operator in an unordered pair. (Contributed by NM, 17-Jun-2007.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → if(𝜑, 𝐴, 𝐵) ∈ {𝐴, 𝐵}) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |