HomeHome Intuitionistic Logic Explorer
Theorem List (p. 37 of 138)
< Previous  Next >
Bad symbols? Try the
GIF version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 3601-3700   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremralsng 3601* Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.)
(𝑥 = 𝐴 → (𝜑𝜓))       (𝐴𝑉 → (∀𝑥 ∈ {𝐴}𝜑𝜓))
 
Theoremrexsng 3602* Restricted existential quantification over a singleton. (Contributed by NM, 29-Jan-2012.)
(𝑥 = 𝐴 → (𝜑𝜓))       (𝐴𝑉 → (∃𝑥 ∈ {𝐴}𝜑𝜓))
 
Theoremexsnrex 3603 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.)
(∃𝑥 𝑀 = {𝑥} ↔ ∃𝑥𝑀 𝑀 = {𝑥})
 
Theoremralsn 3604* Convert a quantification over a singleton to a substitution. (Contributed by NM, 27-Apr-2009.)
𝐴 ∈ V    &   (𝑥 = 𝐴 → (𝜑𝜓))       (∀𝑥 ∈ {𝐴}𝜑𝜓)
 
Theoremrexsn 3605* Restricted existential quantification over a singleton. (Contributed by Jeff Madsen, 5-Jan-2011.)
𝐴 ∈ V    &   (𝑥 = 𝐴 → (𝜑𝜓))       (∃𝑥 ∈ {𝐴}𝜑𝜓)
 
Theoremeltpg 3606 Members of an unordered triple of classes. (Contributed by FL, 2-Feb-2014.) (Proof shortened by Mario Carneiro, 11-Feb-2015.)
(𝐴𝑉 → (𝐴 ∈ {𝐵, 𝐶, 𝐷} ↔ (𝐴 = 𝐵𝐴 = 𝐶𝐴 = 𝐷)))
 
Theoremeldiftp 3607 Membership in a set with three elements removed. Similar to eldifsn 3688 and eldifpr 3588. (Contributed by David A. Wheeler, 22-Jul-2017.)
(𝐴 ∈ (𝐵 ∖ {𝐶, 𝐷, 𝐸}) ↔ (𝐴𝐵 ∧ (𝐴𝐶𝐴𝐷𝐴𝐸)))
 
Theoremeltpi 3608 A member of an unordered triple of classes is one of them. (Contributed by Mario Carneiro, 11-Feb-2015.)
(𝐴 ∈ {𝐵, 𝐶, 𝐷} → (𝐴 = 𝐵𝐴 = 𝐶𝐴 = 𝐷))
 
Theoremeltp 3609 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       (𝐴 ∈ {𝐵, 𝐶, 𝐷} ↔ (𝐴 = 𝐵𝐴 = 𝐶𝐴 = 𝐷))
 
Theoremdftp2 3610* Alternate definition of unordered triple of classes. Special case of Definition 5.3 of [TakeutiZaring] p. 16. (Contributed by NM, 8-Apr-1994.)
{𝐴, 𝐵, 𝐶} = {𝑥 ∣ (𝑥 = 𝐴𝑥 = 𝐵𝑥 = 𝐶)}
 
Theoremnfpr 3611 Bound-variable hypothesis builder for unordered pairs. (Contributed by NM, 14-Nov-1995.)
𝑥𝐴    &   𝑥𝐵       𝑥{𝐴, 𝐵}
 
Theoremralprg 3612* Convert a quantification over a pair to a conjunction. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
(𝑥 = 𝐴 → (𝜑𝜓))    &   (𝑥 = 𝐵 → (𝜑𝜒))       ((𝐴𝑉𝐵𝑊) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓𝜒)))
 
Theoremrexprg 3613* Convert a quantification over a pair to a disjunction. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
(𝑥 = 𝐴 → (𝜑𝜓))    &   (𝑥 = 𝐵 → (𝜑𝜒))       ((𝐴𝑉𝐵𝑊) → (∃𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓𝜒)))
 
Theoremraltpg 3614* Convert a quantification over a triple to a conjunction. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
(𝑥 = 𝐴 → (𝜑𝜓))    &   (𝑥 = 𝐵 → (𝜑𝜒))    &   (𝑥 = 𝐶 → (𝜑𝜃))       ((𝐴𝑉𝐵𝑊𝐶𝑋) → (∀𝑥 ∈ {𝐴, 𝐵, 𝐶}𝜑 ↔ (𝜓𝜒𝜃)))
 
Theoremrextpg 3615* Convert a quantification over a triple to a disjunction. (Contributed by Mario Carneiro, 23-Apr-2015.)
(𝑥 = 𝐴 → (𝜑𝜓))    &   (𝑥 = 𝐵 → (𝜑𝜒))    &   (𝑥 = 𝐶 → (𝜑𝜃))       ((𝐴𝑉𝐵𝑊𝐶𝑋) → (∃𝑥 ∈ {𝐴, 𝐵, 𝐶}𝜑 ↔ (𝜓𝜒𝜃)))
 
Theoremralpr 3616* Convert a quantification over a pair to a conjunction. (Contributed by NM, 3-Jun-2007.) (Revised by Mario Carneiro, 23-Apr-2015.)
𝐴 ∈ V    &   𝐵 ∈ V    &   (𝑥 = 𝐴 → (𝜑𝜓))    &   (𝑥 = 𝐵 → (𝜑𝜒))       (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓𝜒))
 
Theoremrexpr 3617* Convert an existential quantification over a pair to a disjunction. (Contributed by NM, 3-Jun-2007.) (Revised by Mario Carneiro, 23-Apr-2015.)
𝐴 ∈ V    &   𝐵 ∈ V    &   (𝑥 = 𝐴 → (𝜑𝜓))    &   (𝑥 = 𝐵 → (𝜑𝜒))       (∃𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓𝜒))
 
Theoremraltp 3618* Convert a quantification over a triple to a conjunction. (Contributed by NM, 13-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
𝐴 ∈ V    &   𝐵 ∈ V    &   𝐶 ∈ V    &   (𝑥 = 𝐴 → (𝜑𝜓))    &   (𝑥 = 𝐵 → (𝜑𝜒))    &   (𝑥 = 𝐶 → (𝜑𝜃))       (∀𝑥 ∈ {𝐴, 𝐵, 𝐶}𝜑 ↔ (𝜓𝜒𝜃))
 
Theoremrextp 3619* Convert a quantification over a triple to a disjunction. (Contributed by Mario Carneiro, 23-Apr-2015.)
𝐴 ∈ V    &   𝐵 ∈ V    &   𝐶 ∈ V    &   (𝑥 = 𝐴 → (𝜑𝜓))    &   (𝑥 = 𝐵 → (𝜑𝜒))    &   (𝑥 = 𝐶 → (𝜑𝜃))       (∃𝑥 ∈ {𝐴, 𝐵, 𝐶}𝜑 ↔ (𝜓𝜒𝜃))
 
Theoremsbcsng 3620* Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.)
(𝐴𝑉 → ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥 ∈ {𝐴}𝜑))
 
Theoremnfsn 3621 Bound-variable hypothesis builder for singletons. (Contributed by NM, 14-Nov-1995.)
𝑥𝐴       𝑥{𝐴}
 
Theoremcsbsng 3622 Distribute proper substitution through the singleton of a class. (Contributed by Alan Sare, 10-Nov-2012.)
(𝐴𝑉𝐴 / 𝑥{𝐵} = {𝐴 / 𝑥𝐵})
 
Theoremdisjsn 3623 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.)
((𝐴 ∩ {𝐵}) = ∅ ↔ ¬ 𝐵𝐴)
 
Theoremdisjsn2 3624 Intersection of distinct singletons is disjoint. (Contributed by NM, 25-May-1998.)
(𝐴𝐵 → ({𝐴} ∩ {𝐵}) = ∅)
 
Theoremdisjpr2 3625 The intersection of distinct unordered pairs is disjoint. (Contributed by Alexander van der Vekens, 11-Nov-2017.)
(((𝐴𝐶𝐵𝐶) ∧ (𝐴𝐷𝐵𝐷)) → ({𝐴, 𝐵} ∩ {𝐶, 𝐷}) = ∅)
 
Theoremsnprc 3626 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, 5-Aug-1993.)
𝐴 ∈ V ↔ {𝐴} = ∅)
 
Theoremr19.12sn 3627* Special case of r19.12 2563 where its converse holds. (Contributed by NM, 19-May-2008.) (Revised by Mario Carneiro, 23-Apr-2015.) (Revised by BJ, 20-Dec-2021.)
(𝐴𝑉 → (∃𝑥 ∈ {𝐴}∀𝑦𝐵 𝜑 ↔ ∀𝑦𝐵𝑥 ∈ {𝐴}𝜑))
 
Theoremrabsn 3628* Condition where a restricted class abstraction is a singleton. (Contributed by NM, 28-May-2006.)
(𝐵𝐴 → {𝑥𝐴𝑥 = 𝐵} = {𝐵})
 
Theoremrabrsndc 3629* A class abstraction over a decidable proposition restricted to a singleton is either the empty set or the singleton itself. (Contributed by Jim Kingdon, 8-Aug-2018.)
𝐴 ∈ V    &   DECID 𝜑       (𝑀 = {𝑥 ∈ {𝐴} ∣ 𝜑} → (𝑀 = ∅ ∨ 𝑀 = {𝐴}))
 
Theoremeuabsn2 3630* Another way to express existential uniqueness of a wff: its class abstraction is a singleton. (Contributed by Mario Carneiro, 14-Nov-2016.)
(∃!𝑥𝜑 ↔ ∃𝑦{𝑥𝜑} = {𝑦})
 
Theoremeuabsn 3631 Another way to express existential uniqueness of a wff: its class abstraction is a singleton. (Contributed by NM, 22-Feb-2004.)
(∃!𝑥𝜑 ↔ ∃𝑥{𝑥𝜑} = {𝑥})
 
Theoremreusn 3632* 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.)
(∃!𝑥𝐴 𝜑 ↔ ∃𝑦{𝑥𝐴𝜑} = {𝑦})
 
Theoremabsneu 3633 Restricted existential uniqueness determined by a singleton. (Contributed by NM, 29-May-2006.)
((𝐴𝑉 ∧ {𝑥𝜑} = {𝐴}) → ∃!𝑥𝜑)
 
Theoremrabsneu 3634 Restricted existential uniqueness determined by a singleton. (Contributed by NM, 29-May-2006.) (Revised by Mario Carneiro, 23-Dec-2016.)
((𝐴𝑉 ∧ {𝑥𝐵𝜑} = {𝐴}) → ∃!𝑥𝐵 𝜑)
 
Theoremeusn 3635* Two ways to express "𝐴 is a singleton." (Contributed by NM, 30-Oct-2010.)
(∃!𝑥 𝑥𝐴 ↔ ∃𝑥 𝐴 = {𝑥})
 
Theoremrabsnt 3636* 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    &   (𝑥 = 𝐵 → (𝜑𝜓))       ({𝑥𝐴𝜑} = {𝐵} → 𝜓)
 
Theoremprcom 3637 Commutative law for unordered pairs. (Contributed by NM, 5-Aug-1993.)
{𝐴, 𝐵} = {𝐵, 𝐴}
 
Theorempreq1 3638 Equality theorem for unordered pairs. (Contributed by NM, 29-Mar-1998.)
(𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
 
Theorempreq2 3639 Equality theorem for unordered pairs. (Contributed by NM, 5-Aug-1993.)
(𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
 
Theorempreq12 3640 Equality theorem for unordered pairs. (Contributed by NM, 19-Oct-2012.)
((𝐴 = 𝐶𝐵 = 𝐷) → {𝐴, 𝐵} = {𝐶, 𝐷})
 
Theorempreq1i 3641 Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
𝐴 = 𝐵       {𝐴, 𝐶} = {𝐵, 𝐶}
 
Theorempreq2i 3642 Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
𝐴 = 𝐵       {𝐶, 𝐴} = {𝐶, 𝐵}
 
Theorempreq12i 3643 Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
𝐴 = 𝐵    &   𝐶 = 𝐷       {𝐴, 𝐶} = {𝐵, 𝐷}
 
Theorempreq1d 3644 Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
(𝜑𝐴 = 𝐵)       (𝜑 → {𝐴, 𝐶} = {𝐵, 𝐶})
 
Theorempreq2d 3645 Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
(𝜑𝐴 = 𝐵)       (𝜑 → {𝐶, 𝐴} = {𝐶, 𝐵})
 
Theorempreq12d 3646 Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐶 = 𝐷)       (𝜑 → {𝐴, 𝐶} = {𝐵, 𝐷})
 
Theoremtpeq1 3647 Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
(𝐴 = 𝐵 → {𝐴, 𝐶, 𝐷} = {𝐵, 𝐶, 𝐷})
 
Theoremtpeq2 3648 Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
(𝐴 = 𝐵 → {𝐶, 𝐴, 𝐷} = {𝐶, 𝐵, 𝐷})
 
Theoremtpeq3 3649 Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
(𝐴 = 𝐵 → {𝐶, 𝐷, 𝐴} = {𝐶, 𝐷, 𝐵})
 
Theoremtpeq1d 3650 Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
(𝜑𝐴 = 𝐵)       (𝜑 → {𝐴, 𝐶, 𝐷} = {𝐵, 𝐶, 𝐷})
 
Theoremtpeq2d 3651 Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
(𝜑𝐴 = 𝐵)       (𝜑 → {𝐶, 𝐴, 𝐷} = {𝐶, 𝐵, 𝐷})
 
Theoremtpeq3d 3652 Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
(𝜑𝐴 = 𝐵)       (𝜑 → {𝐶, 𝐷, 𝐴} = {𝐶, 𝐷, 𝐵})
 
Theoremtpeq123d 3653 Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐶 = 𝐷)    &   (𝜑𝐸 = 𝐹)       (𝜑 → {𝐴, 𝐶, 𝐸} = {𝐵, 𝐷, 𝐹})
 
Theoremtprot 3654 Rotation of the elements of an unordered triple. (Contributed by Alan Sare, 24-Oct-2011.)
{𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴}
 
Theoremtpcoma 3655 Swap 1st and 2nd members of an undordered triple. (Contributed by NM, 22-May-2015.)
{𝐴, 𝐵, 𝐶} = {𝐵, 𝐴, 𝐶}
 
Theoremtpcomb 3656 Swap 2nd and 3rd members of an undordered triple. (Contributed by NM, 22-May-2015.)
{𝐴, 𝐵, 𝐶} = {𝐴, 𝐶, 𝐵}
 
Theoremtpass 3657 Split off the first element of an unordered triple. (Contributed by Mario Carneiro, 5-Jan-2016.)
{𝐴, 𝐵, 𝐶} = ({𝐴} ∪ {𝐵, 𝐶})
 
Theoremqdass 3658 Two ways to write an unordered quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.)
({𝐴, 𝐵} ∪ {𝐶, 𝐷}) = ({𝐴, 𝐵, 𝐶} ∪ {𝐷})
 
Theoremqdassr 3659 Two ways to write an unordered quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.)
({𝐴, 𝐵} ∪ {𝐶, 𝐷}) = ({𝐴} ∪ {𝐵, 𝐶, 𝐷})
 
Theoremtpidm12 3660 Unordered triple {𝐴, 𝐴, 𝐵} is just an overlong way to write {𝐴, 𝐵}. (Contributed by David A. Wheeler, 10-May-2015.)
{𝐴, 𝐴, 𝐵} = {𝐴, 𝐵}
 
Theoremtpidm13 3661 Unordered triple {𝐴, 𝐵, 𝐴} is just an overlong way to write {𝐴, 𝐵}. (Contributed by David A. Wheeler, 10-May-2015.)
{𝐴, 𝐵, 𝐴} = {𝐴, 𝐵}
 
Theoremtpidm23 3662 Unordered triple {𝐴, 𝐵, 𝐵} is just an overlong way to write {𝐴, 𝐵}. (Contributed by David A. Wheeler, 10-May-2015.)
{𝐴, 𝐵, 𝐵} = {𝐴, 𝐵}
 
Theoremtpidm 3663 Unordered triple {𝐴, 𝐴, 𝐴} is just an overlong way to write {𝐴}. (Contributed by David A. Wheeler, 10-May-2015.)
{𝐴, 𝐴, 𝐴} = {𝐴}
 
Theoremtppreq3 3664 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.)
(𝐵 = 𝐶 → {𝐴, 𝐵, 𝐶} = {𝐴, 𝐵})
 
Theoremprid1g 3665 An unordered pair contains its first member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by Stefan Allan, 8-Nov-2008.)
(𝐴𝑉𝐴 ∈ {𝐴, 𝐵})
 
Theoremprid2g 3666 An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by Stefan Allan, 8-Nov-2008.)
(𝐵𝑉𝐵 ∈ {𝐴, 𝐵})
 
Theoremprid1 3667 An unordered pair contains its first member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 5-Aug-1993.)
𝐴 ∈ V       𝐴 ∈ {𝐴, 𝐵}
 
Theoremprid2 3668 An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 5-Aug-1993.)
𝐵 ∈ V       𝐵 ∈ {𝐴, 𝐵}
 
Theoremprprc1 3669 A proper class vanishes in an unordered pair. (Contributed by NM, 5-Aug-1993.)
𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
 
Theoremprprc2 3670 A proper class vanishes in an unordered pair. (Contributed by NM, 22-Mar-2006.)
𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
 
Theoremprprc 3671 An unordered pair containing two proper classes is the empty set. (Contributed by NM, 22-Mar-2006.)
((¬ 𝐴 ∈ V ∧ ¬ 𝐵 ∈ V) → {𝐴, 𝐵} = ∅)
 
Theoremtpid1 3672 One of the three elements of an unordered triple. (Contributed by NM, 7-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
𝐴 ∈ V       𝐴 ∈ {𝐴, 𝐵, 𝐶}
 
Theoremtpid1g 3673 Closed theorem form of tpid1 3672. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
(𝐴𝐵𝐴 ∈ {𝐴, 𝐶, 𝐷})
 
Theoremtpid2 3674 One of the three elements of an unordered triple. (Contributed by NM, 7-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
𝐵 ∈ V       𝐵 ∈ {𝐴, 𝐵, 𝐶}
 
Theoremtpid2g 3675 Closed theorem form of tpid2 3674. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
(𝐴𝐵𝐴 ∈ {𝐶, 𝐴, 𝐷})
 
Theoremtpid3g 3676 Closed theorem form of tpid3 3677. (Contributed by Alan Sare, 24-Oct-2011.)
(𝐴𝐵𝐴 ∈ {𝐶, 𝐷, 𝐴})
 
Theoremtpid3 3677 One of the three elements of an unordered triple. (Contributed by NM, 7-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
𝐶 ∈ V       𝐶 ∈ {𝐴, 𝐵, 𝐶}
 
Theoremsnnzg 3678 The singleton of a set is not empty. (Contributed by NM, 14-Dec-2008.)
(𝐴𝑉 → {𝐴} ≠ ∅)
 
Theoremsnmg 3679* The singleton of a set is inhabited. (Contributed by Jim Kingdon, 11-Aug-2018.)
(𝐴𝑉 → ∃𝑥 𝑥 ∈ {𝐴})
 
Theoremsnnz 3680 The singleton of a set is not empty. (Contributed by NM, 10-Apr-1994.)
𝐴 ∈ V       {𝐴} ≠ ∅
 
Theoremsnm 3681* The singleton of a set is inhabited. (Contributed by Jim Kingdon, 11-Aug-2018.)
𝐴 ∈ V       𝑥 𝑥 ∈ {𝐴}
 
Theoremprmg 3682* A pair containing a set is inhabited. (Contributed by Jim Kingdon, 21-Sep-2018.)
(𝐴𝑉 → ∃𝑥 𝑥 ∈ {𝐴, 𝐵})
 
Theoremprnz 3683 A pair containing a set is not empty. (Contributed by NM, 9-Apr-1994.)
𝐴 ∈ V       {𝐴, 𝐵} ≠ ∅
 
Theoremprm 3684* A pair containing a set is inhabited. (Contributed by Jim Kingdon, 21-Sep-2018.)
𝐴 ∈ V       𝑥 𝑥 ∈ {𝐴, 𝐵}
 
Theoremprnzg 3685 A pair containing a set is not empty. (Contributed by FL, 19-Sep-2011.)
(𝐴𝑉 → {𝐴, 𝐵} ≠ ∅)
 
Theoremtpnz 3686 A triplet containing a set is not empty. (Contributed by NM, 10-Apr-1994.)
𝐴 ∈ V       {𝐴, 𝐵, 𝐶} ≠ ∅
 
Theoremsnss 3687 The singleton of an element of a class is a subset of the class. Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 5-Aug-1993.)
𝐴 ∈ V       (𝐴𝐵 ↔ {𝐴} ⊆ 𝐵)
 
Theoremeldifsn 3688 Membership in a set with an element removed. (Contributed by NM, 10-Oct-2007.)
(𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴𝐵𝐴𝐶))
 
Theoremssdifsn 3689 Subset of a set with an element removed. (Contributed by Emmett Weisz, 7-Jul-2021.) (Proof shortened by JJ, 31-May-2022.)
(𝐴 ⊆ (𝐵 ∖ {𝐶}) ↔ (𝐴𝐵 ∧ ¬ 𝐶𝐴))
 
Theoremeldifsni 3690 Membership in a set with an element removed. (Contributed by NM, 10-Mar-2015.)
(𝐴 ∈ (𝐵 ∖ {𝐶}) → 𝐴𝐶)
 
Theoremneldifsn 3691 𝐴 is not in (𝐵 ∖ {𝐴}). (Contributed by David Moews, 1-May-2017.)
¬ 𝐴 ∈ (𝐵 ∖ {𝐴})
 
Theoremneldifsnd 3692 𝐴 is not in (𝐵 ∖ {𝐴}). Deduction form. (Contributed by David Moews, 1-May-2017.)
(𝜑 → ¬ 𝐴 ∈ (𝐵 ∖ {𝐴}))
 
Theoremrexdifsn 3693 Restricted existential quantification over a set with an element removed. (Contributed by NM, 4-Feb-2015.)
(∃𝑥 ∈ (𝐴 ∖ {𝐵})𝜑 ↔ ∃𝑥𝐴 (𝑥𝐵𝜑))
 
Theoremsnssg 3694 The singleton of an element of a class is a subset of the class. Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 22-Jul-2001.)
(𝐴𝑉 → (𝐴𝐵 ↔ {𝐴} ⊆ 𝐵))
 
Theoremdifsn 3695 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.)
𝐴𝐵 → (𝐵 ∖ {𝐴}) = 𝐵)
 
Theoremdifprsnss 3696 Removal of a singleton from an unordered pair. (Contributed by NM, 16-Mar-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
({𝐴, 𝐵} ∖ {𝐴}) ⊆ {𝐵}
 
Theoremdifprsn1 3697 Removal of a singleton from an unordered pair. (Contributed by Thierry Arnoux, 4-Feb-2017.)
(𝐴𝐵 → ({𝐴, 𝐵} ∖ {𝐴}) = {𝐵})
 
Theoremdifprsn2 3698 Removal of a singleton from an unordered pair. (Contributed by Alexander van der Vekens, 5-Oct-2017.)
(𝐴𝐵 → ({𝐴, 𝐵} ∖ {𝐵}) = {𝐴})
 
Theoremdiftpsn3 3699 Removal of a singleton from an unordered triple. (Contributed by Alexander van der Vekens, 5-Oct-2017.)
((𝐴𝐶𝐵𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = {𝐴, 𝐵})
 
Theoremdifpr 3700 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.)
(𝐴 ∖ {𝐵, 𝐶}) = ((𝐴 ∖ {𝐵}) ∖ {𝐶})
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13749
  Copyright terms: Public domain < Previous  Next >