![]() |
Metamath
Proof Explorer Theorem List (p. 46 of 435) | < 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-28326) |
![]() (28327-29851) |
![]() (29852-43461) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | tpeq2d 4501 | Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → {𝐶, 𝐴, 𝐷} = {𝐶, 𝐵, 𝐷}) | ||
Theorem | tpeq3d 4502 | Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → {𝐶, 𝐷, 𝐴} = {𝐶, 𝐷, 𝐵}) | ||
Theorem | tpeq123d 4503 | Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) & ⊢ (𝜑 → 𝐸 = 𝐹) ⇒ ⊢ (𝜑 → {𝐴, 𝐶, 𝐸} = {𝐵, 𝐷, 𝐹}) | ||
Theorem | tprot 4504 | Rotation of the elements of an unordered triple. (Contributed by Alan Sare, 24-Oct-2011.) |
⊢ {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴} | ||
Theorem | tpcoma 4505 | Swap 1st and 2nd members of an unordered triple. (Contributed by NM, 22-May-2015.) |
⊢ {𝐴, 𝐵, 𝐶} = {𝐵, 𝐴, 𝐶} | ||
Theorem | tpcomb 4506 | Swap 2nd and 3rd members of an unordered triple. (Contributed by NM, 22-May-2015.) |
⊢ {𝐴, 𝐵, 𝐶} = {𝐴, 𝐶, 𝐵} | ||
Theorem | tpass 4507 | Split off the first element of an unordered triple. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ {𝐴, 𝐵, 𝐶} = ({𝐴} ∪ {𝐵, 𝐶}) | ||
Theorem | qdass 4508 | Two ways to write an unordered quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ ({𝐴, 𝐵} ∪ {𝐶, 𝐷}) = ({𝐴, 𝐵, 𝐶} ∪ {𝐷}) | ||
Theorem | qdassr 4509 | Two ways to write an unordered quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ ({𝐴, 𝐵} ∪ {𝐶, 𝐷}) = ({𝐴} ∪ {𝐵, 𝐶, 𝐷}) | ||
Theorem | tpidm12 4510 | Unordered triple {𝐴, 𝐴, 𝐵} is just an overlong way to write {𝐴, 𝐵}. (Contributed by David A. Wheeler, 10-May-2015.) |
⊢ {𝐴, 𝐴, 𝐵} = {𝐴, 𝐵} | ||
Theorem | tpidm13 4511 | Unordered triple {𝐴, 𝐵, 𝐴} is just an overlong way to write {𝐴, 𝐵}. (Contributed by David A. Wheeler, 10-May-2015.) |
⊢ {𝐴, 𝐵, 𝐴} = {𝐴, 𝐵} | ||
Theorem | tpidm23 4512 | Unordered triple {𝐴, 𝐵, 𝐵} is just an overlong way to write {𝐴, 𝐵}. (Contributed by David A. Wheeler, 10-May-2015.) |
⊢ {𝐴, 𝐵, 𝐵} = {𝐴, 𝐵} | ||
Theorem | tpidm 4513 | Unordered triple {𝐴, 𝐴, 𝐴} is just an overlong way to write {𝐴}. (Contributed by David A. Wheeler, 10-May-2015.) |
⊢ {𝐴, 𝐴, 𝐴} = {𝐴} | ||
Theorem | tppreq3 4514 | An unordered triple is an unordered pair if one of its elements is identical with another element. (Contributed by Alexander van der Vekens, 6-Oct-2017.) |
⊢ (𝐵 = 𝐶 → {𝐴, 𝐵, 𝐶} = {𝐴, 𝐵}) | ||
Theorem | prid1g 4515 | An unordered pair contains its first member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by Stefan Allan, 8-Nov-2008.) |
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐵}) | ||
Theorem | prid2g 4516 | An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by Stefan Allan, 8-Nov-2008.) |
⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ {𝐴, 𝐵}) | ||
Theorem | prid1 4517 | An unordered pair contains its first member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 24-Jun-1993.) |
⊢ 𝐴 ∈ V ⇒ ⊢ 𝐴 ∈ {𝐴, 𝐵} | ||
Theorem | prid2 4518 | An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Note: the proof from prid2g 4516 and ax-mp 5 has one fewer essential step but one more total step.) (Contributed by NM, 5-Aug-1993.) |
⊢ 𝐵 ∈ V ⇒ ⊢ 𝐵 ∈ {𝐴, 𝐵} | ||
Theorem | ifpprsnss 4519 | An unordered pair is a singleton or a subset of itself. This theorem is helpful to convert theorems about walks in arbitrary graphs into theorems about walks in pseudographs. (Contributed by AV, 27-Feb-2021.) |
⊢ (𝑃 = {𝐴, 𝐵} → if-(𝐴 = 𝐵, 𝑃 = {𝐴}, {𝐴, 𝐵} ⊆ 𝑃)) | ||
Theorem | prprc1 4520 | A proper class vanishes in an unordered pair. (Contributed by NM, 15-Jul-1993.) |
⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵}) | ||
Theorem | prprc2 4521 | A proper class vanishes in an unordered pair. (Contributed by NM, 22-Mar-2006.) |
⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴}) | ||
Theorem | prprc 4522 | An unordered pair containing two proper classes is the empty set. (Contributed by NM, 22-Mar-2006.) |
⊢ ((¬ 𝐴 ∈ V ∧ ¬ 𝐵 ∈ V) → {𝐴, 𝐵} = ∅) | ||
Theorem | tpid1 4523 | One of the three elements of an unordered triple. (Contributed by NM, 7-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ 𝐴 ∈ V ⇒ ⊢ 𝐴 ∈ {𝐴, 𝐵, 𝐶} | ||
Theorem | tpid1g 4524 | Closed theorem form of tpid1 4523. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ {𝐴, 𝐶, 𝐷}) | ||
Theorem | tpid2 4525 | One of the three elements of an unordered triple. (Contributed by NM, 7-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ 𝐵 ∈ V ⇒ ⊢ 𝐵 ∈ {𝐴, 𝐵, 𝐶} | ||
Theorem | tpid2g 4526 | Closed theorem form of tpid2 4525. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ {𝐶, 𝐴, 𝐷}) | ||
Theorem | tpid3g 4527 | Closed theorem form of tpid3 4528. (Contributed by Alan Sare, 24-Oct-2011.) (Proof shortened by JJ, 30-Apr-2021.) |
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ {𝐶, 𝐷, 𝐴}) | ||
Theorem | tpid3 4528 | 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 4529 | The singleton of a set is not empty. (Contributed by NM, 14-Dec-2008.) |
⊢ (𝐴 ∈ 𝑉 → {𝐴} ≠ ∅) | ||
Theorem | snnz 4530 | The singleton of a set is not empty. (Contributed by NM, 10-Apr-1994.) |
⊢ 𝐴 ∈ V ⇒ ⊢ {𝐴} ≠ ∅ | ||
Theorem | prnz 4531 | A pair containing a set is not empty. (Contributed by NM, 9-Apr-1994.) |
⊢ 𝐴 ∈ V ⇒ ⊢ {𝐴, 𝐵} ≠ ∅ | ||
Theorem | prnzg 4532 | A pair containing a set is not empty. (Contributed by FL, 19-Sep-2011.) (Proof shortened by JJ, 23-Jul-2021.) |
⊢ (𝐴 ∈ 𝑉 → {𝐴, 𝐵} ≠ ∅) | ||
Theorem | tpnz 4533 | A triplet containing a set is not empty. (Contributed by NM, 10-Apr-1994.) |
⊢ 𝐴 ∈ V ⇒ ⊢ {𝐴, 𝐵, 𝐶} ≠ ∅ | ||
Theorem | tpnzd 4534 | A triplet containing a set is not empty. (Contributed by Thierry Arnoux, 8-Apr-2019.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → {𝐴, 𝐵, 𝐶} ≠ ∅) | ||
Theorem | raltpd 4535* | Convert a quantification over a triple to a conjunction. (Contributed by Thierry Arnoux, 8-Apr-2019.) |
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) & ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → (𝜓 ↔ 𝜃)) & ⊢ ((𝜑 ∧ 𝑥 = 𝐶) → (𝜓 ↔ 𝜏)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ {𝐴, 𝐵, 𝐶}𝜓 ↔ (𝜒 ∧ 𝜃 ∧ 𝜏))) | ||
Theorem | snssg 4536 | The singleton of an element of a class is a subset of the class (general form of snss 4537). Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 22-Jul-2001.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵)) | ||
Theorem | snss 4537 | The singleton of an element of a class is a subset of the class (inference form of snssg 4536). Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 21-Jun-1993.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵) | ||
Theorem | eldifsn 4538 | Membership in a set with an element removed. (Contributed by NM, 10-Oct-2007.) |
⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶)) | ||
Theorem | ssdifsn 4539 | Subset of a set with an element removed. (Contributed by Emmett Weisz, 7-Jul-2021.) (Proof shortened by JJ, 31-May-2022.) |
⊢ (𝐴 ⊆ (𝐵 ∖ {𝐶}) ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐶 ∈ 𝐴)) | ||
Theorem | ssdifsnOLD 4540 | Obsolete proof of ssdifsn 4539 as of 31-May-2022. (Contributed by Emmett Weisz, 7-Jul-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐴 ⊆ (𝐵 ∖ {𝐶}) ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐶 ∈ 𝐴)) | ||
Theorem | elpwdifsn 4541 | 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 4542 | Membership in a set with an element removed. (Contributed by NM, 10-Mar-2015.) |
⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) → 𝐴 ≠ 𝐶) | ||
Theorem | neldifsn 4543 | The class 𝐴 is not in (𝐵 ∖ {𝐴}). (Contributed by David Moews, 1-May-2017.) |
⊢ ¬ 𝐴 ∈ (𝐵 ∖ {𝐴}) | ||
Theorem | neldifsnd 4544 | The class 𝐴 is not in (𝐵 ∖ {𝐴}). Deduction form. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → ¬ 𝐴 ∈ (𝐵 ∖ {𝐴})) | ||
Theorem | rexdifsn 4545 | Restricted existential quantification over a set with an element removed. (Contributed by NM, 4-Feb-2015.) |
⊢ (∃𝑥 ∈ (𝐴 ∖ {𝐵})𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝑥 ≠ 𝐵 ∧ 𝜑)) | ||
Theorem | raldifsni 4546 | Rearrangement of a property of a singleton difference. (Contributed by Stefan O'Rear, 27-Feb-2015.) |
⊢ (∀𝑥 ∈ (𝐴 ∖ {𝐵}) ¬ 𝜑 ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝐵)) | ||
Theorem | raldifsnb 4547* | 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 4548 | 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 4549 | 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 4550 | Removal of a singleton from an unordered pair. (Contributed by NM, 16-Mar-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ ({𝐴, 𝐵} ∖ {𝐴}) ⊆ {𝐵} | ||
Theorem | difprsn1 4551 | Removal of a singleton from an unordered pair. (Contributed by Thierry Arnoux, 4-Feb-2017.) |
⊢ (𝐴 ≠ 𝐵 → ({𝐴, 𝐵} ∖ {𝐴}) = {𝐵}) | ||
Theorem | difprsn2 4552 | Removal of a singleton from an unordered pair. (Contributed by Alexander van der Vekens, 5-Oct-2017.) |
⊢ (𝐴 ≠ 𝐵 → ({𝐴, 𝐵} ∖ {𝐵}) = {𝐴}) | ||
Theorem | diftpsn3 4553 | 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 4554 | 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 4555 | 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 4556 | 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 4557 | (𝐵 ∖ {𝐴}) equals 𝐵 if and only if 𝐴 is not a member of 𝐵. Generalization of difsn 4549. (Contributed by David Moews, 1-May-2017.) |
⊢ (¬ 𝐴 ∈ 𝐵 ↔ (𝐵 ∖ {𝐴}) = 𝐵) | ||
Theorem | difsnpss 4558 | (𝐵 ∖ {𝐴}) is a proper subclass of 𝐵 if and only if 𝐴 is a member of 𝐵. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝐴 ∈ 𝐵 ↔ (𝐵 ∖ {𝐴}) ⊊ 𝐵) | ||
Theorem | snssi 4559 | The singleton of an element of a class is a subset of the class. (Contributed by NM, 6-Jun-1994.) |
⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵) | ||
Theorem | snssd 4560 | 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 4561 | 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 4562 | An element of a difference set is an element of the difference with a singleton. (Contributed by AV, 2-Jan-2022.) |
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ (𝐵 ∖ 𝐴)) → 𝑌 ∈ (𝐵 ∖ {𝑋})) | ||
Theorem | pw0 4563 | 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 4564 | Compute the power set of the power set of the empty set. (See pw0 4563 for the power set of the empty set.) Theorem 90 of [Suppes] p. 48. Although this theorem is a special case of pwsn 4652, we have chosen to show a direct elementary proof. (Contributed by NM, 7-Aug-1994.) |
⊢ 𝒫 {∅} = {∅, {∅}} | ||
Theorem | snsspr1 4565 | A singleton is a subset of an unordered pair containing its member. (Contributed by NM, 27-Aug-2004.) |
⊢ {𝐴} ⊆ {𝐴, 𝐵} | ||
Theorem | snsspr2 4566 | A singleton is a subset of an unordered pair containing its member. (Contributed by NM, 2-May-2009.) |
⊢ {𝐵} ⊆ {𝐴, 𝐵} | ||
Theorem | snsstp1 4567 | A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013.) |
⊢ {𝐴} ⊆ {𝐴, 𝐵, 𝐶} | ||
Theorem | snsstp2 4568 | A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013.) |
⊢ {𝐵} ⊆ {𝐴, 𝐵, 𝐶} | ||
Theorem | snsstp3 4569 | A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013.) |
⊢ {𝐶} ⊆ {𝐴, 𝐵, 𝐶} | ||
Theorem | prssg 4570 | 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 4571 | 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 4572 | A pair of elements of a class is a subset of the class. (Contributed by NM, 16-Jan-2015.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → {𝐴, 𝐵} ⊆ 𝐶) | ||
Theorem | prssd 4573 | Deduction version of prssi 4572: A pair of elements of a class is a subset of the class. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ (𝜑 → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → {𝐴, 𝐵} ⊆ 𝐶) | ||
Theorem | prsspwg 4574 | 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 4575 | A pair as subset of a pair. (Contributed by AV, 26-Oct-2020.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴, 𝐵} ⊆ {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷)))) | ||
Theorem | ssprsseq 4576 | A proper pair is a subset of a pair iff it is equal to the superset. (Contributed by AV, 26-Oct-2020.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ({𝐴, 𝐵} ⊆ {𝐶, 𝐷} ↔ {𝐴, 𝐵} = {𝐶, 𝐷})) | ||
Theorem | sssn 4577 | The subsets of a singleton. (Contributed by NM, 24-Apr-2004.) |
⊢ (𝐴 ⊆ {𝐵} ↔ (𝐴 = ∅ ∨ 𝐴 = {𝐵})) | ||
Theorem | ssunsn2 4578 | 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 4655. (Contributed by Mario Carneiro, 2-Jul-2016.) |
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷})) ↔ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶) ∨ ((𝐵 ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷})))) | ||
Theorem | ssunsn 4579 | Possible values for a set sandwiched between another set and it plus a singleton. (Contributed by Mario Carneiro, 2-Jul-2016.) |
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐵 ∪ {𝐶})) ↔ (𝐴 = 𝐵 ∨ 𝐴 = (𝐵 ∪ {𝐶}))) | ||
Theorem | eqsn 4580* | 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 4581* | A sufficient condition for a (nonempty) set to be a singleton. (Contributed by AV, 20-Sep-2020.) |
⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 = 𝑦 → ∃𝑧 𝐴 = {𝑧}) | ||
Theorem | n0snor2el 4582* | A nonempty set is either a singleton or contains at least two different elements. (Contributed by AV, 20-Sep-2020.) |
⊢ (𝐴 ≠ ∅ → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 ∨ ∃𝑧 𝐴 = {𝑧})) | ||
Theorem | ssunpr 4583 | Possible values for a set sandwiched between another set and it plus a singleton. (Contributed by Mario Carneiro, 2-Jul-2016.) |
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐵 ∪ {𝐶, 𝐷})) ↔ ((𝐴 = 𝐵 ∨ 𝐴 = (𝐵 ∪ {𝐶})) ∨ (𝐴 = (𝐵 ∪ {𝐷}) ∨ 𝐴 = (𝐵 ∪ {𝐶, 𝐷})))) | ||
Theorem | sspr 4584 | The subsets of a pair. (Contributed by NM, 16-Mar-2006.) (Proof shortened by Mario Carneiro, 2-Jul-2016.) |
⊢ (𝐴 ⊆ {𝐵, 𝐶} ↔ ((𝐴 = ∅ ∨ 𝐴 = {𝐵}) ∨ (𝐴 = {𝐶} ∨ 𝐴 = {𝐵, 𝐶}))) | ||
Theorem | sstp 4585 | The subsets of a triple. (Contributed by Mario Carneiro, 2-Jul-2016.) |
⊢ (𝐴 ⊆ {𝐵, 𝐶, 𝐷} ↔ (((𝐴 = ∅ ∨ 𝐴 = {𝐵}) ∨ (𝐴 = {𝐶} ∨ 𝐴 = {𝐵, 𝐶})) ∨ ((𝐴 = {𝐷} ∨ 𝐴 = {𝐵, 𝐷}) ∨ (𝐴 = {𝐶, 𝐷} ∨ 𝐴 = {𝐵, 𝐶, 𝐷})))) | ||
Theorem | tpss 4586 | 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 4587 | A triple of elements of a class is a subset of the class. (Contributed by Alexander van der Vekens, 1-Feb-2018.) |
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) → {𝐴, 𝐵, 𝐶} ⊆ 𝐷) | ||
Theorem | sneqrg 4588 | Closed form of sneqr 4589. (Contributed by Scott Fenton, 1-Apr-2011.) (Proof shortened by JJ, 23-Jul-2021.) |
⊢ (𝐴 ∈ 𝑉 → ({𝐴} = {𝐵} → 𝐴 = 𝐵)) | ||
Theorem | sneqr 4589 | 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 4590 | If a singleton is a subset of another, their members are equal. (Contributed by NM, 28-May-2006.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ({𝐴} ⊆ {𝐵} → 𝐴 = 𝐵) | ||
Theorem | mosneq 4591* | There exists at most one set whose singleton is equal to a given class. See also moeq 3601. (Contributed by BJ, 24-Sep-2022.) |
⊢ ∃*𝑥{𝑥} = 𝐴 | ||
Theorem | sneqbg 4592 | Two singletons of sets are equal iff their elements are equal. (Contributed by Scott Fenton, 16-Apr-2012.) |
⊢ (𝐴 ∈ 𝑉 → ({𝐴} = {𝐵} ↔ 𝐴 = 𝐵)) | ||
Theorem | snsspw 4593 | The singleton of a class is a subset of its power class. (Contributed by NM, 21-Jun-1993.) |
⊢ {𝐴} ⊆ 𝒫 𝐴 | ||
Theorem | prsspw 4594 | 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 4595 | 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 4596 | 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 4597 | 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 4598 | 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 4599 | Equality relationship for two unordered pairs. (Contributed by NM, 17-Oct-1996.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))) | ||
Theorem | prel12OLD 4600 | Obsolete as of 16-Jun-2022. Use prel12g 4616 instead. (Contributed by NM, 17-Oct-1996.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ (¬ 𝐴 = 𝐵 → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ (𝐴 ∈ {𝐶, 𝐷} ∧ 𝐵 ∈ {𝐶, 𝐷}))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |