![]() |
Metamath
Proof Explorer Theorem List (p. 48 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: | ![]() (1-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | snssi 4701 | The singleton of an element of a class is a subset of the class. (Contributed by NM, 6-Jun-1994.) |
⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵) | ||
Theorem | snssd 4702 | The singleton of an element of a class is a subset of the class (deduction form). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → {𝐴} ⊆ 𝐵) | ||
Theorem | difsnid 4703 | If we remove a single element from a class then put it back in, we end up with the original class. (Contributed by NM, 2-Oct-2006.) |
⊢ (𝐵 ∈ 𝐴 → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴) | ||
Theorem | eldifeldifsn 4704 | An element of a difference set is an element of the difference with a singleton. (Contributed by AV, 2-Jan-2022.) |
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ (𝐵 ∖ 𝐴)) → 𝑌 ∈ (𝐵 ∖ {𝑋})) | ||
Theorem | pw0 4705 | Compute the power set of the empty set. Theorem 89 of [Suppes] p. 47. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ 𝒫 ∅ = {∅} | ||
Theorem | pwpw0 4706 | Compute the power set of the power set of the empty set. (See pw0 4705 for the power set of the empty set.) Theorem 90 of [Suppes] p. 48. Although this theorem is a special case of pwsn 4792, we have chosen to show a direct elementary proof. (Contributed by NM, 7-Aug-1994.) |
⊢ 𝒫 {∅} = {∅, {∅}} | ||
Theorem | snsspr1 4707 | A singleton is a subset of an unordered pair containing its member. (Contributed by NM, 27-Aug-2004.) |
⊢ {𝐴} ⊆ {𝐴, 𝐵} | ||
Theorem | snsspr2 4708 | A singleton is a subset of an unordered pair containing its member. (Contributed by NM, 2-May-2009.) |
⊢ {𝐵} ⊆ {𝐴, 𝐵} | ||
Theorem | snsstp1 4709 | A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013.) |
⊢ {𝐴} ⊆ {𝐴, 𝐵, 𝐶} | ||
Theorem | snsstp2 4710 | A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013.) |
⊢ {𝐵} ⊆ {𝐴, 𝐵, 𝐶} | ||
Theorem | snsstp3 4711 | A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013.) |
⊢ {𝐶} ⊆ {𝐴, 𝐵, 𝐶} | ||
Theorem | prssg 4712 | A pair of elements of a class is a subset of the class. Theorem 7.5 of [Quine] p. 49. (Contributed by NM, 22-Mar-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶)) | ||
Theorem | prss 4713 | A pair of elements of a class is a subset of the class. Theorem 7.5 of [Quine] p. 49. (Contributed by NM, 30-May-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) (Proof shortened by JJ, 23-Jul-2021.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶) | ||
Theorem | prssi 4714 | A pair of elements of a class is a subset of the class. (Contributed by NM, 16-Jan-2015.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → {𝐴, 𝐵} ⊆ 𝐶) | ||
Theorem | prssd 4715 | Deduction version of prssi 4714: A pair of elements of a class is a subset of the class. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ (𝜑 → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → {𝐴, 𝐵} ⊆ 𝐶) | ||
Theorem | prsspwg 4716 | An unordered pair belongs to the power class of a class iff each member belongs to the class. (Contributed by Thierry Arnoux, 3-Oct-2016.) (Revised by NM, 18-Jan-2018.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴, 𝐵} ⊆ 𝒫 𝐶 ↔ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶))) | ||
Theorem | ssprss 4717 | A pair as subset of a pair. (Contributed by AV, 26-Oct-2020.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴, 𝐵} ⊆ {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷)))) | ||
Theorem | ssprsseq 4718 | A proper pair is a subset of a pair iff it is equal to the superset. (Contributed by AV, 26-Oct-2020.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ({𝐴, 𝐵} ⊆ {𝐶, 𝐷} ↔ {𝐴, 𝐵} = {𝐶, 𝐷})) | ||
Theorem | sssn 4719 | The subsets of a singleton. (Contributed by NM, 24-Apr-2004.) |
⊢ (𝐴 ⊆ {𝐵} ↔ (𝐴 = ∅ ∨ 𝐴 = {𝐵})) | ||
Theorem | ssunsn2 4720 | The property of being sandwiched between two sets naturally splits under union with a singleton. This is the induction hypothesis for the determination of large powersets such as pwtp 4795. (Contributed by Mario Carneiro, 2-Jul-2016.) |
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷})) ↔ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶) ∨ ((𝐵 ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷})))) | ||
Theorem | ssunsn 4721 | Possible values for a set sandwiched between another set and it plus a singleton. (Contributed by Mario Carneiro, 2-Jul-2016.) |
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐵 ∪ {𝐶})) ↔ (𝐴 = 𝐵 ∨ 𝐴 = (𝐵 ∪ {𝐶}))) | ||
Theorem | eqsn 4722* | Two ways to express that a nonempty set equals a singleton. (Contributed by NM, 15-Dec-2007.) (Proof shortened by JJ, 23-Jul-2021.) |
⊢ (𝐴 ≠ ∅ → (𝐴 = {𝐵} ↔ ∀𝑥 ∈ 𝐴 𝑥 = 𝐵)) | ||
Theorem | issn 4723* | A sufficient condition for a (nonempty) set to be a singleton. (Contributed by AV, 20-Sep-2020.) |
⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 = 𝑦 → ∃𝑧 𝐴 = {𝑧}) | ||
Theorem | n0snor2el 4724* | A nonempty set is either a singleton or contains at least two different elements. (Contributed by AV, 20-Sep-2020.) |
⊢ (𝐴 ≠ ∅ → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 ∨ ∃𝑧 𝐴 = {𝑧})) | ||
Theorem | ssunpr 4725 | Possible values for a set sandwiched between another set and it plus a singleton. (Contributed by Mario Carneiro, 2-Jul-2016.) |
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐵 ∪ {𝐶, 𝐷})) ↔ ((𝐴 = 𝐵 ∨ 𝐴 = (𝐵 ∪ {𝐶})) ∨ (𝐴 = (𝐵 ∪ {𝐷}) ∨ 𝐴 = (𝐵 ∪ {𝐶, 𝐷})))) | ||
Theorem | sspr 4726 | The subsets of a pair. (Contributed by NM, 16-Mar-2006.) (Proof shortened by Mario Carneiro, 2-Jul-2016.) |
⊢ (𝐴 ⊆ {𝐵, 𝐶} ↔ ((𝐴 = ∅ ∨ 𝐴 = {𝐵}) ∨ (𝐴 = {𝐶} ∨ 𝐴 = {𝐵, 𝐶}))) | ||
Theorem | sstp 4727 | The subsets of an unordered triple. (Contributed by Mario Carneiro, 2-Jul-2016.) |
⊢ (𝐴 ⊆ {𝐵, 𝐶, 𝐷} ↔ (((𝐴 = ∅ ∨ 𝐴 = {𝐵}) ∨ (𝐴 = {𝐶} ∨ 𝐴 = {𝐵, 𝐶})) ∨ ((𝐴 = {𝐷} ∨ 𝐴 = {𝐵, 𝐷}) ∨ (𝐴 = {𝐶, 𝐷} ∨ 𝐴 = {𝐵, 𝐶, 𝐷})))) | ||
Theorem | tpss 4728 | An unordered triple of elements of a class is a subset of the class. (Contributed by NM, 9-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) ↔ {𝐴, 𝐵, 𝐶} ⊆ 𝐷) | ||
Theorem | tpssi 4729 | An unordered triple of elements of a class is a subset of the class. (Contributed by Alexander van der Vekens, 1-Feb-2018.) |
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) → {𝐴, 𝐵, 𝐶} ⊆ 𝐷) | ||
Theorem | sneqrg 4730 | Closed form of sneqr 4731. (Contributed by Scott Fenton, 1-Apr-2011.) (Proof shortened by JJ, 23-Jul-2021.) |
⊢ (𝐴 ∈ 𝑉 → ({𝐴} = {𝐵} → 𝐴 = 𝐵)) | ||
Theorem | sneqr 4731 | If the singletons of two sets are equal, the two sets are equal. Part of Exercise 4 of [TakeutiZaring] p. 15. (Contributed by NM, 27-Aug-1993.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ({𝐴} = {𝐵} → 𝐴 = 𝐵) | ||
Theorem | snsssn 4732 | If a singleton is a subset of another, their members are equal. (Contributed by NM, 28-May-2006.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ({𝐴} ⊆ {𝐵} → 𝐴 = 𝐵) | ||
Theorem | mosneq 4733* | There exists at most one set whose singleton is equal to a given class. See also moeq 3646. (Contributed by BJ, 24-Sep-2022.) |
⊢ ∃*𝑥{𝑥} = 𝐴 | ||
Theorem | sneqbg 4734 | Two singletons of sets are equal iff their elements are equal. (Contributed by Scott Fenton, 16-Apr-2012.) |
⊢ (𝐴 ∈ 𝑉 → ({𝐴} = {𝐵} ↔ 𝐴 = 𝐵)) | ||
Theorem | snsspw 4735 | The singleton of a class is a subset of its power class. (Contributed by NM, 21-Jun-1993.) |
⊢ {𝐴} ⊆ 𝒫 𝐴 | ||
Theorem | prsspw 4736 | An unordered pair belongs to the power class of a class iff each member belongs to the class. (Contributed by NM, 10-Dec-2003.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) (Proof shortened by OpenAI, 25-Mar-2020.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ({𝐴, 𝐵} ⊆ 𝒫 𝐶 ↔ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶)) | ||
Theorem | preq1b 4737 | Biconditional equality lemma for unordered pairs, deduction form. Two unordered pairs have the same second element iff the first elements are equal. (Contributed by AV, 18-Dec-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ({𝐴, 𝐶} = {𝐵, 𝐶} ↔ 𝐴 = 𝐵)) | ||
Theorem | preq2b 4738 | Biconditional equality lemma for unordered pairs, deduction form. Two unordered pairs have the same first element iff the second elements are equal. (Contributed by AV, 18-Dec-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ({𝐶, 𝐴} = {𝐶, 𝐵} ↔ 𝐴 = 𝐵)) | ||
Theorem | preqr1 4739 | Reverse equality lemma for unordered pairs. If two unordered pairs have the same second element, the first elements are equal. (Contributed by NM, 18-Oct-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ({𝐴, 𝐶} = {𝐵, 𝐶} → 𝐴 = 𝐵) | ||
Theorem | preqr2 4740 | Reverse equality lemma for unordered pairs. If two unordered pairs have the same first element, the second elements are equal. (Contributed by NM, 15-Jul-1993.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ({𝐶, 𝐴} = {𝐶, 𝐵} → 𝐴 = 𝐵) | ||
Theorem | preq12b 4741 | Equality relationship for two unordered pairs. (Contributed by NM, 17-Oct-1996.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))) | ||
Theorem | opthpr 4742 | An unordered pair has the ordered pair property (compare opth 5333) under certain conditions. (Contributed by NM, 27-Mar-2007.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ (𝐴 ≠ 𝐷 → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) | ||
Theorem | preqr1g 4743 | Reverse equality lemma for unordered pairs. If two unordered pairs have the same second element, the first elements are equal. Closed form of preqr1 4739. (Contributed by AV, 29-Jan-2021.) (Revised by AV, 18-Sep-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴, 𝐶} = {𝐵, 𝐶} → 𝐴 = 𝐵)) | ||
Theorem | preq12bg 4744 | Closed form of preq12b 4741. (Contributed by Scott Fenton, 28-Mar-2014.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))) | ||
Theorem | prneimg 4745 | Two pairs are not equal if at least one element of the first pair is not contained in the second pair. (Contributed by Alexander van der Vekens, 13-Aug-2017.) |
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → (((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∨ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)) → {𝐴, 𝐵} ≠ {𝐶, 𝐷})) | ||
Theorem | prnebg 4746 | A (proper) pair is not equal to another (maybe improper) pair if and only if an element of the first pair is not contained in the second pair. (Contributed by Alexander van der Vekens, 16-Jan-2018.) |
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) → (((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∨ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)) ↔ {𝐴, 𝐵} ≠ {𝐶, 𝐷})) | ||
Theorem | pr1eqbg 4747 | A (proper) pair is equal to another (maybe improper) pair containing one element of the first pair if and only if the other element of the first pair is contained in the second pair. (Contributed by Alexander van der Vekens, 26-Jan-2018.) |
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → (𝐴 = 𝐶 ↔ {𝐴, 𝐵} = {𝐵, 𝐶})) | ||
Theorem | pr1nebg 4748 | A (proper) pair is not equal to another (maybe improper) pair containing one element of the first pair if and only if the other element of the first pair is not contained in the second pair. (Contributed by Alexander van der Vekens, 26-Jan-2018.) |
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → (𝐴 ≠ 𝐶 ↔ {𝐴, 𝐵} ≠ {𝐵, 𝐶})) | ||
Theorem | preqsnd 4749 | Equivalence for a pair equal to a singleton, deduction form. (Contributed by Thierry Arnoux, 27-Dec-2016.) (Revised by AV, 13-Jun-2022.) |
⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) ⇒ ⊢ (𝜑 → ({𝐴, 𝐵} = {𝐶} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶))) | ||
Theorem | prnesn 4750 | A proper unordered pair is not a (proper or improper) singleton. (Contributed by AV, 13-Jun-2022.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ≠ {𝐶}) | ||
Theorem | prneprprc 4751 | A proper unordered pair is not an improper unordered pair. (Contributed by AV, 13-Jun-2022.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ ¬ 𝐶 ∈ V) → {𝐴, 𝐵} ≠ {𝐶, 𝐷}) | ||
Theorem | preqsn 4752 | Equivalence for a pair equal to a singleton. (Contributed by NM, 3-Jun-2008.) (Revised by AV, 12-Jun-2022.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ({𝐴, 𝐵} = {𝐶} ↔ (𝐴 = 𝐵 ∧ 𝐵 = 𝐶)) | ||
Theorem | preq12nebg 4753 | Equality relationship for two proper unordered pairs. (Contributed by AV, 12-Jun-2022.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))) | ||
Theorem | prel12g 4754 | Equality of two unordered pairs. (Contributed by NM, 17-Oct-1996.) (Revised by AV, 9-Dec-2018.) (Revised by AV, 12-Jun-2022.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ (𝐴 ∈ {𝐶, 𝐷} ∧ 𝐵 ∈ {𝐶, 𝐷}))) | ||
Theorem | opthprneg 4755 | An unordered pair has the ordered pair property (compare opth 5333) under certain conditions. Variant of opthpr 4742 in closed form. (Contributed by AV, 13-Jun-2022.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐷)) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) | ||
Theorem | elpreqprlem 4756* | Lemma for elpreqpr 4757. (Contributed by Scott Fenton, 7-Dec-2020.) (Revised by AV, 9-Dec-2020.) |
⊢ (𝐵 ∈ 𝑉 → ∃𝑥{𝐵, 𝐶} = {𝐵, 𝑥}) | ||
Theorem | elpreqpr 4757* | Equality and membership rule for pairs. (Contributed by Scott Fenton, 7-Dec-2020.) |
⊢ (𝐴 ∈ {𝐵, 𝐶} → ∃𝑥{𝐵, 𝐶} = {𝐴, 𝑥}) | ||
Theorem | elpreqprb 4758* | A set is an element of an unordered pair iff there is another (maybe the same) set which is an element of the unordered pair. (Proposed by BJ, 8-Dec-2020.) (Contributed by AV, 9-Dec-2020.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵, 𝐶} ↔ ∃𝑥{𝐵, 𝐶} = {𝐴, 𝑥})) | ||
Theorem | elpr2elpr 4759* | For an element 𝐴 of an unordered pair which is a subset of a given set 𝑉, there is another (maybe the same) element 𝑏 of the given set 𝑉 being an element of the unordered pair. (Contributed by AV, 5-Dec-2020.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝐴 ∈ {𝑋, 𝑌}) → ∃𝑏 ∈ 𝑉 {𝑋, 𝑌} = {𝐴, 𝑏}) | ||
Theorem | dfopif 4760 | Rewrite df-op 4532 using if. When both arguments are sets, it reduces to the standard Kuratowski definition; otherwise, it is defined to be the empty set. Avoid directly depending on this detail so that theorems will not depend on the Kuratowski construction. (Contributed by Mario Carneiro, 26-Apr-2015.) (Avoid depending on this detail.) |
⊢ 〈𝐴, 𝐵〉 = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅) | ||
Theorem | dfopg 4761 | Value of the ordered pair when the arguments are sets. (Contributed by Mario Carneiro, 26-Apr-2015.) (Avoid depending on this detail.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 〈𝐴, 𝐵〉 = {{𝐴}, {𝐴, 𝐵}}) | ||
Theorem | dfop 4762 | Value of an ordered pair when the arguments are sets, with the conclusion corresponding to Kuratowski's original definition. (Contributed by NM, 25-Jun-1998.) (Avoid depending on this detail.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ 〈𝐴, 𝐵〉 = {{𝐴}, {𝐴, 𝐵}} | ||
Theorem | opeq1 4763 | Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.) Avoid ax-10 2142, ax-11 2158, ax-12 2175. (Revised by Gino Giotto, 26-May-2024.) |
⊢ (𝐴 = 𝐵 → 〈𝐴, 𝐶〉 = 〈𝐵, 𝐶〉) | ||
Theorem | opeq1OLD 4764 | Obsolete version of opeq1 4763 as of 25-May-2024. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 = 𝐵 → 〈𝐴, 𝐶〉 = 〈𝐵, 𝐶〉) | ||
Theorem | opeq2 4765 | Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.) Avoid ax-10 2142, ax-11 2158, ax-12 2175. (Revised by Gino Giotto, 26-May-2024.) |
⊢ (𝐴 = 𝐵 → 〈𝐶, 𝐴〉 = 〈𝐶, 𝐵〉) | ||
Theorem | opeq2OLD 4766 | Obsolete version of opeq2 4765 as of 25-May-2024. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 = 𝐵 → 〈𝐶, 𝐴〉 = 〈𝐶, 𝐵〉) | ||
Theorem | opeq12 4767 | Equality theorem for ordered pairs. (Contributed by NM, 28-May-1995.) |
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → 〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉) | ||
Theorem | opeq1i 4768 | Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ 〈𝐴, 𝐶〉 = 〈𝐵, 𝐶〉 | ||
Theorem | opeq2i 4769 | Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ 〈𝐶, 𝐴〉 = 〈𝐶, 𝐵〉 | ||
Theorem | opeq12i 4770 | Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.) (Proof shortened by Eric Schmidt, 4-Apr-2007.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ 〈𝐴, 𝐶〉 = 〈𝐵, 𝐷〉 | ||
Theorem | opeq1d 4771 | Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 〈𝐴, 𝐶〉 = 〈𝐵, 𝐶〉) | ||
Theorem | opeq2d 4772 | Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 〈𝐶, 𝐴〉 = 〈𝐶, 𝐵〉) | ||
Theorem | opeq12d 4773 | Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → 〈𝐴, 𝐶〉 = 〈𝐵, 𝐷〉) | ||
Theorem | oteq1 4774 | Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015.) |
⊢ (𝐴 = 𝐵 → 〈𝐴, 𝐶, 𝐷〉 = 〈𝐵, 𝐶, 𝐷〉) | ||
Theorem | oteq2 4775 | Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015.) |
⊢ (𝐴 = 𝐵 → 〈𝐶, 𝐴, 𝐷〉 = 〈𝐶, 𝐵, 𝐷〉) | ||
Theorem | oteq3 4776 | Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015.) |
⊢ (𝐴 = 𝐵 → 〈𝐶, 𝐷, 𝐴〉 = 〈𝐶, 𝐷, 𝐵〉) | ||
Theorem | oteq1d 4777 | Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 〈𝐴, 𝐶, 𝐷〉 = 〈𝐵, 𝐶, 𝐷〉) | ||
Theorem | oteq2d 4778 | Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 〈𝐶, 𝐴, 𝐷〉 = 〈𝐶, 𝐵, 𝐷〉) | ||
Theorem | oteq3d 4779 | Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 〈𝐶, 𝐷, 𝐴〉 = 〈𝐶, 𝐷, 𝐵〉) | ||
Theorem | oteq123d 4780 | Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) & ⊢ (𝜑 → 𝐸 = 𝐹) ⇒ ⊢ (𝜑 → 〈𝐴, 𝐶, 𝐸〉 = 〈𝐵, 𝐷, 𝐹〉) | ||
Theorem | nfop 4781 | Bound-variable hypothesis builder for ordered pairs. (Contributed by NM, 14-Nov-1995.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥〈𝐴, 𝐵〉 | ||
Theorem | nfopd 4782 | Deduction version of bound-variable hypothesis builder nfop 4781. This shows how the deduction version of a not-free theorem such as nfop 4781 can be created from the corresponding not-free inference theorem. (Contributed by NM, 4-Feb-2008.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥〈𝐴, 𝐵〉) | ||
Theorem | csbopg 4783 | Distribution of class substitution over ordered pairs. (Contributed by Drahflow, 25-Sep-2015.) (Revised by Mario Carneiro, 29-Oct-2015.) (Revised by ML, 25-Oct-2020.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌〈𝐶, 𝐷〉 = 〈⦋𝐴 / 𝑥⦌𝐶, ⦋𝐴 / 𝑥⦌𝐷〉) | ||
Theorem | opidg 4784 | The ordered pair 〈𝐴, 𝐴〉 in Kuratowski's representation. Closed form of opid 4785. (Contributed by Peter Mazsa, 22-Jul-2019.) (Avoid depending on this detail.) |
⊢ (𝐴 ∈ 𝑉 → 〈𝐴, 𝐴〉 = {{𝐴}}) | ||
Theorem | opid 4785 | The ordered pair 〈𝐴, 𝐴〉 in Kuratowski's representation. Inference form of opidg 4784. (Contributed by FL, 28-Dec-2011.) (Proof shortened by AV, 16-Feb-2022.) (Avoid depending on this detail.) |
⊢ 𝐴 ∈ V ⇒ ⊢ 〈𝐴, 𝐴〉 = {{𝐴}} | ||
Theorem | ralunsn 4786* | Restricted quantification over the union of a set and a singleton, using implicit substitution. (Contributed by Paul Chapman, 17-Nov-2012.) (Revised by Mario Carneiro, 23-Apr-2015.) |
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐵 ∈ 𝐶 → (∀𝑥 ∈ (𝐴 ∪ {𝐵})𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))) | ||
Theorem | 2ralunsn 4787* | Double restricted quantification over the union of a set and a singleton, using implicit substitution. (Contributed by Paul Chapman, 17-Nov-2012.) |
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝐵 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝐵 ∈ 𝐶 → (∀𝑥 ∈ (𝐴 ∪ {𝐵})∀𝑦 ∈ (𝐴 ∪ {𝐵})𝜑 ↔ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) ∧ (∀𝑦 ∈ 𝐴 𝜒 ∧ 𝜃)))) | ||
Theorem | opprc 4788 | Expansion of an ordered pair when either member is a proper class. (Contributed by Mario Carneiro, 26-Apr-2015.) |
⊢ (¬ (𝐴 ∈ V ∧ 𝐵 ∈ V) → 〈𝐴, 𝐵〉 = ∅) | ||
Theorem | opprc1 4789 | Expansion of an ordered pair when the first member is a proper class. See also opprc 4788. (Contributed by NM, 10-Apr-2004.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ (¬ 𝐴 ∈ V → 〈𝐴, 𝐵〉 = ∅) | ||
Theorem | opprc2 4790 | Expansion of an ordered pair when the second member is a proper class. See also opprc 4788. (Contributed by NM, 15-Nov-1994.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ (¬ 𝐵 ∈ V → 〈𝐴, 𝐵〉 = ∅) | ||
Theorem | oprcl 4791 | If an ordered pair has an element, then its arguments are sets. (Contributed by Mario Carneiro, 26-Apr-2015.) |
⊢ (𝐶 ∈ 〈𝐴, 𝐵〉 → (𝐴 ∈ V ∧ 𝐵 ∈ V)) | ||
Theorem | pwsn 4792 | The power set of a singleton. (Contributed by NM, 5-Jun-2006.) |
⊢ 𝒫 {𝐴} = {∅, {𝐴}} | ||
Theorem | pwsnOLD 4793 | Obsolete version of pwsn 4792 as of 14-Apr-2024. Note that the proof is essentially the same once one inlines sssn 4719 in the proof of pwsn 4792. (Contributed by NM, 5-Jun-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝒫 {𝐴} = {∅, {𝐴}} | ||
Theorem | pwpr 4794 | The power set of an unordered pair. (Contributed by NM, 1-May-2009.) |
⊢ 𝒫 {𝐴, 𝐵} = ({∅, {𝐴}} ∪ {{𝐵}, {𝐴, 𝐵}}) | ||
Theorem | pwtp 4795 | The power set of an unordered triple. (Contributed by Mario Carneiro, 2-Jul-2016.) |
⊢ 𝒫 {𝐴, 𝐵, 𝐶} = (({∅, {𝐴}} ∪ {{𝐵}, {𝐴, 𝐵}}) ∪ ({{𝐶}, {𝐴, 𝐶}} ∪ {{𝐵, 𝐶}, {𝐴, 𝐵, 𝐶}})) | ||
Theorem | pwpwpw0 4796 | Compute the power set of the power set of the power set of the empty set. (See also pw0 4705 and pwpw0 4706.) (Contributed by NM, 2-May-2009.) |
⊢ 𝒫 {∅, {∅}} = ({∅, {∅}} ∪ {{{∅}}, {∅, {∅}}}) | ||
Theorem | pwv 4797 |
The power class of the universe is the universe. Exercise 4.12(d) of
[Mendelson] p. 235.
The collection of all classes is of course larger than V, which is the collection of all sets. But 𝒫 V, being a class, cannot contain proper classes, so 𝒫 V is actually no larger than V. This fact is exploited in ncanth 7091. (Contributed by NM, 14-Sep-2003.) |
⊢ 𝒫 V = V | ||
Theorem | prproe 4798* | For an element of a proper unordered pair of elements of a class 𝑉, there is another (different) element of the class 𝑉 which is an element of the proper pair. (Contributed by AV, 18-Dec-2021.) |
⊢ ((𝐶 ∈ {𝐴, 𝐵} ∧ 𝐴 ≠ 𝐵 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → ∃𝑣 ∈ (𝑉 ∖ {𝐶})𝑣 ∈ {𝐴, 𝐵}) | ||
Theorem | 3elpr2eq 4799 | If there are three elements in a proper unordered pair, and two of them are different from the third one, the two must be equal. (Contributed by AV, 19-Dec-2021.) |
⊢ (((𝑋 ∈ {𝐴, 𝐵} ∧ 𝑌 ∈ {𝐴, 𝐵} ∧ 𝑍 ∈ {𝐴, 𝐵}) ∧ (𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋)) → 𝑌 = 𝑍) | ||
Syntax | cuni 4800 | Extend class notation to include the union of a class. Read: "union (of) 𝐴". |
class ∪ 𝐴 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |