Home | Metamath
Proof Explorer Theorem List (p. 46 of 454) | < 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: | Metamath Proof Explorer
(1-28701) |
Hilbert Space Explorer
(28702-30224) |
Users' Mathboxes
(30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | elpw 4501 | 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 4502 | Setvar variable membership in a power class. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴) | ||
Theorem | elpwOLD 4503 | Obsolete proof of elpw 4501 as of 31-Dec-2023. (Proof modification is discouraged.) (New usage is discouraged.) (Contributed by NM, 31-Dec-1993.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵) | ||
Theorem | elpwgOLD 4504 | Obsolete proof of elpwg 4500 as of 31-Dec-2023. (Contributed by NM, 6-Aug-2000.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) | ||
Theorem | elpwd 4505 | Membership in a power class. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐵) | ||
Theorem | elpwi 4506 | Subset relation implied by membership in a power class. (Contributed by NM, 17-Feb-2007.) |
⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵) | ||
Theorem | elpwb 4507 | Characterization of the elements of a power class. (Contributed by BJ, 29-Apr-2021.) |
⊢ (𝐴 ∈ 𝒫 𝐵 ↔ (𝐴 ∈ V ∧ 𝐴 ⊆ 𝐵)) | ||
Theorem | elpwid 4508 | An element of a power class is a subclass. Deduction form of elpwi 4506. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | ||
Theorem | elelpwi 4509 | If 𝐴 belongs to a part of 𝐶, then 𝐴 belongs to 𝐶. (Contributed by FL, 3-Aug-2009.) |
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝒫 𝐶) → 𝐴 ∈ 𝐶) | ||
Theorem | sspw 4510 | The powerclass preserves inclusion. See sspwb 5307 for the biconditional version. (Contributed by NM, 13-Oct-1996.) Extract forward implication of sspwb 5307 since it requires fewer axioms. (Revised by BJ, 13-Apr-2024.) |
⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵) | ||
Theorem | sspwi 4511 | The powerclass preserves inclusion (inference form). (Contributed by BJ, 13-Apr-2024.) |
⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ 𝒫 𝐴 ⊆ 𝒫 𝐵 | ||
Theorem | sspwd 4512 | The powerclass preserves inclusion (deduction form). (Contributed by BJ, 13-Apr-2024.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → 𝒫 𝐴 ⊆ 𝒫 𝐵) | ||
Theorem | pweq 4513 | Equality theorem for power class. (Contributed by NM, 21-Jun-1993.) (Proof shortened by BJ, 13-Apr-2024.) |
⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵) | ||
Theorem | pweqALT 4514 | Alternate proof of pweq 4513 directly from the definition. (Contributed by NM, 21-Jun-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵) | ||
Theorem | pweqi 4515 | Equality inference for power class. (Contributed by NM, 27-Nov-2013.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ 𝒫 𝐴 = 𝒫 𝐵 | ||
Theorem | pweqd 4516 | Equality deduction for power class. (Contributed by NM, 27-Nov-2013.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 𝒫 𝐴 = 𝒫 𝐵) | ||
Theorem | pwunss 4517 | 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 5167, ax-nul 5174, ax-pr 5295 and shorten proof. (Revised by BJ, 13-Apr-2024.) |
⊢ (𝒫 𝐴 ∪ 𝒫 𝐵) ⊆ 𝒫 (𝐴 ∪ 𝐵) | ||
Theorem | nfpw 4518 | Bound-variable hypothesis builder for power class. (Contributed by NM, 28-Oct-2003.) (Revised by Mario Carneiro, 13-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥𝒫 𝐴 | ||
Theorem | pwidg 4519 | A set is an element of its power set. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ 𝒫 𝐴) | ||
Theorem | pwidb 4520 | 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 4521 | A set is a member of its power class. Theorem 87 of [Suppes] p. 47. (Contributed by NM, 5-Aug-1993.) |
⊢ 𝐴 ∈ V ⇒ ⊢ 𝐴 ∈ 𝒫 𝐴 | ||
Theorem | pwss 4522* | Subclass relationship for power class. (Contributed by NM, 21-Jun-2009.) |
⊢ (𝒫 𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐵)) | ||
Theorem | pwundif 4523 | 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 5167, ax-nul 5174, ax-pr 5295 and shorten proof. (Revised by BJ, 14-Apr-2024.) |
⊢ 𝒫 (𝐴 ∪ 𝐵) = ((𝒫 (𝐴 ∪ 𝐵) ∖ 𝒫 𝐴) ∪ 𝒫 𝐴) | ||
Theorem | snjust 4524* | Soundness justification theorem for df-sn 4526. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ {𝑥 ∣ 𝑥 = 𝐴} = {𝑦 ∣ 𝑦 = 𝐴} | ||
Syntax | csn 4525 | Extend class notation to include singleton. |
class {𝐴} | ||
Definition | df-sn 4526* | 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 4613. For an alternate definition see dfsn2 4538. (Contributed by NM, 21-Jun-1993.) |
⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴} | ||
Syntax | cpr 4527 | Extend class notation to include unordered pair. |
class {𝐴, 𝐵} | ||
Definition | df-pr 4528 |
Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. For
example, 𝐴 ∈ {1, -1} → (𝐴↑2) = 1 (ex-pr 28215). They are
unordered, so {𝐴, 𝐵} = {𝐵, 𝐴} as proven by prcom 4628. For a more
traditional definition, but requiring a dummy variable, see dfpr2 4544.
{𝐴,
𝐴} is also an
unordered pair, but also a singleton because of
{𝐴} =
{𝐴, 𝐴} (see dfsn2 4538). 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 4532. 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 4529 | Extend class notation to include unordered triple (sometimes called "unordered triplet"). |
class {𝐴, 𝐵, 𝐶} | ||
Definition | df-tp 4530 |
Define unordered triple of classes. Definition of [Enderton] p. 19.
Note: ordered triples are a completely different object defined below in df-ot 4534. As with all tuples, when the term "triple" is used without qualifier, it means "ordered triple". (Contributed by NM, 9-Apr-1994.) |
⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶}) | ||
Syntax | cop 4531 | Extend class notation to include ordered pair. |
class 〈𝐴, 𝐵〉 | ||
Definition | df-op 4532* |
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 4789, opprc2 4790, and
0nelop 5351). For Kuratowski's actual definition when
the arguments are
sets, see dfop 4762. For the justifying theorem (for sets) see
opth 5333.
See dfopif 4760 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 4532 when the arguments are proper classes. Ordinarily this difference is not important, since neither definition is meaningful in that case. Our df-op 4532 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 5369. This was simplified by Kazimierz Kuratowski in 1921 to our present definition. An even simpler definition 〈𝐴, 𝐵〉3 = {𝐴, {𝐴, 𝐵}} is justified by opthreg 9065, 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 5580. 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 5223). 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 5373 and opthhausdorff 5372. If we restrict our sets to nonnegative integers, an ordered pair definition that involves only elementary arithmetic is provided by nn0opthi 13626. An ordered pair of real numbers can also be represented by a complex number as shown by cru 11617. 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 4760. (Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro, 26-Apr-2015.) (Avoid depending on this detail.) |
⊢ 〈𝐴, 𝐵〉 = {𝑥 ∣ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})} | ||
Syntax | cotp 4533 | Extend class notation to include ordered triple. |
class 〈𝐴, 𝐵, 𝐶〉 | ||
Definition | df-ot 4534 | Define ordered triple of classes. Definition of ordered triple in [Stoll] p. 25. (Contributed by NM, 3-Apr-2015.) |
⊢ 〈𝐴, 𝐵, 𝐶〉 = 〈〈𝐴, 𝐵〉, 𝐶〉 | ||
Theorem | sneq 4535 | Equality theorem for singletons. Part of Exercise 4 of [TakeutiZaring] p. 15. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵}) | ||
Theorem | sneqi 4536 | Equality inference for singletons. (Contributed by NM, 22-Jan-2004.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ {𝐴} = {𝐵} | ||
Theorem | sneqd 4537 | Equality deduction for singletons. (Contributed by NM, 22-Jan-2004.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → {𝐴} = {𝐵}) | ||
Theorem | dfsn2 4538 | Alternate definition of singleton. Definition 5.1 of [TakeutiZaring] p. 15. (Contributed by NM, 24-Apr-1994.) |
⊢ {𝐴} = {𝐴, 𝐴} | ||
Theorem | elsng 4539 | 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 4540 | There is exactly one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. (Contributed by NM, 13-Sep-1995.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵) | ||
Theorem | velsn 4541 | There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) | ||
Theorem | elsni 4542 | There is at most one element in a singleton. (Contributed by NM, 5-Jun-1994.) |
⊢ (𝐴 ∈ {𝐵} → 𝐴 = 𝐵) | ||
Theorem | absn 4543* | Condition for a class abstraction to be a singleton. Formerly part of proof of dfiota2 6284. (Contributed by Andrew Salmon, 30-Jun-2011.) (Revised by AV, 24-Aug-2022.) |
⊢ ({𝑥 ∣ 𝜑} = {𝑌} ↔ ∀𝑥(𝜑 ↔ 𝑥 = 𝑌)) | ||
Theorem | dfpr2 4544* | Alternate definition of a pair. Definition 5.1 of [TakeutiZaring] p. 15. (Contributed by NM, 24-Apr-1994.) |
⊢ {𝐴, 𝐵} = {𝑥 ∣ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵)} | ||
Theorem | dfsn2ALT 4545 | 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 4546 | 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 4547 | 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 4548 | 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 4549 | 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 4550 | 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 4551 | Obsolete version of elpr2 4550 as of 25-May-2024. (Contributed by NM, 14-Oct-2005.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)) | ||
Theorem | nelpr2 4552 | 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 4553 | 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 4554 | 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 4555 | 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 4556 | 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 4557 | Membership in a set with two elements removed. Similar to eldifsn 4680 and eldiftp 4584. (Contributed by Mario Carneiro, 18-Jul-2017.) |
⊢ (𝐴 ∈ (𝐵 ∖ {𝐶, 𝐷}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷)) | ||
Theorem | rexdifpr 4558 | Restricted existential quantification over a set with two elements removed. (Contributed by Alexander van der Vekens, 7-Feb-2018.) |
⊢ (∃𝑥 ∈ (𝐴 ∖ {𝐵, 𝐶})𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝑥 ≠ 𝐵 ∧ 𝑥 ≠ 𝐶 ∧ 𝜑)) | ||
Theorem | snidg 4559 | 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 4560 | A class is a set iff it is a member of its singleton. (Contributed by NM, 5-Apr-2004.) |
⊢ (𝐴 ∈ V ↔ 𝐴 ∈ {𝐴}) | ||
Theorem | snid 4561 | 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 4562 | A setvar variable is a member of its singleton. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 𝑥 ∈ {𝑥} | ||
Theorem | elsn2g 4563 | 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 4564 | 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 4565 | 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 4566* | 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 4567* | 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 | ralsnsg 4568* | Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.) |
⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ [𝐴 / 𝑥]𝜑)) | ||
Theorem | rexsns 4569* | Restricted existential quantification over a singleton. (Contributed by Mario Carneiro, 23-Apr-2015.) (Revised by NM, 22-Aug-2018.) |
⊢ (∃𝑥 ∈ {𝐴}𝜑 ↔ [𝐴 / 𝑥]𝜑) | ||
Theorem | rexsngf 4570* | Restricted existential quantification over a singleton. (Contributed by NM, 29-Jan-2012.) (Revised by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) | ||
Theorem | ralsngf 4571* | Restricted universal quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by AV, 3-Apr-2023.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) | ||
Theorem | reusngf 4572* | Restricted existential uniqueness over a singleton. (Contributed by AV, 3-Apr-2023.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∃!𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) | ||
Theorem | ralsng 4573* | Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.) (Proof shortened by AV, 7-Apr-2023.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) | ||
Theorem | rexsng 4574* | Restricted existential quantification over a singleton. (Contributed by NM, 29-Jan-2012.) (Proof shortened by AV, 7-Apr-2023.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) | ||
Theorem | reusng 4575* | Restricted existential uniqueness over a singleton. (Contributed by AV, 3-Apr-2023.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∃!𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) | ||
Theorem | 2ralsng 4576* | Substitution expressed in terms of two quantifications over singletons. (Contributed by AV, 22-Dec-2019.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ {𝐴}∀𝑦 ∈ {𝐵}𝜑 ↔ 𝜒)) | ||
Theorem | rexreusng 4577* | Restricted existential uniqueness over a singleton is equivalent to a restricted existential quantification over a singleton. (Contributed by AV, 3-Apr-2023.) |
⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}𝜑 ↔ ∃!𝑥 ∈ {𝐴}𝜑)) | ||
Theorem | exsnrex 4578 | 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 4579* | Convert a universal quantification restricted to a singleton to a substitution. (Contributed by NM, 27-Apr-2009.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓) | ||
Theorem | rexsn 4580* | Convert an existential quantification restricted to a singleton to a substitution. (Contributed by Jeff Madsen, 5-Jan-2011.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓) | ||
Theorem | elpwunsn 4581 | Membership in an extension of a power class. (Contributed by NM, 26-Mar-2007.) |
⊢ (𝐴 ∈ (𝒫 (𝐵 ∪ {𝐶}) ∖ 𝒫 𝐵) → 𝐶 ∈ 𝐴) | ||
Theorem | eqoreldif 4582 | 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 4583 | Members of an unordered triple of classes. (Contributed by FL, 2-Feb-2014.) (Proof shortened by Mario Carneiro, 11-Feb-2015.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵, 𝐶, 𝐷} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ∨ 𝐴 = 𝐷))) | ||
Theorem | eldiftp 4584 | Membership in a set with three elements removed. Similar to eldifsn 4680 and eldifpr 4557. (Contributed by David A. Wheeler, 22-Jul-2017.) |
⊢ (𝐴 ∈ (𝐵 ∖ {𝐶, 𝐷, 𝐸}) ↔ (𝐴 ∈ 𝐵 ∧ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ∧ 𝐴 ≠ 𝐸))) | ||
Theorem | eltpi 4585 | A member of an unordered triple of classes is one of them. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ (𝐴 ∈ {𝐵, 𝐶, 𝐷} → (𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ∨ 𝐴 = 𝐷)) | ||
Theorem | eltp 4586 | 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 4587* | 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 4588 | Bound-variable hypothesis builder for unordered pairs. (Contributed by NM, 14-Nov-1995.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥{𝐴, 𝐵} | ||
Theorem | ifpr 4589 | Membership of a conditional operator in an unordered pair. (Contributed by NM, 17-Jun-2007.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → if(𝜑, 𝐴, 𝐵) ∈ {𝐴, 𝐵}) | ||
Theorem | ralprgf 4590* | Convert a restricted universal quantification over a pair to a conjunction, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 17-Sep-2011.) (Revised by AV, 8-Apr-2023.) |
⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑥𝜒 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒))) | ||
Theorem | rexprgf 4591* | Convert a restricted existential quantification over a pair to a disjunction, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 17-Sep-2011.) (Revised by AV, 2-Apr-2023.) |
⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑥𝜒 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∨ 𝜒))) | ||
Theorem | ralprg 4592* | Convert a restricted universal quantification over a pair to a conjunction. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.) (Proof shortened by AV, 8-Apr-2023.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒))) | ||
Theorem | rexprg 4593* | Convert a restricted existential quantification over a pair to a disjunction. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.) (Proof shortened by AV, 8-Apr-2023.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∨ 𝜒))) | ||
Theorem | raltpg 4594* | Convert a restricted universal quantification over a triple to a conjunction. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜃)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (∀𝑥 ∈ {𝐴, 𝐵, 𝐶}𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))) | ||
Theorem | rextpg 4595* | Convert a restricted existential quantification over a triple to a disjunction. (Contributed by Mario Carneiro, 23-Apr-2015.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜃)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (∃𝑥 ∈ {𝐴, 𝐵, 𝐶}𝜑 ↔ (𝜓 ∨ 𝜒 ∨ 𝜃))) | ||
Theorem | ralpr 4596* | Convert a restricted universal quantification over a pair to a conjunction. (Contributed by NM, 3-Jun-2007.) (Revised by Mario Carneiro, 23-Apr-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) ⇒ ⊢ (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒)) | ||
Theorem | rexpr 4597* | Convert a restricted existential quantification over a pair to a disjunction. (Contributed by NM, 3-Jun-2007.) (Revised by Mario Carneiro, 23-Apr-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) ⇒ ⊢ (∃𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∨ 𝜒)) | ||
Theorem | reuprg0 4598* | Convert a restricted existential uniqueness over a pair to a disjunction of conjunctions. (Contributed by AV, 2-Apr-2023.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃!𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ ((𝜓 ∧ (𝜒 → 𝐴 = 𝐵)) ∨ (𝜒 ∧ (𝜓 → 𝐴 = 𝐵))))) | ||
Theorem | reuprg 4599* | Convert a restricted existential uniqueness over a pair to a disjunction and an implication . (Contributed by AV, 2-Apr-2023.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃!𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ ((𝜓 ∨ 𝜒) ∧ ((𝜒 ∧ 𝜓) → 𝐴 = 𝐵)))) | ||
Theorem | reurexprg 4600* | Convert a restricted existential uniqueness over a pair to a restricted existential quantification and an implication . (Contributed by AV, 3-Apr-2023.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃!𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (∃𝑥 ∈ {𝐴, 𝐵}𝜑 ∧ ((𝜒 ∧ 𝜓) → 𝐴 = 𝐵)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |