Theorem List for Intuitionistic Logic Explorer - 3401-3500 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | rexsnsOLD 3401* |
Restricted existential quantification over a singleton. (Contributed by
Mario Carneiro, 23-Apr-2015.) Obsolete as of 22-Aug-2018. Use rexsns 3400
instead. (New usage is discouraged.)
(Proof modification is discouraged.)
|
⊢ (A ∈ 𝑉 → (∃x ∈ {A}φ ↔ [A / x]φ)) |
|
Theorem | ralsng 3402* |
Substitution expressed in terms of quantification over a singleton.
(Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro,
23-Apr-2015.)
|
⊢ (x =
A → (φ ↔ ψ)) ⇒ ⊢ (A ∈ 𝑉 → (∀x ∈ {A}φ ↔ ψ)) |
|
Theorem | rexsng 3403* |
Restricted existential quantification over a singleton. (Contributed by
NM, 29-Jan-2012.)
|
⊢ (x =
A → (φ ↔ ψ)) ⇒ ⊢ (A ∈ 𝑉 → (∃x ∈ {A}φ ↔ ψ)) |
|
Theorem | exsnrex 3404 |
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.)
|
⊢ (∃x 𝑀 = {x}
↔ ∃x ∈ 𝑀 𝑀 = {x}) |
|
Theorem | ralsn 3405* |
Convert a quantification over a singleton to a substitution.
(Contributed by NM, 27-Apr-2009.)
|
⊢ A ∈ V
& ⊢ (x =
A → (φ ↔ ψ)) ⇒ ⊢ (∀x ∈ {A}φ ↔ ψ) |
|
Theorem | rexsn 3406* |
Restricted existential quantification over a singleton. (Contributed by
Jeff Madsen, 5-Jan-2011.)
|
⊢ A ∈ V
& ⊢ (x =
A → (φ ↔ ψ)) ⇒ ⊢ (∃x ∈ {A}φ ↔ ψ) |
|
Theorem | eltpg 3407 |
Members of an unordered triple of classes. (Contributed by FL,
2-Feb-2014.) (Proof shortened by Mario Carneiro, 11-Feb-2015.)
|
⊢ (A ∈ 𝑉 → (A ∈ {B, 𝐶, 𝐷} ↔ (A = B ∨ A = 𝐶
∨ A = 𝐷))) |
|
Theorem | eltpi 3408 |
A member of an unordered triple of classes is one of them. (Contributed
by Mario Carneiro, 11-Feb-2015.)
|
⊢ (A ∈ {B, 𝐶, 𝐷} → (A = B ∨ A = 𝐶
∨ A = 𝐷)) |
|
Theorem | eltp 3409 |
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.)
|
⊢ A ∈ V ⇒ ⊢ (A ∈ {B, 𝐶, 𝐷} ↔ (A = B ∨ A = 𝐶
∨ A = 𝐷)) |
|
Theorem | dftp2 3410* |
Alternate definition of unordered triple of classes. Special case of
Definition 5.3 of [TakeutiZaring]
p. 16. (Contributed by NM,
8-Apr-1994.)
|
⊢ {A,
B, 𝐶} = {x
∣ (x = A ∨ x = B ∨ x = 𝐶)} |
|
Theorem | nfpr 3411 |
Bound-variable hypothesis builder for unordered pairs. (Contributed by
NM, 14-Nov-1995.)
|
⊢ ℲxA & ⊢
ℲxB ⇒ ⊢ Ⅎx{A, B} |
|
Theorem | ralprg 3412* |
Convert a quantification over a pair to a conjunction. (Contributed by
NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
|
⊢ (x =
A → (φ ↔ ψ)) & ⊢ (x = B →
(φ ↔ χ)) ⇒ ⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊) → (∀x ∈ {A, B}φ ↔
(ψ ∧
χ))) |
|
Theorem | rexprg 3413* |
Convert a quantification over a pair to a disjunction. (Contributed by
NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
|
⊢ (x =
A → (φ ↔ ψ)) & ⊢ (x = B →
(φ ↔ χ)) ⇒ ⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊) → (∃x ∈ {A, B}φ ↔
(ψ ∨
χ))) |
|
Theorem | raltpg 3414* |
Convert a quantification over a triple to a conjunction. (Contributed
by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
|
⊢ (x =
A → (φ ↔ ψ)) & ⊢ (x = B →
(φ ↔ χ)) & ⊢ (x = 𝐶 → (φ ↔ θ)) ⇒ ⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (∀x ∈ {A, B, 𝐶}φ
↔ (ψ ∧ χ ∧ θ))) |
|
Theorem | rextpg 3415* |
Convert a quantification over a triple to a disjunction. (Contributed
by Mario Carneiro, 23-Apr-2015.)
|
⊢ (x =
A → (φ ↔ ψ)) & ⊢ (x = B →
(φ ↔ χ)) & ⊢ (x = 𝐶 → (φ ↔ θ)) ⇒ ⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (∃x ∈ {A, B, 𝐶}φ
↔ (ψ
∨ χ
∨ θ))) |
|
Theorem | ralpr 3416* |
Convert a quantification over a pair to a conjunction. (Contributed by
NM, 3-Jun-2007.) (Revised by Mario Carneiro, 23-Apr-2015.)
|
⊢ A ∈ V
& ⊢ B ∈ V
& ⊢ (x =
A → (φ ↔ ψ)) & ⊢ (x = B →
(φ ↔ χ)) ⇒ ⊢ (∀x ∈ {A, B}φ ↔
(ψ ∧
χ)) |
|
Theorem | rexpr 3417* |
Convert an existential quantification over a pair to a disjunction.
(Contributed by NM, 3-Jun-2007.) (Revised by Mario Carneiro,
23-Apr-2015.)
|
⊢ A ∈ V
& ⊢ B ∈ V
& ⊢ (x =
A → (φ ↔ ψ)) & ⊢ (x = B →
(φ ↔ χ)) ⇒ ⊢ (∃x ∈ {A, B}φ ↔
(ψ ∨
χ)) |
|
Theorem | raltp 3418* |
Convert a quantification over a triple to a conjunction. (Contributed
by NM, 13-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
|
⊢ A ∈ V
& ⊢ B ∈ V
& ⊢ 𝐶 ∈
V
& ⊢ (x =
A → (φ ↔ ψ)) & ⊢ (x = B →
(φ ↔ χ)) & ⊢ (x = 𝐶 → (φ ↔ θ)) ⇒ ⊢ (∀x ∈ {A, B, 𝐶}φ
↔ (ψ ∧ χ ∧ θ)) |
|
Theorem | rextp 3419* |
Convert a quantification over a triple to a disjunction. (Contributed
by Mario Carneiro, 23-Apr-2015.)
|
⊢ A ∈ V
& ⊢ B ∈ V
& ⊢ 𝐶 ∈
V
& ⊢ (x =
A → (φ ↔ ψ)) & ⊢ (x = B →
(φ ↔ χ)) & ⊢ (x = 𝐶 → (φ ↔ θ)) ⇒ ⊢ (∃x ∈ {A, B, 𝐶}φ
↔ (ψ
∨ χ
∨ θ)) |
|
Theorem | sbcsng 3420* |
Substitution expressed in terms of quantification over a singleton.
(Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro,
23-Apr-2015.)
|
⊢ (A ∈ 𝑉 → ([A / x]φ
↔ ∀x ∈ {A}φ)) |
|
Theorem | nfsn 3421 |
Bound-variable hypothesis builder for singletons. (Contributed by NM,
14-Nov-1995.)
|
⊢ ℲxA ⇒ ⊢ Ⅎx{A} |
|
Theorem | csbsng 3422 |
Distribute proper substitution through the singleton of a class.
(Contributed by Alan Sare, 10-Nov-2012.)
|
⊢ (A ∈ 𝑉 → ⦋A / x⦌{B} = {⦋A / x⦌B}) |
|
Theorem | disjsn 3423 |
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.)
|
⊢ ((A ∩
{B}) = ∅ ↔ ¬ B ∈ A) |
|
Theorem | disjsn2 3424 |
Intersection of distinct singletons is disjoint. (Contributed by NM,
25-May-1998.)
|
⊢ (A ≠
B → ({A} ∩ {B}) =
∅) |
|
Theorem | disjpr2 3425 |
The intersection of distinct unordered pairs is disjoint. (Contributed by
Alexander van der Vekens, 11-Nov-2017.)
|
⊢ (((A ≠
𝐶 ∧ B ≠ 𝐶) ∧ (A ≠ 𝐷 ∧ B ≠ 𝐷)) → ({A, B} ∩
{𝐶, 𝐷}) = ∅) |
|
Theorem | snprc 3426 |
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.)
|
⊢ (¬ A
∈ V ↔ {A} = ∅) |
|
Theorem | r19.12sn 3427* |
Special case of r19.12 2416 where its converse holds. (Contributed by
NM,
19-May-2008.) (Revised by Mario Carneiro, 23-Apr-2015.)
|
⊢ A ∈ V ⇒ ⊢ (∃x ∈ {A}∀y ∈ B φ ↔ ∀y ∈ B ∃x ∈ {A}φ) |
|
Theorem | rabsn 3428* |
Condition where a restricted class abstraction is a singleton.
(Contributed by NM, 28-May-2006.)
|
⊢ (B ∈ A →
{x ∈
A ∣ x = B} =
{B}) |
|
Theorem | rabrsndc 3429* |
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.)
|
⊢ A ∈ V
& ⊢ DECID φ ⇒ ⊢ (𝑀 = {x
∈ {A}
∣ φ} → (𝑀 = ∅
∨ 𝑀 = {A})) |
|
Theorem | euabsn2 3430* |
Another way to express existential uniqueness of a wff: its class
abstraction is a singleton. (Contributed by Mario Carneiro,
14-Nov-2016.)
|
⊢ (∃!xφ ↔
∃y{x ∣
φ} = {y}) |
|
Theorem | euabsn 3431 |
Another way to express existential uniqueness of a wff: its class
abstraction is a singleton. (Contributed by NM, 22-Feb-2004.)
|
⊢ (∃!xφ ↔
∃x{x ∣
φ} = {x}) |
|
Theorem | reusn 3432* |
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.)
|
⊢ (∃!x ∈ A φ ↔
∃y{x ∈ A ∣
φ} = {y}) |
|
Theorem | absneu 3433 |
Restricted existential uniqueness determined by a singleton.
(Contributed by NM, 29-May-2006.)
|
⊢ ((A ∈ 𝑉 ∧
{x ∣ φ} = {A}) → ∃!xφ) |
|
Theorem | rabsneu 3434 |
Restricted existential uniqueness determined by a singleton.
(Contributed by NM, 29-May-2006.) (Revised by Mario Carneiro,
23-Dec-2016.)
|
⊢ ((A ∈ 𝑉 ∧
{x ∈
B ∣ φ} = {A}) → ∃!x ∈ B φ) |
|
Theorem | eusn 3435* |
Two ways to express "A is a singleton." (Contributed by NM,
30-Oct-2010.)
|
⊢ (∃!x x ∈ A ↔
∃x
A = {x}) |
|
Theorem | rabsnt 3436* |
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.)
|
⊢ B ∈ V
& ⊢ (x =
B → (φ ↔ ψ)) ⇒ ⊢ ({x ∈ A ∣ φ} = {B}
→ ψ) |
|
Theorem | prcom 3437 |
Commutative law for unordered pairs. (Contributed by NM, 5-Aug-1993.)
|
⊢ {A,
B} = {B, A} |
|
Theorem | preq1 3438 |
Equality theorem for unordered pairs. (Contributed by NM,
29-Mar-1998.)
|
⊢ (A =
B → {A, 𝐶} = {B,
𝐶}) |
|
Theorem | preq2 3439 |
Equality theorem for unordered pairs. (Contributed by NM, 5-Aug-1993.)
|
⊢ (A =
B → {𝐶, A} =
{𝐶, B}) |
|
Theorem | preq12 3440 |
Equality theorem for unordered pairs. (Contributed by NM,
19-Oct-2012.)
|
⊢ ((A = 𝐶 ∧ B = 𝐷) → {A, B} = {𝐶, 𝐷}) |
|
Theorem | preq1i 3441 |
Equality inference for unordered pairs. (Contributed by NM,
19-Oct-2012.)
|
⊢ A =
B ⇒ ⊢ {A, 𝐶} = {B,
𝐶} |
|
Theorem | preq2i 3442 |
Equality inference for unordered pairs. (Contributed by NM,
19-Oct-2012.)
|
⊢ A =
B ⇒ ⊢ {𝐶, A} =
{𝐶, B} |
|
Theorem | preq12i 3443 |
Equality inference for unordered pairs. (Contributed by NM,
19-Oct-2012.)
|
⊢ A =
B & ⊢ 𝐶 = 𝐷 ⇒ ⊢ {A, 𝐶} = {B,
𝐷} |
|
Theorem | preq1d 3444 |
Equality deduction for unordered pairs. (Contributed by NM,
19-Oct-2012.)
|
⊢ (φ
→ A = B) ⇒ ⊢ (φ → {A, 𝐶} = {B,
𝐶}) |
|
Theorem | preq2d 3445 |
Equality deduction for unordered pairs. (Contributed by NM,
19-Oct-2012.)
|
⊢ (φ
→ A = B) ⇒ ⊢ (φ → {𝐶, A} =
{𝐶, B}) |
|
Theorem | preq12d 3446 |
Equality deduction for unordered pairs. (Contributed by NM,
19-Oct-2012.)
|
⊢ (φ
→ A = B)
& ⊢ (φ
→ 𝐶 = 𝐷)
⇒ ⊢ (φ → {A, 𝐶} = {B,
𝐷}) |
|
Theorem | tpeq1 3447 |
Equality theorem for unordered triples. (Contributed by NM,
13-Sep-2011.)
|
⊢ (A =
B → {A, 𝐶, 𝐷} = {B,
𝐶, 𝐷}) |
|
Theorem | tpeq2 3448 |
Equality theorem for unordered triples. (Contributed by NM,
13-Sep-2011.)
|
⊢ (A =
B → {𝐶, A,
𝐷} = {𝐶, B,
𝐷}) |
|
Theorem | tpeq3 3449 |
Equality theorem for unordered triples. (Contributed by NM,
13-Sep-2011.)
|
⊢ (A =
B → {𝐶, 𝐷, A} =
{𝐶, 𝐷, B}) |
|
Theorem | tpeq1d 3450 |
Equality theorem for unordered triples. (Contributed by NM,
22-Jun-2014.)
|
⊢ (φ
→ A = B) ⇒ ⊢ (φ → {A, 𝐶, 𝐷} = {B,
𝐶, 𝐷}) |
|
Theorem | tpeq2d 3451 |
Equality theorem for unordered triples. (Contributed by NM,
22-Jun-2014.)
|
⊢ (φ
→ A = B) ⇒ ⊢ (φ → {𝐶, A,
𝐷} = {𝐶, B,
𝐷}) |
|
Theorem | tpeq3d 3452 |
Equality theorem for unordered triples. (Contributed by NM,
22-Jun-2014.)
|
⊢ (φ
→ A = B) ⇒ ⊢ (φ → {𝐶, 𝐷, A} =
{𝐶, 𝐷, B}) |
|
Theorem | tpeq123d 3453 |
Equality theorem for unordered triples. (Contributed by NM,
22-Jun-2014.)
|
⊢ (φ
→ A = B)
& ⊢ (φ
→ 𝐶 = 𝐷) & ⊢ (φ → 𝐸 = 𝐹) ⇒ ⊢ (φ → {A, 𝐶, 𝐸} = {B,
𝐷, 𝐹}) |
|
Theorem | tprot 3454 |
Rotation of the elements of an unordered triple. (Contributed by Alan
Sare, 24-Oct-2011.)
|
⊢ {A,
B, 𝐶} = {B,
𝐶, A} |
|
Theorem | tpcoma 3455 |
Swap 1st and 2nd members of an undordered triple. (Contributed by NM,
22-May-2015.)
|
⊢ {A,
B, 𝐶} = {B,
A, 𝐶} |
|
Theorem | tpcomb 3456 |
Swap 2nd and 3rd members of an undordered triple. (Contributed by NM,
22-May-2015.)
|
⊢ {A,
B, 𝐶} = {A,
𝐶, B} |
|
Theorem | tpass 3457 |
Split off the first element of an unordered triple. (Contributed by Mario
Carneiro, 5-Jan-2016.)
|
⊢ {A,
B, 𝐶} = ({A} ∪ {B,
𝐶}) |
|
Theorem | qdass 3458 |
Two ways to write an unordered quadruple. (Contributed by Mario Carneiro,
5-Jan-2016.)
|
⊢ ({A,
B} ∪ {𝐶, 𝐷}) = ({A, B, 𝐶} ∪ {𝐷}) |
|
Theorem | qdassr 3459 |
Two ways to write an unordered quadruple. (Contributed by Mario Carneiro,
5-Jan-2016.)
|
⊢ ({A,
B} ∪ {𝐶, 𝐷}) = ({A} ∪ {B,
𝐶, 𝐷}) |
|
Theorem | tpidm12 3460 |
Unordered triple {A,
A, B} is just an overlong way to write
{A, B}. (Contributed by David A. Wheeler,
10-May-2015.)
|
⊢ {A,
A, B}
= {A, B} |
|
Theorem | tpidm13 3461 |
Unordered triple {A,
B, A} is just an overlong way to write
{A, B}. (Contributed by David A. Wheeler,
10-May-2015.)
|
⊢ {A,
B, A}
= {A, B} |
|
Theorem | tpidm23 3462 |
Unordered triple {A,
B, B} is just an overlong way to write
{A, B}. (Contributed by David A. Wheeler,
10-May-2015.)
|
⊢ {A,
B, B}
= {A, B} |
|
Theorem | tpidm 3463 |
Unordered triple {A,
A, A} is just an overlong way to write
{A}.
(Contributed by David A. Wheeler, 10-May-2015.)
|
⊢ {A,
A, A}
= {A} |
|
Theorem | tppreq3 3464 |
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.)
|
⊢ (B = 𝐶 → {A, B, 𝐶} = {A, B}) |
|
Theorem | prid1g 3465 |
An unordered pair contains its first member. Part of Theorem 7.6 of
[Quine] p. 49. (Contributed by Stefan
Allan, 8-Nov-2008.)
|
⊢ (A ∈ 𝑉 → A ∈ {A, B}) |
|
Theorem | prid2g 3466 |
An unordered pair contains its second member. Part of Theorem 7.6 of
[Quine] p. 49. (Contributed by Stefan
Allan, 8-Nov-2008.)
|
⊢ (B ∈ 𝑉 → B ∈ {A, B}) |
|
Theorem | prid1 3467 |
An unordered pair contains its first member. Part of Theorem 7.6 of
[Quine] p. 49. (Contributed by NM,
5-Aug-1993.)
|
⊢ A ∈ V ⇒ ⊢ A ∈ {A, B} |
|
Theorem | prid2 3468 |
An unordered pair contains its second member. Part of Theorem 7.6 of
[Quine] p. 49. (Contributed by NM,
5-Aug-1993.)
|
⊢ B ∈ V ⇒ ⊢ B ∈ {A, B} |
|
Theorem | prprc1 3469 |
A proper class vanishes in an unordered pair. (Contributed by NM,
5-Aug-1993.)
|
⊢ (¬ A
∈ V → {A, B} =
{B}) |
|
Theorem | prprc2 3470 |
A proper class vanishes in an unordered pair. (Contributed by NM,
22-Mar-2006.)
|
⊢ (¬ B
∈ V → {A, B} =
{A}) |
|
Theorem | prprc 3471 |
An unordered pair containing two proper classes is the empty set.
(Contributed by NM, 22-Mar-2006.)
|
⊢ ((¬ A
∈ V ∧ ¬
B ∈ V)
→ {A, B} = ∅) |
|
Theorem | tpid1 3472 |
One of the three elements of an unordered triple. (Contributed by NM,
7-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|
⊢ A ∈ V ⇒ ⊢ A ∈ {A, B, 𝐶} |
|
Theorem | tpid2 3473 |
One of the three elements of an unordered triple. (Contributed by NM,
7-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|
⊢ B ∈ V ⇒ ⊢ B ∈ {A, B, 𝐶} |
|
Theorem | tpid3g 3474 |
Closed theorem form of tpid3 3475. (Contributed by Alan Sare,
24-Oct-2011.)
|
⊢ (A ∈ B →
A ∈
{𝐶, 𝐷, A}) |
|
Theorem | tpid3 3475 |
One of the three elements of an unordered triple. (Contributed by NM,
7-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|
⊢ 𝐶 ∈
V ⇒ ⊢ 𝐶 ∈
{A, B,
𝐶} |
|
Theorem | snnzg 3476 |
The singleton of a set is not empty. (Contributed by NM, 14-Dec-2008.)
|
⊢ (A ∈ 𝑉 → {A} ≠ ∅) |
|
Theorem | snmg 3477* |
The singleton of a set is inhabited. (Contributed by Jim Kingdon,
11-Aug-2018.)
|
⊢ (A ∈ 𝑉 → ∃x x ∈ {A}) |
|
Theorem | snnz 3478 |
The singleton of a set is not empty. (Contributed by NM,
10-Apr-1994.)
|
⊢ A ∈ V ⇒ ⊢ {A} ≠ ∅ |
|
Theorem | snm 3479* |
The singleton of a set is inhabited. (Contributed by Jim Kingdon,
11-Aug-2018.)
|
⊢ A ∈ V ⇒ ⊢ ∃x x ∈ {A} |
|
Theorem | prmg 3480* |
A pair containing a set is inhabited. (Contributed by Jim Kingdon,
21-Sep-2018.)
|
⊢ (A ∈ 𝑉 → ∃x x ∈ {A, B}) |
|
Theorem | prnz 3481 |
A pair containing a set is not empty. (Contributed by NM,
9-Apr-1994.)
|
⊢ A ∈ V ⇒ ⊢ {A, B} ≠
∅ |
|
Theorem | prm 3482* |
A pair containing a set is inhabited. (Contributed by Jim Kingdon,
21-Sep-2018.)
|
⊢ A ∈ V ⇒ ⊢ ∃x x ∈ {A, B} |
|
Theorem | prnzg 3483 |
A pair containing a set is not empty. (Contributed by FL,
19-Sep-2011.)
|
⊢ (A ∈ 𝑉 → {A, B} ≠
∅) |
|
Theorem | tpnz 3484 |
A triplet containing a set is not empty. (Contributed by NM,
10-Apr-1994.)
|
⊢ A ∈ V ⇒ ⊢ {A, B, 𝐶} ≠ ∅ |
|
Theorem | snss 3485 |
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.)
|
⊢ A ∈ V ⇒ ⊢ (A ∈ B ↔ {A}
⊆ B) |
|
Theorem | eldifsn 3486 |
Membership in a set with an element removed. (Contributed by NM,
10-Oct-2007.)
|
⊢ (A ∈ (B ∖
{𝐶}) ↔ (A ∈ B ∧ A ≠ 𝐶)) |
|
Theorem | eldifsni 3487 |
Membership in a set with an element removed. (Contributed by NM,
10-Mar-2015.)
|
⊢ (A ∈ (B ∖
{𝐶}) → A ≠ 𝐶) |
|
Theorem | neldifsn 3488 |
A is not in (B ∖ {A}). (Contributed by David Moews,
1-May-2017.)
|
⊢ ¬ A
∈ (B
∖ {A}) |
|
Theorem | neldifsnd 3489 |
A is not in (B ∖ {A}). Deduction form. (Contributed by
David Moews, 1-May-2017.)
|
⊢ (φ
→ ¬ A ∈ (B ∖
{A})) |
|
Theorem | rexdifsn 3490 |
Restricted existential quantification over a set with an element removed.
(Contributed by NM, 4-Feb-2015.)
|
⊢ (∃x ∈ (A ∖ {B})φ ↔
∃x
∈ A
(x ≠ B ∧ φ)) |
|
Theorem | snssg 3491 |
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.)
|
⊢ (A ∈ 𝑉 → (A ∈ B ↔ {A}
⊆ B)) |
|
Theorem | difsn 3492 |
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.)
|
⊢ (¬ A
∈ B
→ (B ∖ {A}) = B) |
|
Theorem | difprsnss 3493 |
Removal of a singleton from an unordered pair. (Contributed by NM,
16-Mar-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|
⊢ ({A,
B} ∖ {A}) ⊆ {B} |
|
Theorem | difprsn1 3494 |
Removal of a singleton from an unordered pair. (Contributed by Thierry
Arnoux, 4-Feb-2017.)
|
⊢ (A ≠
B → ({A, B} ∖
{A}) = {B}) |
|
Theorem | difprsn2 3495 |
Removal of a singleton from an unordered pair. (Contributed by Alexander
van der Vekens, 5-Oct-2017.)
|
⊢ (A ≠
B → ({A, B} ∖
{B}) = {A}) |
|
Theorem | diftpsn3 3496 |
Removal of a singleton from an unordered triple. (Contributed by
Alexander van der Vekens, 5-Oct-2017.)
|
⊢ ((A ≠
𝐶 ∧ B ≠ 𝐶) → ({A, B, 𝐶} ∖ {𝐶}) = {A, B}) |
|
Theorem | difsnb 3497 |
(B ∖ {A}) equals B if and only if A is not a member of
B.
Generalization of difsn 3492. (Contributed by David Moews,
1-May-2017.)
|
⊢ (¬ A
∈ B
↔ (B ∖ {A}) = B) |
|
Theorem | difsnpssim 3498 |
(B ∖ {A}) is a proper subclass of B if A is a member of
B. In
classical logic, the converse holds as well. (Contributed by
Jim Kingdon, 9-Aug-2018.)
|
⊢ (A ∈ B →
(B ∖ {A}) ⊊ B) |
|
Theorem | snssi 3499 |
The singleton of an element of a class is a subset of the class.
(Contributed by NM, 6-Jun-1994.)
|
⊢ (A ∈ B →
{A} ⊆ B) |
|
Theorem | snssd 3500 |
The singleton of an element of a class is a subset of the class
(deduction rule). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|
⊢ (φ
→ A ∈ B) ⇒ ⊢ (φ → {A} ⊆ B) |