Home | Metamath
Proof Explorer Theorem List (p. 48 of 449) | < 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-28689) |
Hilbert Space Explorer
(28690-30212) |
Users' Mathboxes
(30213-44900) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | tpid3g 4701 | Closed theorem form of tpid3 4702. (Contributed by Alan Sare, 24-Oct-2011.) (Proof shortened by JJ, 30-Apr-2021.) |
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ {𝐶, 𝐷, 𝐴}) | ||
Theorem | tpid3 4702 | One of the three elements of an unordered triple. (Contributed by NM, 7-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) (Proof shortened by JJ, 30-Apr-2021.) |
⊢ 𝐶 ∈ V ⇒ ⊢ 𝐶 ∈ {𝐴, 𝐵, 𝐶} | ||
Theorem | snnzg 4703 | The singleton of a set is not empty. (Contributed by NM, 14-Dec-2008.) |
⊢ (𝐴 ∈ 𝑉 → {𝐴} ≠ ∅) | ||
Theorem | snnz 4704 | The singleton of a set is not empty. (Contributed by NM, 10-Apr-1994.) |
⊢ 𝐴 ∈ V ⇒ ⊢ {𝐴} ≠ ∅ | ||
Theorem | prnz 4705 | A pair containing a set is not empty. (Contributed by NM, 9-Apr-1994.) |
⊢ 𝐴 ∈ V ⇒ ⊢ {𝐴, 𝐵} ≠ ∅ | ||
Theorem | prnzg 4706 | A pair containing a set is not empty. (Contributed by FL, 19-Sep-2011.) (Proof shortened by JJ, 23-Jul-2021.) |
⊢ (𝐴 ∈ 𝑉 → {𝐴, 𝐵} ≠ ∅) | ||
Theorem | tpnz 4707 | A triplet containing a set is not empty. (Contributed by NM, 10-Apr-1994.) |
⊢ 𝐴 ∈ V ⇒ ⊢ {𝐴, 𝐵, 𝐶} ≠ ∅ | ||
Theorem | tpnzd 4708 | A triplet containing a set is not empty. (Contributed by Thierry Arnoux, 8-Apr-2019.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → {𝐴, 𝐵, 𝐶} ≠ ∅) | ||
Theorem | raltpd 4709* | Convert a quantification over a triple to a conjunction. (Contributed by Thierry Arnoux, 8-Apr-2019.) |
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) & ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → (𝜓 ↔ 𝜃)) & ⊢ ((𝜑 ∧ 𝑥 = 𝐶) → (𝜓 ↔ 𝜏)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ {𝐴, 𝐵, 𝐶}𝜓 ↔ (𝜒 ∧ 𝜃 ∧ 𝜏))) | ||
Theorem | snssg 4710 | The singleton of an element of a class is a subset of the class (general form of snss 4711). Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 22-Jul-2001.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵)) | ||
Theorem | snss 4711 | The singleton of an element of a class is a subset of the class (inference form of snssg 4710). Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 21-Jun-1993.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵) | ||
Theorem | eldifsn 4712 | Membership in a set with an element removed. (Contributed by NM, 10-Oct-2007.) |
⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶)) | ||
Theorem | ssdifsn 4713 | Subset of a set with an element removed. (Contributed by Emmett Weisz, 7-Jul-2021.) (Proof shortened by JJ, 31-May-2022.) |
⊢ (𝐴 ⊆ (𝐵 ∖ {𝐶}) ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐶 ∈ 𝐴)) | ||
Theorem | elpwdifsn 4714 | A subset of a set is an element of the power set of the difference of the set with a singleton if the subset does not contain the singleton element. (Contributed by AV, 10-Jan-2020.) |
⊢ ((𝑆 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ∧ 𝐴 ∉ 𝑆) → 𝑆 ∈ 𝒫 (𝑉 ∖ {𝐴})) | ||
Theorem | eldifsni 4715 | Membership in a set with an element removed. (Contributed by NM, 10-Mar-2015.) |
⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) → 𝐴 ≠ 𝐶) | ||
Theorem | eldifsnneq 4716 | An element of a difference with a singleton is not equal to the element of that singleton. Note that (¬ 𝐴 ∈ {𝐶} → ¬ 𝐴 = 𝐶) need not hold if 𝐴 is a proper class. (Contributed by BJ, 18-Mar-2023.) (Proof shortened by Steven Nguyen, 1-Jun-2023.) |
⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) → ¬ 𝐴 = 𝐶) | ||
Theorem | eldifsnneqOLD 4717 | Obsolete version of eldifsnneq 4716 as of 1-Jun-2023. An element of a difference with a singleton is not equal to the element of that singleton. Note that (¬ 𝐴 ∈ {𝐶} → ¬ 𝐴 = 𝐶) need not hold if 𝐴 is a proper class. (Contributed by BJ, 18-Mar-2023.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) → ¬ 𝐴 = 𝐶) | ||
Theorem | neldifsn 4718 | The class 𝐴 is not in (𝐵 ∖ {𝐴}). (Contributed by David Moews, 1-May-2017.) |
⊢ ¬ 𝐴 ∈ (𝐵 ∖ {𝐴}) | ||
Theorem | neldifsnd 4719 | The class 𝐴 is not in (𝐵 ∖ {𝐴}). Deduction form. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → ¬ 𝐴 ∈ (𝐵 ∖ {𝐴})) | ||
Theorem | rexdifsn 4720 | Restricted existential quantification over a set with an element removed. (Contributed by NM, 4-Feb-2015.) |
⊢ (∃𝑥 ∈ (𝐴 ∖ {𝐵})𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝑥 ≠ 𝐵 ∧ 𝜑)) | ||
Theorem | raldifsni 4721 | Rearrangement of a property of a singleton difference. (Contributed by Stefan O'Rear, 27-Feb-2015.) |
⊢ (∀𝑥 ∈ (𝐴 ∖ {𝐵}) ¬ 𝜑 ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝐵)) | ||
Theorem | raldifsnb 4722* | Restricted universal quantification on a class difference with a singleton in terms of an implication. (Contributed by Alexander van der Vekens, 26-Jan-2018.) |
⊢ (∀𝑥 ∈ 𝐴 (𝑥 ≠ 𝑌 → 𝜑) ↔ ∀𝑥 ∈ (𝐴 ∖ {𝑌})𝜑) | ||
Theorem | eldifvsn 4723 | A set is an element of the universal class excluding a singleton iff it is not the singleton element. (Contributed by AV, 7-Apr-2019.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ (V ∖ {𝐵}) ↔ 𝐴 ≠ 𝐵)) | ||
Theorem | difsn 4724 | An element not in a set can be removed without affecting the set. (Contributed by NM, 16-Mar-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ (¬ 𝐴 ∈ 𝐵 → (𝐵 ∖ {𝐴}) = 𝐵) | ||
Theorem | difprsnss 4725 | Removal of a singleton from an unordered pair. (Contributed by NM, 16-Mar-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ ({𝐴, 𝐵} ∖ {𝐴}) ⊆ {𝐵} | ||
Theorem | difprsn1 4726 | Removal of a singleton from an unordered pair. (Contributed by Thierry Arnoux, 4-Feb-2017.) |
⊢ (𝐴 ≠ 𝐵 → ({𝐴, 𝐵} ∖ {𝐴}) = {𝐵}) | ||
Theorem | difprsn2 4727 | Removal of a singleton from an unordered pair. (Contributed by Alexander van der Vekens, 5-Oct-2017.) |
⊢ (𝐴 ≠ 𝐵 → ({𝐴, 𝐵} ∖ {𝐵}) = {𝐴}) | ||
Theorem | diftpsn3 4728 | Removal of a singleton from an unordered triple. (Contributed by Alexander van der Vekens, 5-Oct-2017.) (Proof shortened by JJ, 23-Jul-2021.) |
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = {𝐴, 𝐵}) | ||
Theorem | difpr 4729 | Removing two elements as pair of elements corresponds to removing each of the two elements as singletons. (Contributed by Alexander van der Vekens, 13-Jul-2018.) |
⊢ (𝐴 ∖ {𝐵, 𝐶}) = ((𝐴 ∖ {𝐵}) ∖ {𝐶}) | ||
Theorem | tpprceq3 4730 | An unordered triple is an unordered pair if one of its elements is a proper class or is identical with another element. (Contributed by Alexander van der Vekens, 6-Oct-2017.) |
⊢ (¬ (𝐶 ∈ V ∧ 𝐶 ≠ 𝐵) → {𝐴, 𝐵, 𝐶} = {𝐴, 𝐵}) | ||
Theorem | tppreqb 4731 | An unordered triple is an unordered pair if and only if one of its elements is a proper class or is identical with one of the another elements. (Contributed by Alexander van der Vekens, 15-Jan-2018.) |
⊢ (¬ (𝐶 ∈ V ∧ 𝐶 ≠ 𝐴 ∧ 𝐶 ≠ 𝐵) ↔ {𝐴, 𝐵, 𝐶} = {𝐴, 𝐵}) | ||
Theorem | difsnb 4732 | (𝐵 ∖ {𝐴}) equals 𝐵 if and only if 𝐴 is not a member of 𝐵. Generalization of difsn 4724. (Contributed by David Moews, 1-May-2017.) |
⊢ (¬ 𝐴 ∈ 𝐵 ↔ (𝐵 ∖ {𝐴}) = 𝐵) | ||
Theorem | difsnpss 4733 | (𝐵 ∖ {𝐴}) is a proper subclass of 𝐵 if and only if 𝐴 is a member of 𝐵. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝐴 ∈ 𝐵 ↔ (𝐵 ∖ {𝐴}) ⊊ 𝐵) | ||
Theorem | snssi 4734 | The singleton of an element of a class is a subset of the class. (Contributed by NM, 6-Jun-1994.) |
⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵) | ||
Theorem | snssd 4735 | 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 4736 | 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 4737 | An element of a difference set is an element of the difference with a singleton. (Contributed by AV, 2-Jan-2022.) |
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ (𝐵 ∖ 𝐴)) → 𝑌 ∈ (𝐵 ∖ {𝑋})) | ||
Theorem | pw0 4738 | 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 4739 | Compute the power set of the power set of the empty set. (See pw0 4738 for the power set of the empty set.) Theorem 90 of [Suppes] p. 48. Although this theorem is a special case of pwsn 4823, we have chosen to show a direct elementary proof. (Contributed by NM, 7-Aug-1994.) |
⊢ 𝒫 {∅} = {∅, {∅}} | ||
Theorem | snsspr1 4740 | A singleton is a subset of an unordered pair containing its member. (Contributed by NM, 27-Aug-2004.) |
⊢ {𝐴} ⊆ {𝐴, 𝐵} | ||
Theorem | snsspr2 4741 | A singleton is a subset of an unordered pair containing its member. (Contributed by NM, 2-May-2009.) |
⊢ {𝐵} ⊆ {𝐴, 𝐵} | ||
Theorem | snsstp1 4742 | A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013.) |
⊢ {𝐴} ⊆ {𝐴, 𝐵, 𝐶} | ||
Theorem | snsstp2 4743 | A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013.) |
⊢ {𝐵} ⊆ {𝐴, 𝐵, 𝐶} | ||
Theorem | snsstp3 4744 | A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013.) |
⊢ {𝐶} ⊆ {𝐴, 𝐵, 𝐶} | ||
Theorem | prssg 4745 | 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 4746 | 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 4747 | A pair of elements of a class is a subset of the class. (Contributed by NM, 16-Jan-2015.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → {𝐴, 𝐵} ⊆ 𝐶) | ||
Theorem | prssd 4748 | Deduction version of prssi 4747: A pair of elements of a class is a subset of the class. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ (𝜑 → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → {𝐴, 𝐵} ⊆ 𝐶) | ||
Theorem | prsspwg 4749 | 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 4750 | A pair as subset of a pair. (Contributed by AV, 26-Oct-2020.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴, 𝐵} ⊆ {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷)))) | ||
Theorem | ssprsseq 4751 | A proper pair is a subset of a pair iff it is equal to the superset. (Contributed by AV, 26-Oct-2020.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ({𝐴, 𝐵} ⊆ {𝐶, 𝐷} ↔ {𝐴, 𝐵} = {𝐶, 𝐷})) | ||
Theorem | sssn 4752 | The subsets of a singleton. (Contributed by NM, 24-Apr-2004.) |
⊢ (𝐴 ⊆ {𝐵} ↔ (𝐴 = ∅ ∨ 𝐴 = {𝐵})) | ||
Theorem | ssunsn2 4753 | 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 4826. (Contributed by Mario Carneiro, 2-Jul-2016.) |
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷})) ↔ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶) ∨ ((𝐵 ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷})))) | ||
Theorem | ssunsn 4754 | Possible values for a set sandwiched between another set and it plus a singleton. (Contributed by Mario Carneiro, 2-Jul-2016.) |
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐵 ∪ {𝐶})) ↔ (𝐴 = 𝐵 ∨ 𝐴 = (𝐵 ∪ {𝐶}))) | ||
Theorem | eqsn 4755* | 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 4756* | A sufficient condition for a (nonempty) set to be a singleton. (Contributed by AV, 20-Sep-2020.) |
⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 = 𝑦 → ∃𝑧 𝐴 = {𝑧}) | ||
Theorem | n0snor2el 4757* | A nonempty set is either a singleton or contains at least two different elements. (Contributed by AV, 20-Sep-2020.) |
⊢ (𝐴 ≠ ∅ → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 ∨ ∃𝑧 𝐴 = {𝑧})) | ||
Theorem | ssunpr 4758 | Possible values for a set sandwiched between another set and it plus a singleton. (Contributed by Mario Carneiro, 2-Jul-2016.) |
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐵 ∪ {𝐶, 𝐷})) ↔ ((𝐴 = 𝐵 ∨ 𝐴 = (𝐵 ∪ {𝐶})) ∨ (𝐴 = (𝐵 ∪ {𝐷}) ∨ 𝐴 = (𝐵 ∪ {𝐶, 𝐷})))) | ||
Theorem | sspr 4759 | The subsets of a pair. (Contributed by NM, 16-Mar-2006.) (Proof shortened by Mario Carneiro, 2-Jul-2016.) |
⊢ (𝐴 ⊆ {𝐵, 𝐶} ↔ ((𝐴 = ∅ ∨ 𝐴 = {𝐵}) ∨ (𝐴 = {𝐶} ∨ 𝐴 = {𝐵, 𝐶}))) | ||
Theorem | sstp 4760 | The subsets of a triple. (Contributed by Mario Carneiro, 2-Jul-2016.) |
⊢ (𝐴 ⊆ {𝐵, 𝐶, 𝐷} ↔ (((𝐴 = ∅ ∨ 𝐴 = {𝐵}) ∨ (𝐴 = {𝐶} ∨ 𝐴 = {𝐵, 𝐶})) ∨ ((𝐴 = {𝐷} ∨ 𝐴 = {𝐵, 𝐷}) ∨ (𝐴 = {𝐶, 𝐷} ∨ 𝐴 = {𝐵, 𝐶, 𝐷})))) | ||
Theorem | tpss 4761 | A triplet 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 4762 | A triple of elements of a class is a subset of the class. (Contributed by Alexander van der Vekens, 1-Feb-2018.) |
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) → {𝐴, 𝐵, 𝐶} ⊆ 𝐷) | ||
Theorem | sneqrg 4763 | Closed form of sneqr 4764. (Contributed by Scott Fenton, 1-Apr-2011.) (Proof shortened by JJ, 23-Jul-2021.) |
⊢ (𝐴 ∈ 𝑉 → ({𝐴} = {𝐵} → 𝐴 = 𝐵)) | ||
Theorem | sneqr 4764 | 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 4765 | If a singleton is a subset of another, their members are equal. (Contributed by NM, 28-May-2006.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ({𝐴} ⊆ {𝐵} → 𝐴 = 𝐵) | ||
Theorem | mosneq 4766* | There exists at most one set whose singleton is equal to a given class. See also moeq 3697. (Contributed by BJ, 24-Sep-2022.) |
⊢ ∃*𝑥{𝑥} = 𝐴 | ||
Theorem | sneqbg 4767 | Two singletons of sets are equal iff their elements are equal. (Contributed by Scott Fenton, 16-Apr-2012.) |
⊢ (𝐴 ∈ 𝑉 → ({𝐴} = {𝐵} ↔ 𝐴 = 𝐵)) | ||
Theorem | snsspw 4768 | The singleton of a class is a subset of its power class. (Contributed by NM, 21-Jun-1993.) |
⊢ {𝐴} ⊆ 𝒫 𝐴 | ||
Theorem | prsspw 4769 | 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 4770 | 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 4771 | 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 4772 | 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 4773 | 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 4774 | Equality relationship for two unordered pairs. (Contributed by NM, 17-Oct-1996.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))) | ||
Theorem | opthpr 4775 | An unordered pair has the ordered pair property (compare opth 5360) under certain conditions. (Contributed by NM, 27-Mar-2007.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ (𝐴 ≠ 𝐷 → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) | ||
Theorem | preqr1g 4776 | Reverse equality lemma for unordered pairs. If two unordered pairs have the same second element, the first elements are equal. Closed form of preqr1 4772. (Contributed by AV, 29-Jan-2021.) (Revised by AV, 18-Sep-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴, 𝐶} = {𝐵, 𝐶} → 𝐴 = 𝐵)) | ||
Theorem | preq12bg 4777 | Closed form of preq12b 4774. (Contributed by Scott Fenton, 28-Mar-2014.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))) | ||
Theorem | prneimg 4778 | 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 4779 | 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 4780 | 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 4781 | 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 4782 | 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 4783 | A proper unordered pair is not a (proper or improper) singleton. (Contributed by AV, 13-Jun-2022.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ≠ {𝐶}) | ||
Theorem | prneprprc 4784 | A proper unordered pair is not an improper unordered pair. (Contributed by AV, 13-Jun-2022.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ ¬ 𝐶 ∈ V) → {𝐴, 𝐵} ≠ {𝐶, 𝐷}) | ||
Theorem | preqsn 4785 | Equivalence for a pair equal to a singleton. (Contributed by NM, 3-Jun-2008.) (Revised by AV, 12-Jun-2022.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ({𝐴, 𝐵} = {𝐶} ↔ (𝐴 = 𝐵 ∧ 𝐵 = 𝐶)) | ||
Theorem | preq12nebg 4786 | Equality relationship for two proper unordered pairs. (Contributed by AV, 12-Jun-2022.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))) | ||
Theorem | prel12g 4787 | 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 4788 | An unordered pair has the ordered pair property (compare opth 5360) under certain conditions. Variant of opthpr 4775 in closed form. (Contributed by AV, 13-Jun-2022.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐷)) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) | ||
Theorem | elpreqprlem 4789* | Lemma for elpreqpr 4790. (Contributed by Scott Fenton, 7-Dec-2020.) (Revised by AV, 9-Dec-2020.) |
⊢ (𝐵 ∈ 𝑉 → ∃𝑥{𝐵, 𝐶} = {𝐵, 𝑥}) | ||
Theorem | elpreqpr 4790* | Equality and membership rule for pairs. (Contributed by Scott Fenton, 7-Dec-2020.) |
⊢ (𝐴 ∈ {𝐵, 𝐶} → ∃𝑥{𝐵, 𝐶} = {𝐴, 𝑥}) | ||
Theorem | elpreqprb 4791* | 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 4792* | 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 4793 | Rewrite df-op 4567 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 4794 | Value of the ordered pair when the arguments are sets. (Contributed by Mario Carneiro, 26-Apr-2015.) (Avoid depending on this detail.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 〈𝐴, 𝐵〉 = {{𝐴}, {𝐴, 𝐵}}) | ||
Theorem | dfop 4795 | 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 4796 | Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ (𝐴 = 𝐵 → 〈𝐴, 𝐶〉 = 〈𝐵, 𝐶〉) | ||
Theorem | opeq2 4797 | Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ (𝐴 = 𝐵 → 〈𝐶, 𝐴〉 = 〈𝐶, 𝐵〉) | ||
Theorem | opeq12 4798 | Equality theorem for ordered pairs. (Contributed by NM, 28-May-1995.) |
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → 〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉) | ||
Theorem | opeq1i 4799 | Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ 〈𝐴, 𝐶〉 = 〈𝐵, 𝐶〉 | ||
Theorem | opeq2i 4800 | Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ 〈𝐶, 𝐴〉 = 〈𝐶, 𝐵〉 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |