Theorem List for Intuitionistic Logic Explorer - 3701-3800 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | preq1d 3701 |
Equality deduction for unordered pairs. (Contributed by NM,
19-Oct-2012.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → {𝐴, 𝐶} = {𝐵, 𝐶}) |
|
Theorem | preq2d 3702 |
Equality deduction for unordered pairs. (Contributed by NM,
19-Oct-2012.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → {𝐶, 𝐴} = {𝐶, 𝐵}) |
|
Theorem | preq12d 3703 |
Equality deduction for unordered pairs. (Contributed by NM,
19-Oct-2012.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → {𝐴, 𝐶} = {𝐵, 𝐷}) |
|
Theorem | tpeq1 3704 |
Equality theorem for unordered triples. (Contributed by NM,
13-Sep-2011.)
|
⊢ (𝐴 = 𝐵 → {𝐴, 𝐶, 𝐷} = {𝐵, 𝐶, 𝐷}) |
|
Theorem | tpeq2 3705 |
Equality theorem for unordered triples. (Contributed by NM,
13-Sep-2011.)
|
⊢ (𝐴 = 𝐵 → {𝐶, 𝐴, 𝐷} = {𝐶, 𝐵, 𝐷}) |
|
Theorem | tpeq3 3706 |
Equality theorem for unordered triples. (Contributed by NM,
13-Sep-2011.)
|
⊢ (𝐴 = 𝐵 → {𝐶, 𝐷, 𝐴} = {𝐶, 𝐷, 𝐵}) |
|
Theorem | tpeq1d 3707 |
Equality theorem for unordered triples. (Contributed by NM,
22-Jun-2014.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → {𝐴, 𝐶, 𝐷} = {𝐵, 𝐶, 𝐷}) |
|
Theorem | tpeq2d 3708 |
Equality theorem for unordered triples. (Contributed by NM,
22-Jun-2014.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → {𝐶, 𝐴, 𝐷} = {𝐶, 𝐵, 𝐷}) |
|
Theorem | tpeq3d 3709 |
Equality theorem for unordered triples. (Contributed by NM,
22-Jun-2014.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → {𝐶, 𝐷, 𝐴} = {𝐶, 𝐷, 𝐵}) |
|
Theorem | tpeq123d 3710 |
Equality theorem for unordered triples. (Contributed by NM,
22-Jun-2014.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐶 = 𝐷)
& ⊢ (𝜑 → 𝐸 = 𝐹) ⇒ ⊢ (𝜑 → {𝐴, 𝐶, 𝐸} = {𝐵, 𝐷, 𝐹}) |
|
Theorem | tprot 3711 |
Rotation of the elements of an unordered triple. (Contributed by Alan
Sare, 24-Oct-2011.)
|
⊢ {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴} |
|
Theorem | tpcoma 3712 |
Swap 1st and 2nd members of an undordered triple. (Contributed by NM,
22-May-2015.)
|
⊢ {𝐴, 𝐵, 𝐶} = {𝐵, 𝐴, 𝐶} |
|
Theorem | tpcomb 3713 |
Swap 2nd and 3rd members of an undordered triple. (Contributed by NM,
22-May-2015.)
|
⊢ {𝐴, 𝐵, 𝐶} = {𝐴, 𝐶, 𝐵} |
|
Theorem | tpass 3714 |
Split off the first element of an unordered triple. (Contributed by Mario
Carneiro, 5-Jan-2016.)
|
⊢ {𝐴, 𝐵, 𝐶} = ({𝐴} ∪ {𝐵, 𝐶}) |
|
Theorem | qdass 3715 |
Two ways to write an unordered quadruple. (Contributed by Mario Carneiro,
5-Jan-2016.)
|
⊢ ({𝐴, 𝐵} ∪ {𝐶, 𝐷}) = ({𝐴, 𝐵, 𝐶} ∪ {𝐷}) |
|
Theorem | qdassr 3716 |
Two ways to write an unordered quadruple. (Contributed by Mario Carneiro,
5-Jan-2016.)
|
⊢ ({𝐴, 𝐵} ∪ {𝐶, 𝐷}) = ({𝐴} ∪ {𝐵, 𝐶, 𝐷}) |
|
Theorem | tpidm12 3717 |
Unordered triple {𝐴, 𝐴, 𝐵} is just an overlong way to write
{𝐴,
𝐵}. (Contributed by
David A. Wheeler, 10-May-2015.)
|
⊢ {𝐴, 𝐴, 𝐵} = {𝐴, 𝐵} |
|
Theorem | tpidm13 3718 |
Unordered triple {𝐴, 𝐵, 𝐴} is just an overlong way to write
{𝐴,
𝐵}. (Contributed by
David A. Wheeler, 10-May-2015.)
|
⊢ {𝐴, 𝐵, 𝐴} = {𝐴, 𝐵} |
|
Theorem | tpidm23 3719 |
Unordered triple {𝐴, 𝐵, 𝐵} is just an overlong way to write
{𝐴,
𝐵}. (Contributed by
David A. Wheeler, 10-May-2015.)
|
⊢ {𝐴, 𝐵, 𝐵} = {𝐴, 𝐵} |
|
Theorem | tpidm 3720 |
Unordered triple {𝐴, 𝐴, 𝐴} is just an overlong way to write
{𝐴}. (Contributed by David A. Wheeler,
10-May-2015.)
|
⊢ {𝐴, 𝐴, 𝐴} = {𝐴} |
|
Theorem | tppreq3 3721 |
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 3722 |
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 3723 |
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 3724 |
An unordered pair contains its first member. Part of Theorem 7.6 of
[Quine] p. 49. (Contributed by NM,
5-Aug-1993.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ 𝐴 ∈ {𝐴, 𝐵} |
|
Theorem | prid2 3725 |
An unordered pair contains its second member. Part of Theorem 7.6 of
[Quine] p. 49. (Contributed by NM,
5-Aug-1993.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ 𝐵 ∈ {𝐴, 𝐵} |
|
Theorem | prprc1 3726 |
A proper class vanishes in an unordered pair. (Contributed by NM,
5-Aug-1993.)
|
⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵}) |
|
Theorem | prprc2 3727 |
A proper class vanishes in an unordered pair. (Contributed by NM,
22-Mar-2006.)
|
⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴}) |
|
Theorem | prprc 3728 |
An unordered pair containing two proper classes is the empty set.
(Contributed by NM, 22-Mar-2006.)
|
⊢ ((¬ 𝐴 ∈ V ∧ ¬ 𝐵 ∈ V) → {𝐴, 𝐵} = ∅) |
|
Theorem | tpid1 3729 |
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 3730 |
Closed theorem form of tpid1 3729. (Contributed by Glauco Siliprandi,
23-Oct-2021.)
|
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ {𝐴, 𝐶, 𝐷}) |
|
Theorem | tpid2 3731 |
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 3732 |
Closed theorem form of tpid2 3731. (Contributed by Glauco Siliprandi,
23-Oct-2021.)
|
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ {𝐶, 𝐴, 𝐷}) |
|
Theorem | tpid3g 3733 |
Closed theorem form of tpid3 3734. (Contributed by Alan Sare,
24-Oct-2011.)
|
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ {𝐶, 𝐷, 𝐴}) |
|
Theorem | tpid3 3734 |
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 | snnzg 3735 |
The singleton of a set is not empty. (Contributed by NM, 14-Dec-2008.)
|
⊢ (𝐴 ∈ 𝑉 → {𝐴} ≠ ∅) |
|
Theorem | snmg 3736* |
The singleton of a set is inhabited. (Contributed by Jim Kingdon,
11-Aug-2018.)
|
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 ∈ {𝐴}) |
|
Theorem | snnz 3737 |
The singleton of a set is not empty. (Contributed by NM,
10-Apr-1994.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ {𝐴} ≠ ∅ |
|
Theorem | snm 3738* |
The singleton of a set is inhabited. (Contributed by Jim Kingdon,
11-Aug-2018.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ ∃𝑥 𝑥 ∈ {𝐴} |
|
Theorem | prmg 3739* |
A pair containing a set is inhabited. (Contributed by Jim Kingdon,
21-Sep-2018.)
|
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 ∈ {𝐴, 𝐵}) |
|
Theorem | prnz 3740 |
A pair containing a set is not empty. It is also inhabited (see
prm 3741). (Contributed by NM, 9-Apr-1994.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ {𝐴, 𝐵} ≠ ∅ |
|
Theorem | prm 3741* |
A pair containing a set is inhabited. (Contributed by Jim Kingdon,
21-Sep-2018.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ ∃𝑥 𝑥 ∈ {𝐴, 𝐵} |
|
Theorem | prnzg 3742 |
A pair containing a set is not empty. It is also inhabited (see
prmg 3739). (Contributed by FL, 19-Sep-2011.)
|
⊢ (𝐴 ∈ 𝑉 → {𝐴, 𝐵} ≠ ∅) |
|
Theorem | tpnz 3743 |
A triplet containing a set is not empty. (Contributed by NM,
10-Apr-1994.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ {𝐴, 𝐵, 𝐶} ≠ ∅ |
|
Theorem | snssOLD 3744 |
Obsolete version of snss 3753 as of 1-Jan-2025. (Contributed by NM,
5-Aug-1993.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵) |
|
Theorem | eldifsn 3745 |
Membership in a set with an element removed. (Contributed by NM,
10-Oct-2007.)
|
⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶)) |
|
Theorem | ssdifsn 3746 |
Subset of a set with an element removed. (Contributed by Emmett Weisz,
7-Jul-2021.) (Proof shortened by JJ, 31-May-2022.)
|
⊢ (𝐴 ⊆ (𝐵 ∖ {𝐶}) ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐶 ∈ 𝐴)) |
|
Theorem | eldifsni 3747 |
Membership in a set with an element removed. (Contributed by NM,
10-Mar-2015.)
|
⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) → 𝐴 ≠ 𝐶) |
|
Theorem | neldifsn 3748 |
𝐴
is not in (𝐵 ∖ {𝐴}). (Contributed by David Moews,
1-May-2017.)
|
⊢ ¬ 𝐴 ∈ (𝐵 ∖ {𝐴}) |
|
Theorem | neldifsnd 3749 |
𝐴
is not in (𝐵 ∖ {𝐴}). Deduction form. (Contributed by
David Moews, 1-May-2017.)
|
⊢ (𝜑 → ¬ 𝐴 ∈ (𝐵 ∖ {𝐴})) |
|
Theorem | rexdifsn 3750 |
Restricted existential quantification over a set with an element removed.
(Contributed by NM, 4-Feb-2015.)
|
⊢ (∃𝑥 ∈ (𝐴 ∖ {𝐵})𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝑥 ≠ 𝐵 ∧ 𝜑)) |
|
Theorem | snssb 3751 |
Characterization of the inclusion of a singleton in a class.
(Contributed by BJ, 1-Jan-2025.)
|
⊢ ({𝐴} ⊆ 𝐵 ↔ (𝐴 ∈ V → 𝐴 ∈ 𝐵)) |
|
Theorem | snssg 3752 |
The singleton formed on a set is included in a class if and only if the
set is an element of that class. Theorem 7.4 of [Quine] p. 49.
(Contributed by NM, 22-Jul-2001.) (Proof shortened by BJ, 1-Jan-2025.)
|
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵)) |
|
Theorem | snss 3753 |
The singleton of an element of a class is a subset of the class
(inference form of snssg 3752). Theorem 7.4 of [Quine] p. 49.
(Contributed by NM, 21-Jun-1993.) (Proof shortened by BJ,
1-Jan-2025.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵) |
|
Theorem | snssgOLD 3754 |
Obsolete version of snssgOLD 3754 as of 1-Jan-2025. (Contributed by NM,
22-Jul-2001.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵)) |
|
Theorem | difsn 3755 |
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 3756 |
Removal of a singleton from an unordered pair. (Contributed by NM,
16-Mar-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|
⊢ ({𝐴, 𝐵} ∖ {𝐴}) ⊆ {𝐵} |
|
Theorem | difprsn1 3757 |
Removal of a singleton from an unordered pair. (Contributed by Thierry
Arnoux, 4-Feb-2017.)
|
⊢ (𝐴 ≠ 𝐵 → ({𝐴, 𝐵} ∖ {𝐴}) = {𝐵}) |
|
Theorem | difprsn2 3758 |
Removal of a singleton from an unordered pair. (Contributed by Alexander
van der Vekens, 5-Oct-2017.)
|
⊢ (𝐴 ≠ 𝐵 → ({𝐴, 𝐵} ∖ {𝐵}) = {𝐴}) |
|
Theorem | diftpsn3 3759 |
Removal of a singleton from an unordered triple. (Contributed by
Alexander van der Vekens, 5-Oct-2017.)
|
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = {𝐴, 𝐵}) |
|
Theorem | difpr 3760 |
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 | difsnb 3761 |
(𝐵 ∖
{𝐴}) equals 𝐵 if and
only if 𝐴 is not a member of
𝐵. Generalization of difsn 3755. (Contributed by David Moews,
1-May-2017.)
|
⊢ (¬ 𝐴 ∈ 𝐵 ↔ (𝐵 ∖ {𝐴}) = 𝐵) |
|
Theorem | snssi 3762 |
The singleton of an element of a class is a subset of the class.
(Contributed by NM, 6-Jun-1994.)
|
⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵) |
|
Theorem | snssd 3763 |
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 | difsnss 3764 |
If we remove a single element from a class then put it back in, we end up
with a subset of the original class. If equality is decidable, we can
replace subset with equality as seen in nndifsnid 6560. (Contributed by Jim
Kingdon, 10-Aug-2018.)
|
⊢ (𝐵 ∈ 𝐴 → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) ⊆ 𝐴) |
|
Theorem | pw0 3765 |
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 | snsspr1 3766 |
A singleton is a subset of an unordered pair containing its member.
(Contributed by NM, 27-Aug-2004.)
|
⊢ {𝐴} ⊆ {𝐴, 𝐵} |
|
Theorem | snsspr2 3767 |
A singleton is a subset of an unordered pair containing its member.
(Contributed by NM, 2-May-2009.)
|
⊢ {𝐵} ⊆ {𝐴, 𝐵} |
|
Theorem | snsstp1 3768 |
A singleton is a subset of an unordered triple containing its member.
(Contributed by NM, 9-Oct-2013.)
|
⊢ {𝐴} ⊆ {𝐴, 𝐵, 𝐶} |
|
Theorem | snsstp2 3769 |
A singleton is a subset of an unordered triple containing its member.
(Contributed by NM, 9-Oct-2013.)
|
⊢ {𝐵} ⊆ {𝐴, 𝐵, 𝐶} |
|
Theorem | snsstp3 3770 |
A singleton is a subset of an unordered triple containing its member.
(Contributed by NM, 9-Oct-2013.)
|
⊢ {𝐶} ⊆ {𝐴, 𝐵, 𝐶} |
|
Theorem | prsstp12 3771 |
A pair is a subset of an unordered triple containing its members.
(Contributed by Jim Kingdon, 11-Aug-2018.)
|
⊢ {𝐴, 𝐵} ⊆ {𝐴, 𝐵, 𝐶} |
|
Theorem | prsstp13 3772 |
A pair is a subset of an unordered triple containing its members.
(Contributed by Jim Kingdon, 11-Aug-2018.)
|
⊢ {𝐴, 𝐶} ⊆ {𝐴, 𝐵, 𝐶} |
|
Theorem | prsstp23 3773 |
A pair is a subset of an unordered triple containing its members.
(Contributed by Jim Kingdon, 11-Aug-2018.)
|
⊢ {𝐵, 𝐶} ⊆ {𝐴, 𝐵, 𝐶} |
|
Theorem | prss 3774 |
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.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶) |
|
Theorem | prssg 3775 |
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 | prssi 3776 |
A pair of elements of a class is a subset of the class. (Contributed by
NM, 16-Jan-2015.)
|
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → {𝐴, 𝐵} ⊆ 𝐶) |
|
Theorem | prssd 3777 |
Deduction version of prssi 3776: A pair of elements of a class is a
subset of the class. (Contributed by Glauco Siliprandi,
17-Aug-2020.)
|
⊢ (𝜑 → 𝐴 ∈ 𝐶)
& ⊢ (𝜑 → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → {𝐴, 𝐵} ⊆ 𝐶) |
|
Theorem | prsspwg 3778 |
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 | sssnr 3779 |
Empty set and the singleton itself are subsets of a singleton.
Concerning the converse, see exmidsssn 4231. (Contributed by Jim Kingdon,
10-Aug-2018.)
|
⊢ ((𝐴 = ∅ ∨ 𝐴 = {𝐵}) → 𝐴 ⊆ {𝐵}) |
|
Theorem | sssnm 3780* |
The inhabited subset of a singleton. (Contributed by Jim Kingdon,
10-Aug-2018.)
|
⊢ (∃𝑥 𝑥 ∈ 𝐴 → (𝐴 ⊆ {𝐵} ↔ 𝐴 = {𝐵})) |
|
Theorem | eqsnm 3781* |
Two ways to express that an inhabited set equals a singleton.
(Contributed by Jim Kingdon, 11-Aug-2018.)
|
⊢ (∃𝑥 𝑥 ∈ 𝐴 → (𝐴 = {𝐵} ↔ ∀𝑥 ∈ 𝐴 𝑥 = 𝐵)) |
|
Theorem | ssprr 3782 |
The subsets of a pair. (Contributed by Jim Kingdon, 11-Aug-2018.)
|
⊢ (((𝐴 = ∅ ∨ 𝐴 = {𝐵}) ∨ (𝐴 = {𝐶} ∨ 𝐴 = {𝐵, 𝐶})) → 𝐴 ⊆ {𝐵, 𝐶}) |
|
Theorem | sstpr 3783 |
The subsets of a triple. (Contributed by Jim Kingdon, 11-Aug-2018.)
|
⊢ ((((𝐴 = ∅ ∨ 𝐴 = {𝐵}) ∨ (𝐴 = {𝐶} ∨ 𝐴 = {𝐵, 𝐶})) ∨ ((𝐴 = {𝐷} ∨ 𝐴 = {𝐵, 𝐷}) ∨ (𝐴 = {𝐶, 𝐷} ∨ 𝐴 = {𝐵, 𝐶, 𝐷}))) → 𝐴 ⊆ {𝐵, 𝐶, 𝐷}) |
|
Theorem | tpss 3784 |
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 3785 |
A triple of elements of a class is a subset of the class. (Contributed by
Alexander van der Vekens, 1-Feb-2018.)
|
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) → {𝐴, 𝐵, 𝐶} ⊆ 𝐷) |
|
Theorem | sneqr 3786 |
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 3787 |
If a singleton is a subset of another, their members are equal.
(Contributed by NM, 28-May-2006.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ ({𝐴} ⊆ {𝐵} → 𝐴 = 𝐵) |
|
Theorem | sneqrg 3788 |
Closed form of sneqr 3786. (Contributed by Scott Fenton, 1-Apr-2011.)
|
⊢ (𝐴 ∈ 𝑉 → ({𝐴} = {𝐵} → 𝐴 = 𝐵)) |
|
Theorem | sneqbg 3789 |
Two singletons of sets are equal iff their elements are equal.
(Contributed by Scott Fenton, 16-Apr-2012.)
|
⊢ (𝐴 ∈ 𝑉 → ({𝐴} = {𝐵} ↔ 𝐴 = 𝐵)) |
|
Theorem | snsspw 3790 |
The singleton of a class is a subset of its power class. (Contributed
by NM, 5-Aug-1993.)
|
⊢ {𝐴} ⊆ 𝒫 𝐴 |
|
Theorem | prsspw 3791 |
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.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ ({𝐴, 𝐵} ⊆ 𝒫 𝐶 ↔ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶)) |
|
Theorem | preqr1g 3792 |
Reverse equality lemma for unordered pairs. If two unordered pairs have
the same second element, the first elements are equal. Closed form of
preqr1 3794. (Contributed by Jim Kingdon, 21-Sep-2018.)
|
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ({𝐴, 𝐶} = {𝐵, 𝐶} → 𝐴 = 𝐵)) |
|
Theorem | preqr2g 3793 |
Reverse equality lemma for unordered pairs. If two unordered pairs have
the same second element, the second elements are equal. Closed form of
preqr2 3795. (Contributed by Jim Kingdon, 21-Sep-2018.)
|
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ({𝐶, 𝐴} = {𝐶, 𝐵} → 𝐴 = 𝐵)) |
|
Theorem | preqr1 3794 |
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 3795 |
Reverse equality lemma for unordered pairs. If two unordered pairs have
the same first element, the second elements are equal. (Contributed by
NM, 5-Aug-1993.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ ({𝐶, 𝐴} = {𝐶, 𝐵} → 𝐴 = 𝐵) |
|
Theorem | preq12b 3796 |
Equality relationship for two unordered pairs. (Contributed by NM,
17-Oct-1996.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈
V ⇒ ⊢ ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))) |
|
Theorem | prel12 3797 |
Equality of two unordered pairs. (Contributed by NM, 17-Oct-1996.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈
V ⇒ ⊢ (¬ 𝐴 = 𝐵 → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ (𝐴 ∈ {𝐶, 𝐷} ∧ 𝐵 ∈ {𝐶, 𝐷}))) |
|
Theorem | opthpr 3798 |
A way to represent ordered pairs using unordered pairs with distinct
members. (Contributed by NM, 27-Mar-2007.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈
V ⇒ ⊢ (𝐴 ≠ 𝐷 → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) |
|
Theorem | preq12bg 3799 |
Closed form of preq12b 3796. (Contributed by Scott Fenton,
28-Mar-2014.)
|
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))) |
|
Theorem | prneimg 3800 |
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.)
|
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → (((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∨ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)) → {𝐴, 𝐵} ≠ {𝐶, 𝐷})) |