![]() |
Metamath
Proof Explorer Theorem List (p. 47 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 | raltp 4601* | Convert a universal quantification over an unordered triple to a conjunction. (Contributed by NM, 13-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜃)) ⇒ ⊢ (∀𝑥 ∈ {𝐴, 𝐵, 𝐶}𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) | ||
Theorem | rextp 4602* | Convert an existential quantification over an unordered triple to a disjunction. (Contributed by Mario Carneiro, 23-Apr-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜃)) ⇒ ⊢ (∃𝑥 ∈ {𝐴, 𝐵, 𝐶}𝜑 ↔ (𝜓 ∨ 𝜒 ∨ 𝜃)) | ||
Theorem | nfsn 4603 | Bound-variable hypothesis builder for singletons. (Contributed by NM, 14-Nov-1995.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥{𝐴} | ||
Theorem | csbsng 4604 | Distribute proper substitution through the singleton of a class. csbsng 4604 is derived from the virtual deduction proof csbsngVD 41599. (Contributed by Alan Sare, 10-Nov-2012.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{𝐵} = {⦋𝐴 / 𝑥⦌𝐵}) | ||
Theorem | csbprg 4605 | Distribute proper substitution through a pair of classes. (Contributed by Alexander van der Vekens, 4-Sep-2018.) |
⊢ (𝐶 ∈ 𝑉 → ⦋𝐶 / 𝑥⦌{𝐴, 𝐵} = {⦋𝐶 / 𝑥⦌𝐴, ⦋𝐶 / 𝑥⦌𝐵}) | ||
Theorem | elinsn 4606 | If the intersection of two classes is a (proper) singleton, then the singleton element is a member of both classes. (Contributed by AV, 30-Dec-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐵 ∩ 𝐶) = {𝐴}) → (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)) | ||
Theorem | disjsn 4607 | Intersection with the singleton of a non-member is disjoint. (Contributed by NM, 22-May-1998.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) (Proof shortened by Wolf Lammen, 30-Sep-2014.) |
⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ 𝐴) | ||
Theorem | disjsn2 4608 | Two distinct singletons are disjoint. (Contributed by NM, 25-May-1998.) |
⊢ (𝐴 ≠ 𝐵 → ({𝐴} ∩ {𝐵}) = ∅) | ||
Theorem | disjpr2 4609 | Two completely distinct unordered pairs are disjoint. (Contributed by Alexander van der Vekens, 11-Nov-2017.) (Proof shortened by JJ, 23-Jul-2021.) |
⊢ (((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ (𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷)) → ({𝐴, 𝐵} ∩ {𝐶, 𝐷}) = ∅) | ||
Theorem | disjprsn 4610 | The disjoint intersection of an unordered pair and a singleton. (Contributed by AV, 23-Jan-2021.) |
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵} ∩ {𝐶}) = ∅) | ||
Theorem | disjtpsn 4611 | The disjoint intersection of an unordered triple and a singleton. (Contributed by AV, 14-Nov-2021.) |
⊢ ((𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷) → ({𝐴, 𝐵, 𝐶} ∩ {𝐷}) = ∅) | ||
Theorem | disjtp2 4612 | Two completely distinct unordered triples are disjoint. (Contributed by AV, 14-Nov-2021.) |
⊢ (((𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴 ≠ 𝐸 ∧ 𝐵 ≠ 𝐸 ∧ 𝐶 ≠ 𝐸) ∧ (𝐴 ≠ 𝐹 ∧ 𝐵 ≠ 𝐹 ∧ 𝐶 ≠ 𝐹)) → ({𝐴, 𝐵, 𝐶} ∩ {𝐷, 𝐸, 𝐹}) = ∅) | ||
Theorem | snprc 4613 | The singleton of a proper class (one that doesn't exist) is the empty set. Theorem 7.2 of [Quine] p. 48. (Contributed by NM, 21-Jun-1993.) |
⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅) | ||
Theorem | snnzb 4614 | A singleton is nonempty iff its argument is a set. (Contributed by Scott Fenton, 8-May-2018.) |
⊢ (𝐴 ∈ V ↔ {𝐴} ≠ ∅) | ||
Theorem | rmosn 4615* | A restricted at-most-one quantifier over a singleton is always true. (Contributed by AV, 3-Apr-2023.) |
⊢ ∃*𝑥 ∈ {𝐴}𝜑 | ||
Theorem | r19.12sn 4616* | Special case of r19.12 3283 where its converse holds. (Contributed by NM, 19-May-2008.) (Revised by Mario Carneiro, 23-Apr-2015.) (Revised by BJ, 18-Mar-2020.) |
⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ {𝐴}𝜑)) | ||
Theorem | rabsn 4617* | Condition where a restricted class abstraction is a singleton. (Contributed by NM, 28-May-2006.) (Proof shortened by AV, 26-Aug-2022.) |
⊢ (𝐵 ∈ 𝐴 → {𝑥 ∈ 𝐴 ∣ 𝑥 = 𝐵} = {𝐵}) | ||
Theorem | rabsnifsb 4618* | A restricted class abstraction restricted to a singleton is either the empty set or the singleton itself. (Contributed by AV, 21-Jul-2019.) |
⊢ {𝑥 ∈ {𝐴} ∣ 𝜑} = if([𝐴 / 𝑥]𝜑, {𝐴}, ∅) | ||
Theorem | rabsnif 4619* | A restricted class abstraction restricted to a singleton is either the empty set or the singleton itself. (Contributed by AV, 12-Apr-2019.) (Proof shortened by AV, 21-Jul-2019.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∈ {𝐴} ∣ 𝜑} = if(𝜓, {𝐴}, ∅) | ||
Theorem | rabrsn 4620* | A restricted class abstraction restricted to a singleton is either the empty set or the singleton itself. (Contributed by Alexander van der Vekens, 22-Dec-2017.) (Proof shortened by AV, 21-Jul-2019.) |
⊢ (𝑀 = {𝑥 ∈ {𝐴} ∣ 𝜑} → (𝑀 = ∅ ∨ 𝑀 = {𝐴})) | ||
Theorem | euabsn2 4621* | Another way to express existential uniqueness of a wff: its class abstraction is a singleton. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ (∃!𝑥𝜑 ↔ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦}) | ||
Theorem | euabsn 4622 | Another way to express existential uniqueness of a wff: its class abstraction is a singleton. (Contributed by NM, 22-Feb-2004.) |
⊢ (∃!𝑥𝜑 ↔ ∃𝑥{𝑥 ∣ 𝜑} = {𝑥}) | ||
Theorem | reusn 4623* | A way to express restricted existential uniqueness of a wff: its restricted class abstraction is a singleton. (Contributed by NM, 30-May-2006.) (Proof shortened by Mario Carneiro, 14-Nov-2016.) |
⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦{𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦}) | ||
Theorem | absneu 4624 | Restricted existential uniqueness determined by a singleton. (Contributed by NM, 29-May-2006.) |
⊢ ((𝐴 ∈ 𝑉 ∧ {𝑥 ∣ 𝜑} = {𝐴}) → ∃!𝑥𝜑) | ||
Theorem | rabsneu 4625 | Restricted existential uniqueness determined by a singleton. (Contributed by NM, 29-May-2006.) (Revised by Mario Carneiro, 23-Dec-2016.) |
⊢ ((𝐴 ∈ 𝑉 ∧ {𝑥 ∈ 𝐵 ∣ 𝜑} = {𝐴}) → ∃!𝑥 ∈ 𝐵 𝜑) | ||
Theorem | eusn 4626* | Two ways to express "𝐴 is a singleton." (Contributed by NM, 30-Oct-2010.) |
⊢ (∃!𝑥 𝑥 ∈ 𝐴 ↔ ∃𝑥 𝐴 = {𝑥}) | ||
Theorem | rabsnt 4627* | Truth implied by equality of a restricted class abstraction and a singleton. (Contributed by NM, 29-May-2006.) (Proof shortened by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝐵 ∈ V & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = {𝐵} → 𝜓) | ||
Theorem | prcom 4628 | Commutative law for unordered pairs. (Contributed by NM, 15-Jul-1993.) |
⊢ {𝐴, 𝐵} = {𝐵, 𝐴} | ||
Theorem | preq1 4629 | Equality theorem for unordered pairs. (Contributed by NM, 29-Mar-1998.) |
⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶}) | ||
Theorem | preq2 4630 | Equality theorem for unordered pairs. (Contributed by NM, 15-Jul-1993.) |
⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵}) | ||
Theorem | preq12 4631 | Equality theorem for unordered pairs. (Contributed by NM, 19-Oct-2012.) |
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → {𝐴, 𝐵} = {𝐶, 𝐷}) | ||
Theorem | preq1i 4632 | Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ {𝐴, 𝐶} = {𝐵, 𝐶} | ||
Theorem | preq2i 4633 | Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ {𝐶, 𝐴} = {𝐶, 𝐵} | ||
Theorem | preq12i 4634 | Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ {𝐴, 𝐶} = {𝐵, 𝐷} | ||
Theorem | preq1d 4635 | Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → {𝐴, 𝐶} = {𝐵, 𝐶}) | ||
Theorem | preq2d 4636 | Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → {𝐶, 𝐴} = {𝐶, 𝐵}) | ||
Theorem | preq12d 4637 | Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → {𝐴, 𝐶} = {𝐵, 𝐷}) | ||
Theorem | tpeq1 4638 | Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.) |
⊢ (𝐴 = 𝐵 → {𝐴, 𝐶, 𝐷} = {𝐵, 𝐶, 𝐷}) | ||
Theorem | tpeq2 4639 | Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.) |
⊢ (𝐴 = 𝐵 → {𝐶, 𝐴, 𝐷} = {𝐶, 𝐵, 𝐷}) | ||
Theorem | tpeq3 4640 | Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.) |
⊢ (𝐴 = 𝐵 → {𝐶, 𝐷, 𝐴} = {𝐶, 𝐷, 𝐵}) | ||
Theorem | tpeq1d 4641 | Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → {𝐴, 𝐶, 𝐷} = {𝐵, 𝐶, 𝐷}) | ||
Theorem | tpeq2d 4642 | Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → {𝐶, 𝐴, 𝐷} = {𝐶, 𝐵, 𝐷}) | ||
Theorem | tpeq3d 4643 | Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → {𝐶, 𝐷, 𝐴} = {𝐶, 𝐷, 𝐵}) | ||
Theorem | tpeq123d 4644 | Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) & ⊢ (𝜑 → 𝐸 = 𝐹) ⇒ ⊢ (𝜑 → {𝐴, 𝐶, 𝐸} = {𝐵, 𝐷, 𝐹}) | ||
Theorem | tprot 4645 | Rotation of the elements of an unordered triple. (Contributed by Alan Sare, 24-Oct-2011.) |
⊢ {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴} | ||
Theorem | tpcoma 4646 | Swap 1st and 2nd members of an unordered triple. (Contributed by NM, 22-May-2015.) |
⊢ {𝐴, 𝐵, 𝐶} = {𝐵, 𝐴, 𝐶} | ||
Theorem | tpcomb 4647 | Swap 2nd and 3rd members of an unordered triple. (Contributed by NM, 22-May-2015.) |
⊢ {𝐴, 𝐵, 𝐶} = {𝐴, 𝐶, 𝐵} | ||
Theorem | tpass 4648 | Split off the first element of an unordered triple. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ {𝐴, 𝐵, 𝐶} = ({𝐴} ∪ {𝐵, 𝐶}) | ||
Theorem | qdass 4649 | Two ways to write an unordered quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ ({𝐴, 𝐵} ∪ {𝐶, 𝐷}) = ({𝐴, 𝐵, 𝐶} ∪ {𝐷}) | ||
Theorem | qdassr 4650 | Two ways to write an unordered quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ ({𝐴, 𝐵} ∪ {𝐶, 𝐷}) = ({𝐴} ∪ {𝐵, 𝐶, 𝐷}) | ||
Theorem | tpidm12 4651 | Unordered triple {𝐴, 𝐴, 𝐵} is just an overlong way to write {𝐴, 𝐵}. (Contributed by David A. Wheeler, 10-May-2015.) |
⊢ {𝐴, 𝐴, 𝐵} = {𝐴, 𝐵} | ||
Theorem | tpidm13 4652 | Unordered triple {𝐴, 𝐵, 𝐴} is just an overlong way to write {𝐴, 𝐵}. (Contributed by David A. Wheeler, 10-May-2015.) |
⊢ {𝐴, 𝐵, 𝐴} = {𝐴, 𝐵} | ||
Theorem | tpidm23 4653 | Unordered triple {𝐴, 𝐵, 𝐵} is just an overlong way to write {𝐴, 𝐵}. (Contributed by David A. Wheeler, 10-May-2015.) |
⊢ {𝐴, 𝐵, 𝐵} = {𝐴, 𝐵} | ||
Theorem | tpidm 4654 | Unordered triple {𝐴, 𝐴, 𝐴} is just an overlong way to write {𝐴}. (Contributed by David A. Wheeler, 10-May-2015.) |
⊢ {𝐴, 𝐴, 𝐴} = {𝐴} | ||
Theorem | tppreq3 4655 | 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 4656 | 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 4657 | 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 4658 | 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 4659 | An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Note: the proof from prid2g 4657 and ax-mp 5 has one fewer essential step but one more total step.) (Contributed by NM, 5-Aug-1993.) |
⊢ 𝐵 ∈ V ⇒ ⊢ 𝐵 ∈ {𝐴, 𝐵} | ||
Theorem | ifpprsnss 4660 | 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 4661 | A proper class vanishes in an unordered pair. (Contributed by NM, 15-Jul-1993.) |
⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵}) | ||
Theorem | prprc2 4662 | A proper class vanishes in an unordered pair. (Contributed by NM, 22-Mar-2006.) |
⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴}) | ||
Theorem | prprc 4663 | An unordered pair containing two proper classes is the empty set. (Contributed by NM, 22-Mar-2006.) |
⊢ ((¬ 𝐴 ∈ V ∧ ¬ 𝐵 ∈ V) → {𝐴, 𝐵} = ∅) | ||
Theorem | tpid1 4664 | 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 4665 | Closed theorem form of tpid1 4664. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ {𝐴, 𝐶, 𝐷}) | ||
Theorem | tpid2 4666 | 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 4667 | Closed theorem form of tpid2 4666. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ {𝐶, 𝐴, 𝐷}) | ||
Theorem | tpid3g 4668 | Closed theorem form of tpid3 4669. (Contributed by Alan Sare, 24-Oct-2011.) (Proof shortened by JJ, 30-Apr-2021.) |
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ {𝐶, 𝐷, 𝐴}) | ||
Theorem | tpid3 4669 | 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 4670 | The singleton of a set is not empty. (Contributed by NM, 14-Dec-2008.) |
⊢ (𝐴 ∈ 𝑉 → {𝐴} ≠ ∅) | ||
Theorem | snn0d 4671 | The singleton of a set is not empty. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → {𝐴} ≠ ∅) | ||
Theorem | snnz 4672 | The singleton of a set is not empty. (Contributed by NM, 10-Apr-1994.) |
⊢ 𝐴 ∈ V ⇒ ⊢ {𝐴} ≠ ∅ | ||
Theorem | prnz 4673 | A pair containing a set is not empty. (Contributed by NM, 9-Apr-1994.) |
⊢ 𝐴 ∈ V ⇒ ⊢ {𝐴, 𝐵} ≠ ∅ | ||
Theorem | prnzg 4674 | A pair containing a set is not empty. (Contributed by FL, 19-Sep-2011.) (Proof shortened by JJ, 23-Jul-2021.) |
⊢ (𝐴 ∈ 𝑉 → {𝐴, 𝐵} ≠ ∅) | ||
Theorem | tpnz 4675 | An unordered triple containing a set is not empty. (Contributed by NM, 10-Apr-1994.) |
⊢ 𝐴 ∈ V ⇒ ⊢ {𝐴, 𝐵, 𝐶} ≠ ∅ | ||
Theorem | tpnzd 4676 | An unordered triple containing a set is not empty. (Contributed by Thierry Arnoux, 8-Apr-2019.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → {𝐴, 𝐵, 𝐶} ≠ ∅) | ||
Theorem | raltpd 4677* | Convert a universal quantification over an unordered triple to a conjunction. (Contributed by Thierry Arnoux, 8-Apr-2019.) |
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) & ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → (𝜓 ↔ 𝜃)) & ⊢ ((𝜑 ∧ 𝑥 = 𝐶) → (𝜓 ↔ 𝜏)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ {𝐴, 𝐵, 𝐶}𝜓 ↔ (𝜒 ∧ 𝜃 ∧ 𝜏))) | ||
Theorem | snssg 4678 | The singleton of an element of a class is a subset of the class (general form of snss 4679). Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 22-Jul-2001.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵)) | ||
Theorem | snss 4679 | The singleton of an element of a class is a subset of the class (inference form of snssg 4678). Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 21-Jun-1993.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵) | ||
Theorem | eldifsn 4680 | Membership in a set with an element removed. (Contributed by NM, 10-Oct-2007.) |
⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶)) | ||
Theorem | ssdifsn 4681 | Subset of a set with an element removed. (Contributed by Emmett Weisz, 7-Jul-2021.) (Proof shortened by JJ, 31-May-2022.) |
⊢ (𝐴 ⊆ (𝐵 ∖ {𝐶}) ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐶 ∈ 𝐴)) | ||
Theorem | elpwdifsn 4682 | 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 4683 | Membership in a set with an element removed. (Contributed by NM, 10-Mar-2015.) |
⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) → 𝐴 ≠ 𝐶) | ||
Theorem | eldifsnneq 4684 | 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 | neldifsn 4685 | The class 𝐴 is not in (𝐵 ∖ {𝐴}). (Contributed by David Moews, 1-May-2017.) |
⊢ ¬ 𝐴 ∈ (𝐵 ∖ {𝐴}) | ||
Theorem | neldifsnd 4686 | The class 𝐴 is not in (𝐵 ∖ {𝐴}). Deduction form. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → ¬ 𝐴 ∈ (𝐵 ∖ {𝐴})) | ||
Theorem | rexdifsn 4687 | Restricted existential quantification over a set with an element removed. (Contributed by NM, 4-Feb-2015.) |
⊢ (∃𝑥 ∈ (𝐴 ∖ {𝐵})𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝑥 ≠ 𝐵 ∧ 𝜑)) | ||
Theorem | raldifsni 4688 | Rearrangement of a property of a singleton difference. (Contributed by Stefan O'Rear, 27-Feb-2015.) |
⊢ (∀𝑥 ∈ (𝐴 ∖ {𝐵}) ¬ 𝜑 ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝐵)) | ||
Theorem | raldifsnb 4689* | 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 4690 | 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 4691 | 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 4692 | Removal of a singleton from an unordered pair. (Contributed by NM, 16-Mar-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ ({𝐴, 𝐵} ∖ {𝐴}) ⊆ {𝐵} | ||
Theorem | difprsn1 4693 | Removal of a singleton from an unordered pair. (Contributed by Thierry Arnoux, 4-Feb-2017.) |
⊢ (𝐴 ≠ 𝐵 → ({𝐴, 𝐵} ∖ {𝐴}) = {𝐵}) | ||
Theorem | difprsn2 4694 | Removal of a singleton from an unordered pair. (Contributed by Alexander van der Vekens, 5-Oct-2017.) |
⊢ (𝐴 ≠ 𝐵 → ({𝐴, 𝐵} ∖ {𝐵}) = {𝐴}) | ||
Theorem | diftpsn3 4695 | 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 4696 | 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 4697 | 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 4698 | 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 4699 | (𝐵 ∖ {𝐴}) equals 𝐵 if and only if 𝐴 is not a member of 𝐵. Generalization of difsn 4691. (Contributed by David Moews, 1-May-2017.) |
⊢ (¬ 𝐴 ∈ 𝐵 ↔ (𝐵 ∖ {𝐴}) = 𝐵) | ||
Theorem | difsnpss 4700 | (𝐵 ∖ {𝐴}) is a proper subclass of 𝐵 if and only if 𝐴 is a member of 𝐵. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝐴 ∈ 𝐵 ↔ (𝐵 ∖ {𝐴}) ⊊ 𝐵) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |