Theorem List for Intuitionistic Logic Explorer - 3501-3600 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | ralsns 3501* |
Substitution expressed in terms of quantification over a singleton.
(Contributed by Mario Carneiro, 23-Apr-2015.)
|
⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ [𝐴 / 𝑥]𝜑)) |
|
Theorem | rexsns 3502* |
Restricted existential quantification over a singleton. (Contributed by
Mario Carneiro, 23-Apr-2015.) (Revised by NM, 22-Aug-2018.)
|
⊢ (∃𝑥 ∈ {𝐴}𝜑 ↔ [𝐴 / 𝑥]𝜑) |
|
Theorem | ralsng 3503* |
Substitution expressed in terms of quantification over a singleton.
(Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro,
23-Apr-2015.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) |
|
Theorem | rexsng 3504* |
Restricted existential quantification over a singleton. (Contributed by
NM, 29-Jan-2012.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) |
|
Theorem | exsnrex 3505 |
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.)
|
⊢ (∃𝑥 𝑀 = {𝑥} ↔ ∃𝑥 ∈ 𝑀 𝑀 = {𝑥}) |
|
Theorem | ralsn 3506* |
Convert a quantification over a singleton to a substitution.
(Contributed by NM, 27-Apr-2009.)
|
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓) |
|
Theorem | rexsn 3507* |
Restricted existential quantification over a singleton. (Contributed by
Jeff Madsen, 5-Jan-2011.)
|
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓) |
|
Theorem | eltpg 3508 |
Members of an unordered triple of classes. (Contributed by FL,
2-Feb-2014.) (Proof shortened by Mario Carneiro, 11-Feb-2015.)
|
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵, 𝐶, 𝐷} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ∨ 𝐴 = 𝐷))) |
|
Theorem | eltpi 3509 |
A member of an unordered triple of classes is one of them. (Contributed
by Mario Carneiro, 11-Feb-2015.)
|
⊢ (𝐴 ∈ {𝐵, 𝐶, 𝐷} → (𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ∨ 𝐴 = 𝐷)) |
|
Theorem | eltp 3510 |
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 ⇒ ⊢ (𝐴 ∈ {𝐵, 𝐶, 𝐷} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ∨ 𝐴 = 𝐷)) |
|
Theorem | dftp2 3511* |
Alternate definition of unordered triple of classes. Special case of
Definition 5.3 of [TakeutiZaring]
p. 16. (Contributed by NM,
8-Apr-1994.)
|
⊢ {𝐴, 𝐵, 𝐶} = {𝑥 ∣ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶)} |
|
Theorem | nfpr 3512 |
Bound-variable hypothesis builder for unordered pairs. (Contributed by
NM, 14-Nov-1995.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥{𝐴, 𝐵} |
|
Theorem | ralprg 3513* |
Convert a quantification over a pair to a conjunction. (Contributed by
NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒))) |
|
Theorem | rexprg 3514* |
Convert a quantification over a pair to a disjunction. (Contributed by
NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∨ 𝜒))) |
|
Theorem | raltpg 3515* |
Convert a quantification over a triple to a conjunction. (Contributed
by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜃)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (∀𝑥 ∈ {𝐴, 𝐵, 𝐶}𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))) |
|
Theorem | rextpg 3516* |
Convert a quantification over a triple to a disjunction. (Contributed
by Mario Carneiro, 23-Apr-2015.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜃)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (∃𝑥 ∈ {𝐴, 𝐵, 𝐶}𝜑 ↔ (𝜓 ∨ 𝜒 ∨ 𝜃))) |
|
Theorem | ralpr 3517* |
Convert a quantification over a pair to a conjunction. (Contributed by
NM, 3-Jun-2007.) (Revised by Mario Carneiro, 23-Apr-2015.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) ⇒ ⊢ (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒)) |
|
Theorem | rexpr 3518* |
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 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) ⇒ ⊢ (∃𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∨ 𝜒)) |
|
Theorem | raltp 3519* |
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 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜃)) ⇒ ⊢ (∀𝑥 ∈ {𝐴, 𝐵, 𝐶}𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) |
|
Theorem | rextp 3520* |
Convert a quantification over a triple to a disjunction. (Contributed
by Mario Carneiro, 23-Apr-2015.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜃)) ⇒ ⊢ (∃𝑥 ∈ {𝐴, 𝐵, 𝐶}𝜑 ↔ (𝜓 ∨ 𝜒 ∨ 𝜃)) |
|
Theorem | sbcsng 3521* |
Substitution expressed in terms of quantification over a singleton.
(Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro,
23-Apr-2015.)
|
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥 ∈ {𝐴}𝜑)) |
|
Theorem | nfsn 3522 |
Bound-variable hypothesis builder for singletons. (Contributed by NM,
14-Nov-1995.)
|
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥{𝐴} |
|
Theorem | csbsng 3523 |
Distribute proper substitution through the singleton of a class.
(Contributed by Alan Sare, 10-Nov-2012.)
|
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{𝐵} = {⦋𝐴 / 𝑥⦌𝐵}) |
|
Theorem | disjsn 3524 |
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 3525 |
Intersection of distinct singletons is disjoint. (Contributed by NM,
25-May-1998.)
|
⊢ (𝐴 ≠ 𝐵 → ({𝐴} ∩ {𝐵}) = ∅) |
|
Theorem | disjpr2 3526 |
The intersection of distinct unordered pairs is disjoint. (Contributed by
Alexander van der Vekens, 11-Nov-2017.)
|
⊢ (((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ (𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷)) → ({𝐴, 𝐵} ∩ {𝐶, 𝐷}) = ∅) |
|
Theorem | snprc 3527 |
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 ↔ {𝐴} = ∅) |
|
Theorem | r19.12sn 3528* |
Special case of r19.12 2491 where its converse holds. (Contributed by
NM,
19-May-2008.) (Revised by Mario Carneiro, 23-Apr-2015.) (Revised by
BJ, 20-Dec-2021.)
|
⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ {𝐴}𝜑)) |
|
Theorem | rabsn 3529* |
Condition where a restricted class abstraction is a singleton.
(Contributed by NM, 28-May-2006.)
|
⊢ (𝐵 ∈ 𝐴 → {𝑥 ∈ 𝐴 ∣ 𝑥 = 𝐵} = {𝐵}) |
|
Theorem | rabrsndc 3530* |
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 𝜑 ⇒ ⊢ (𝑀 = {𝑥 ∈ {𝐴} ∣ 𝜑} → (𝑀 = ∅ ∨ 𝑀 = {𝐴})) |
|
Theorem | euabsn2 3531* |
Another way to express existential uniqueness of a wff: its class
abstraction is a singleton. (Contributed by Mario Carneiro,
14-Nov-2016.)
|
⊢ (∃!𝑥𝜑 ↔ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦}) |
|
Theorem | euabsn 3532 |
Another way to express existential uniqueness of a wff: its class
abstraction is a singleton. (Contributed by NM, 22-Feb-2004.)
|
⊢ (∃!𝑥𝜑 ↔ ∃𝑥{𝑥 ∣ 𝜑} = {𝑥}) |
|
Theorem | reusn 3533* |
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 3534 |
Restricted existential uniqueness determined by a singleton.
(Contributed by NM, 29-May-2006.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ {𝑥 ∣ 𝜑} = {𝐴}) → ∃!𝑥𝜑) |
|
Theorem | rabsneu 3535 |
Restricted existential uniqueness determined by a singleton.
(Contributed by NM, 29-May-2006.) (Revised by Mario Carneiro,
23-Dec-2016.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ {𝑥 ∈ 𝐵 ∣ 𝜑} = {𝐴}) → ∃!𝑥 ∈ 𝐵 𝜑) |
|
Theorem | eusn 3536* |
Two ways to express "𝐴 is a singleton." (Contributed
by NM,
30-Oct-2010.)
|
⊢ (∃!𝑥 𝑥 ∈ 𝐴 ↔ ∃𝑥 𝐴 = {𝑥}) |
|
Theorem | rabsnt 3537* |
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 3538 |
Commutative law for unordered pairs. (Contributed by NM, 5-Aug-1993.)
|
⊢ {𝐴, 𝐵} = {𝐵, 𝐴} |
|
Theorem | preq1 3539 |
Equality theorem for unordered pairs. (Contributed by NM,
29-Mar-1998.)
|
⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶}) |
|
Theorem | preq2 3540 |
Equality theorem for unordered pairs. (Contributed by NM, 5-Aug-1993.)
|
⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵}) |
|
Theorem | preq12 3541 |
Equality theorem for unordered pairs. (Contributed by NM,
19-Oct-2012.)
|
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → {𝐴, 𝐵} = {𝐶, 𝐷}) |
|
Theorem | preq1i 3542 |
Equality inference for unordered pairs. (Contributed by NM,
19-Oct-2012.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ {𝐴, 𝐶} = {𝐵, 𝐶} |
|
Theorem | preq2i 3543 |
Equality inference for unordered pairs. (Contributed by NM,
19-Oct-2012.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ {𝐶, 𝐴} = {𝐶, 𝐵} |
|
Theorem | preq12i 3544 |
Equality inference for unordered pairs. (Contributed by NM,
19-Oct-2012.)
|
⊢ 𝐴 = 𝐵
& ⊢ 𝐶 = 𝐷 ⇒ ⊢ {𝐴, 𝐶} = {𝐵, 𝐷} |
|
Theorem | preq1d 3545 |
Equality deduction for unordered pairs. (Contributed by NM,
19-Oct-2012.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → {𝐴, 𝐶} = {𝐵, 𝐶}) |
|
Theorem | preq2d 3546 |
Equality deduction for unordered pairs. (Contributed by NM,
19-Oct-2012.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → {𝐶, 𝐴} = {𝐶, 𝐵}) |
|
Theorem | preq12d 3547 |
Equality deduction for unordered pairs. (Contributed by NM,
19-Oct-2012.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → {𝐴, 𝐶} = {𝐵, 𝐷}) |
|
Theorem | tpeq1 3548 |
Equality theorem for unordered triples. (Contributed by NM,
13-Sep-2011.)
|
⊢ (𝐴 = 𝐵 → {𝐴, 𝐶, 𝐷} = {𝐵, 𝐶, 𝐷}) |
|
Theorem | tpeq2 3549 |
Equality theorem for unordered triples. (Contributed by NM,
13-Sep-2011.)
|
⊢ (𝐴 = 𝐵 → {𝐶, 𝐴, 𝐷} = {𝐶, 𝐵, 𝐷}) |
|
Theorem | tpeq3 3550 |
Equality theorem for unordered triples. (Contributed by NM,
13-Sep-2011.)
|
⊢ (𝐴 = 𝐵 → {𝐶, 𝐷, 𝐴} = {𝐶, 𝐷, 𝐵}) |
|
Theorem | tpeq1d 3551 |
Equality theorem for unordered triples. (Contributed by NM,
22-Jun-2014.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → {𝐴, 𝐶, 𝐷} = {𝐵, 𝐶, 𝐷}) |
|
Theorem | tpeq2d 3552 |
Equality theorem for unordered triples. (Contributed by NM,
22-Jun-2014.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → {𝐶, 𝐴, 𝐷} = {𝐶, 𝐵, 𝐷}) |
|
Theorem | tpeq3d 3553 |
Equality theorem for unordered triples. (Contributed by NM,
22-Jun-2014.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → {𝐶, 𝐷, 𝐴} = {𝐶, 𝐷, 𝐵}) |
|
Theorem | tpeq123d 3554 |
Equality theorem for unordered triples. (Contributed by NM,
22-Jun-2014.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐶 = 𝐷)
& ⊢ (𝜑 → 𝐸 = 𝐹) ⇒ ⊢ (𝜑 → {𝐴, 𝐶, 𝐸} = {𝐵, 𝐷, 𝐹}) |
|
Theorem | tprot 3555 |
Rotation of the elements of an unordered triple. (Contributed by Alan
Sare, 24-Oct-2011.)
|
⊢ {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴} |
|
Theorem | tpcoma 3556 |
Swap 1st and 2nd members of an undordered triple. (Contributed by NM,
22-May-2015.)
|
⊢ {𝐴, 𝐵, 𝐶} = {𝐵, 𝐴, 𝐶} |
|
Theorem | tpcomb 3557 |
Swap 2nd and 3rd members of an undordered triple. (Contributed by NM,
22-May-2015.)
|
⊢ {𝐴, 𝐵, 𝐶} = {𝐴, 𝐶, 𝐵} |
|
Theorem | tpass 3558 |
Split off the first element of an unordered triple. (Contributed by Mario
Carneiro, 5-Jan-2016.)
|
⊢ {𝐴, 𝐵, 𝐶} = ({𝐴} ∪ {𝐵, 𝐶}) |
|
Theorem | qdass 3559 |
Two ways to write an unordered quadruple. (Contributed by Mario Carneiro,
5-Jan-2016.)
|
⊢ ({𝐴, 𝐵} ∪ {𝐶, 𝐷}) = ({𝐴, 𝐵, 𝐶} ∪ {𝐷}) |
|
Theorem | qdassr 3560 |
Two ways to write an unordered quadruple. (Contributed by Mario Carneiro,
5-Jan-2016.)
|
⊢ ({𝐴, 𝐵} ∪ {𝐶, 𝐷}) = ({𝐴} ∪ {𝐵, 𝐶, 𝐷}) |
|
Theorem | tpidm12 3561 |
Unordered triple {𝐴, 𝐴, 𝐵} is just an overlong way to write
{𝐴,
𝐵}. (Contributed by
David A. Wheeler, 10-May-2015.)
|
⊢ {𝐴, 𝐴, 𝐵} = {𝐴, 𝐵} |
|
Theorem | tpidm13 3562 |
Unordered triple {𝐴, 𝐵, 𝐴} is just an overlong way to write
{𝐴,
𝐵}. (Contributed by
David A. Wheeler, 10-May-2015.)
|
⊢ {𝐴, 𝐵, 𝐴} = {𝐴, 𝐵} |
|
Theorem | tpidm23 3563 |
Unordered triple {𝐴, 𝐵, 𝐵} is just an overlong way to write
{𝐴,
𝐵}. (Contributed by
David A. Wheeler, 10-May-2015.)
|
⊢ {𝐴, 𝐵, 𝐵} = {𝐴, 𝐵} |
|
Theorem | tpidm 3564 |
Unordered triple {𝐴, 𝐴, 𝐴} is just an overlong way to write
{𝐴}. (Contributed by David A. Wheeler,
10-May-2015.)
|
⊢ {𝐴, 𝐴, 𝐴} = {𝐴} |
|
Theorem | tppreq3 3565 |
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 3566 |
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 3567 |
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 3568 |
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 3569 |
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 3570 |
A proper class vanishes in an unordered pair. (Contributed by NM,
5-Aug-1993.)
|
⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵}) |
|
Theorem | prprc2 3571 |
A proper class vanishes in an unordered pair. (Contributed by NM,
22-Mar-2006.)
|
⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴}) |
|
Theorem | prprc 3572 |
An unordered pair containing two proper classes is the empty set.
(Contributed by NM, 22-Mar-2006.)
|
⊢ ((¬ 𝐴 ∈ V ∧ ¬ 𝐵 ∈ V) → {𝐴, 𝐵} = ∅) |
|
Theorem | tpid1 3573 |
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 3574 |
Closed theorem form of tpid1 3573. (Contributed by Glauco Siliprandi,
23-Oct-2021.)
|
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ {𝐴, 𝐶, 𝐷}) |
|
Theorem | tpid2 3575 |
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 3576 |
Closed theorem form of tpid2 3575. (Contributed by Glauco Siliprandi,
23-Oct-2021.)
|
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ {𝐶, 𝐴, 𝐷}) |
|
Theorem | tpid3g 3577 |
Closed theorem form of tpid3 3578. (Contributed by Alan Sare,
24-Oct-2011.)
|
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ {𝐶, 𝐷, 𝐴}) |
|
Theorem | tpid3 3578 |
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 3579 |
The singleton of a set is not empty. (Contributed by NM, 14-Dec-2008.)
|
⊢ (𝐴 ∈ 𝑉 → {𝐴} ≠ ∅) |
|
Theorem | snmg 3580* |
The singleton of a set is inhabited. (Contributed by Jim Kingdon,
11-Aug-2018.)
|
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 ∈ {𝐴}) |
|
Theorem | snnz 3581 |
The singleton of a set is not empty. (Contributed by NM,
10-Apr-1994.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ {𝐴} ≠ ∅ |
|
Theorem | snm 3582* |
The singleton of a set is inhabited. (Contributed by Jim Kingdon,
11-Aug-2018.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ ∃𝑥 𝑥 ∈ {𝐴} |
|
Theorem | prmg 3583* |
A pair containing a set is inhabited. (Contributed by Jim Kingdon,
21-Sep-2018.)
|
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 ∈ {𝐴, 𝐵}) |
|
Theorem | prnz 3584 |
A pair containing a set is not empty. (Contributed by NM,
9-Apr-1994.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ {𝐴, 𝐵} ≠ ∅ |
|
Theorem | prm 3585* |
A pair containing a set is inhabited. (Contributed by Jim Kingdon,
21-Sep-2018.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ ∃𝑥 𝑥 ∈ {𝐴, 𝐵} |
|
Theorem | prnzg 3586 |
A pair containing a set is not empty. (Contributed by FL,
19-Sep-2011.)
|
⊢ (𝐴 ∈ 𝑉 → {𝐴, 𝐵} ≠ ∅) |
|
Theorem | tpnz 3587 |
A triplet containing a set is not empty. (Contributed by NM,
10-Apr-1994.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ {𝐴, 𝐵, 𝐶} ≠ ∅ |
|
Theorem | snss 3588 |
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 ⇒ ⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵) |
|
Theorem | eldifsn 3589 |
Membership in a set with an element removed. (Contributed by NM,
10-Oct-2007.)
|
⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶)) |
|
Theorem | ssdifsn 3590 |
Subset of a set with an element removed. (Contributed by Emmett Weisz,
7-Jul-2021.) (Proof shortened by JJ, 31-May-2022.)
|
⊢ (𝐴 ⊆ (𝐵 ∖ {𝐶}) ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐶 ∈ 𝐴)) |
|
Theorem | eldifsni 3591 |
Membership in a set with an element removed. (Contributed by NM,
10-Mar-2015.)
|
⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) → 𝐴 ≠ 𝐶) |
|
Theorem | neldifsn 3592 |
𝐴
is not in (𝐵 ∖ {𝐴}). (Contributed by David Moews,
1-May-2017.)
|
⊢ ¬ 𝐴 ∈ (𝐵 ∖ {𝐴}) |
|
Theorem | neldifsnd 3593 |
𝐴
is not in (𝐵 ∖ {𝐴}). Deduction form. (Contributed by
David Moews, 1-May-2017.)
|
⊢ (𝜑 → ¬ 𝐴 ∈ (𝐵 ∖ {𝐴})) |
|
Theorem | rexdifsn 3594 |
Restricted existential quantification over a set with an element removed.
(Contributed by NM, 4-Feb-2015.)
|
⊢ (∃𝑥 ∈ (𝐴 ∖ {𝐵})𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝑥 ≠ 𝐵 ∧ 𝜑)) |
|
Theorem | snssg 3595 |
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.)
|
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵)) |
|
Theorem | difsn 3596 |
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 3597 |
Removal of a singleton from an unordered pair. (Contributed by NM,
16-Mar-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|
⊢ ({𝐴, 𝐵} ∖ {𝐴}) ⊆ {𝐵} |
|
Theorem | difprsn1 3598 |
Removal of a singleton from an unordered pair. (Contributed by Thierry
Arnoux, 4-Feb-2017.)
|
⊢ (𝐴 ≠ 𝐵 → ({𝐴, 𝐵} ∖ {𝐴}) = {𝐵}) |
|
Theorem | difprsn2 3599 |
Removal of a singleton from an unordered pair. (Contributed by Alexander
van der Vekens, 5-Oct-2017.)
|
⊢ (𝐴 ≠ 𝐵 → ({𝐴, 𝐵} ∖ {𝐵}) = {𝐴}) |
|
Theorem | diftpsn3 3600 |
Removal of a singleton from an unordered triple. (Contributed by
Alexander van der Vekens, 5-Oct-2017.)
|
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = {𝐴, 𝐵}) |