Theorem List for Intuitionistic Logic Explorer - 3301-3400 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | inss 3301 |
Inclusion of an intersection of two classes. (Contributed by NM,
30-Oct-2014.)
|
⊢ ((𝐴 ⊆ 𝐶 ∨ 𝐵 ⊆ 𝐶) → (𝐴 ∩ 𝐵) ⊆ 𝐶) |
|
2.1.13.4 Combinations of difference, union, and
intersection of two classes
|
|
Theorem | unabs 3302 |
Absorption law for union. (Contributed by NM, 16-Apr-2006.)
|
⊢ (𝐴 ∪ (𝐴 ∩ 𝐵)) = 𝐴 |
|
Theorem | inabs 3303 |
Absorption law for intersection. (Contributed by NM, 16-Apr-2006.)
|
⊢ (𝐴 ∩ (𝐴 ∪ 𝐵)) = 𝐴 |
|
Theorem | dfss4st 3304* |
Subclass defined in terms of class difference. (Contributed by NM,
22-Mar-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|
⊢ (∀𝑥STAB 𝑥 ∈ 𝐴 → (𝐴 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝐴)) = 𝐴)) |
|
Theorem | ssddif 3305 |
Double complement and subset. Similar to ddifss 3309 but inside a class
𝐵 instead of the universal class V. In classical logic the
subset operation on the right hand side could be an equality (that is,
𝐴
⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝐴)) = 𝐴). (Contributed by Jim Kingdon,
24-Jul-2018.)
|
⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ (𝐵 ∖ (𝐵 ∖ 𝐴))) |
|
Theorem | unssdif 3306 |
Union of two classes and class difference. In classical logic this
would be an equality. (Contributed by Jim Kingdon, 24-Jul-2018.)
|
⊢ (𝐴 ∪ 𝐵) ⊆ (V ∖ ((V ∖ 𝐴) ∖ 𝐵)) |
|
Theorem | inssdif 3307 |
Intersection of two classes and class difference. In classical logic
this would be an equality. (Contributed by Jim Kingdon,
24-Jul-2018.)
|
⊢ (𝐴 ∩ 𝐵) ⊆ (𝐴 ∖ (V ∖ 𝐵)) |
|
Theorem | difin 3308 |
Difference with intersection. Theorem 33 of [Suppes] p. 29.
(Contributed by NM, 31-Mar-1998.) (Proof shortened by Andrew Salmon,
26-Jun-2011.)
|
⊢ (𝐴 ∖ (𝐴 ∩ 𝐵)) = (𝐴 ∖ 𝐵) |
|
Theorem | ddifss 3309 |
Double complement under universal class. In classical logic (or given an
additional hypothesis, as in ddifnel 3202), this is equality rather than
subset. (Contributed by Jim Kingdon, 24-Jul-2018.)
|
⊢ 𝐴 ⊆ (V ∖ (V ∖ 𝐴)) |
|
Theorem | unssin 3310 |
Union as a subset of class complement and intersection (De Morgan's
law). One direction of the definition of union in [Mendelson] p. 231.
This would be an equality, rather than subset, in classical logic.
(Contributed by Jim Kingdon, 25-Jul-2018.)
|
⊢ (𝐴 ∪ 𝐵) ⊆ (V ∖ ((V ∖ 𝐴) ∩ (V ∖ 𝐵))) |
|
Theorem | inssun 3311 |
Intersection in terms of class difference and union (De Morgan's law).
Similar to Exercise 4.10(n) of [Mendelson] p. 231. This would be an
equality, rather than subset, in classical logic. (Contributed by Jim
Kingdon, 25-Jul-2018.)
|
⊢ (𝐴 ∩ 𝐵) ⊆ (V ∖ ((V ∖ 𝐴) ∪ (V ∖ 𝐵))) |
|
Theorem | inssddif 3312 |
Intersection of two classes and class difference. In classical logic,
such as Exercise 4.10(q) of [Mendelson]
p. 231, this is an equality rather
than subset. (Contributed by Jim Kingdon, 26-Jul-2018.)
|
⊢ (𝐴 ∩ 𝐵) ⊆ (𝐴 ∖ (𝐴 ∖ 𝐵)) |
|
Theorem | invdif 3313 |
Intersection with universal complement. Remark in [Stoll] p. 20.
(Contributed by NM, 17-Aug-2004.)
|
⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵) |
|
Theorem | indif 3314 |
Intersection with class difference. Theorem 34 of [Suppes] p. 29.
(Contributed by NM, 17-Aug-2004.)
|
⊢ (𝐴 ∩ (𝐴 ∖ 𝐵)) = (𝐴 ∖ 𝐵) |
|
Theorem | indif2 3315 |
Bring an intersection in and out of a class difference. (Contributed by
Jeff Hankins, 15-Jul-2009.)
|
⊢ (𝐴 ∩ (𝐵 ∖ 𝐶)) = ((𝐴 ∩ 𝐵) ∖ 𝐶) |
|
Theorem | indif1 3316 |
Bring an intersection in and out of a class difference. (Contributed by
Mario Carneiro, 15-May-2015.)
|
⊢ ((𝐴 ∖ 𝐶) ∩ 𝐵) = ((𝐴 ∩ 𝐵) ∖ 𝐶) |
|
Theorem | indifcom 3317 |
Commutation law for intersection and difference. (Contributed by Scott
Fenton, 18-Feb-2013.)
|
⊢ (𝐴 ∩ (𝐵 ∖ 𝐶)) = (𝐵 ∩ (𝐴 ∖ 𝐶)) |
|
Theorem | indi 3318 |
Distributive law for intersection over union. Exercise 10 of
[TakeutiZaring] p. 17.
(Contributed by NM, 30-Sep-2002.) (Proof
shortened by Andrew Salmon, 26-Jun-2011.)
|
⊢ (𝐴 ∩ (𝐵 ∪ 𝐶)) = ((𝐴 ∩ 𝐵) ∪ (𝐴 ∩ 𝐶)) |
|
Theorem | undi 3319 |
Distributive law for union over intersection. Exercise 11 of
[TakeutiZaring] p. 17.
(Contributed by NM, 30-Sep-2002.) (Proof
shortened by Andrew Salmon, 26-Jun-2011.)
|
⊢ (𝐴 ∪ (𝐵 ∩ 𝐶)) = ((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ 𝐶)) |
|
Theorem | indir 3320 |
Distributive law for intersection over union. Theorem 28 of [Suppes]
p. 27. (Contributed by NM, 30-Sep-2002.)
|
⊢ ((𝐴 ∪ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∪ (𝐵 ∩ 𝐶)) |
|
Theorem | undir 3321 |
Distributive law for union over intersection. Theorem 29 of [Suppes]
p. 27. (Contributed by NM, 30-Sep-2002.)
|
⊢ ((𝐴 ∩ 𝐵) ∪ 𝐶) = ((𝐴 ∪ 𝐶) ∩ (𝐵 ∪ 𝐶)) |
|
Theorem | uneqin 3322 |
Equality of union and intersection implies equality of their arguments.
(Contributed by NM, 16-Apr-2006.) (Proof shortened by Andrew Salmon,
26-Jun-2011.)
|
⊢ ((𝐴 ∪ 𝐵) = (𝐴 ∩ 𝐵) ↔ 𝐴 = 𝐵) |
|
Theorem | difundi 3323 |
Distributive law for class difference. Theorem 39 of [Suppes] p. 29.
(Contributed by NM, 17-Aug-2004.)
|
⊢ (𝐴 ∖ (𝐵 ∪ 𝐶)) = ((𝐴 ∖ 𝐵) ∩ (𝐴 ∖ 𝐶)) |
|
Theorem | difundir 3324 |
Distributive law for class difference. (Contributed by NM,
17-Aug-2004.)
|
⊢ ((𝐴 ∪ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶)) |
|
Theorem | difindiss 3325 |
Distributive law for class difference. In classical logic, for example,
theorem 40 of [Suppes] p. 29, this is an
equality instead of subset.
(Contributed by Jim Kingdon, 26-Jul-2018.)
|
⊢ ((𝐴 ∖ 𝐵) ∪ (𝐴 ∖ 𝐶)) ⊆ (𝐴 ∖ (𝐵 ∩ 𝐶)) |
|
Theorem | difindir 3326 |
Distributive law for class difference. (Contributed by NM,
17-Aug-2004.)
|
⊢ ((𝐴 ∩ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∩ (𝐵 ∖ 𝐶)) |
|
Theorem | indifdir 3327 |
Distribute intersection over difference. (Contributed by Scott Fenton,
14-Apr-2011.)
|
⊢ ((𝐴 ∖ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∖ (𝐵 ∩ 𝐶)) |
|
Theorem | difdif2ss 3328 |
Set difference with a set difference. In classical logic this would be
equality rather than subset. (Contributed by Jim Kingdon,
27-Jul-2018.)
|
⊢ ((𝐴 ∖ 𝐵) ∪ (𝐴 ∩ 𝐶)) ⊆ (𝐴 ∖ (𝐵 ∖ 𝐶)) |
|
Theorem | undm 3329 |
De Morgan's law for union. Theorem 5.2(13) of [Stoll] p. 19.
(Contributed by NM, 18-Aug-2004.)
|
⊢ (V ∖ (𝐴 ∪ 𝐵)) = ((V ∖ 𝐴) ∩ (V ∖ 𝐵)) |
|
Theorem | indmss 3330 |
De Morgan's law for intersection. In classical logic, this would be
equality rather than subset, as in Theorem 5.2(13') of [Stoll] p. 19.
(Contributed by Jim Kingdon, 27-Jul-2018.)
|
⊢ ((V ∖ 𝐴) ∪ (V ∖ 𝐵)) ⊆ (V ∖ (𝐴 ∩ 𝐵)) |
|
Theorem | difun1 3331 |
A relationship involving double difference and union. (Contributed by NM,
29-Aug-2004.)
|
⊢ (𝐴 ∖ (𝐵 ∪ 𝐶)) = ((𝐴 ∖ 𝐵) ∖ 𝐶) |
|
Theorem | undif3ss 3332 |
A subset relationship involving class union and class difference. In
classical logic, this would be equality rather than subset, as in the
first equality of Exercise 13 of [TakeutiZaring] p. 22. (Contributed by
Jim Kingdon, 28-Jul-2018.)
|
⊢ (𝐴 ∪ (𝐵 ∖ 𝐶)) ⊆ ((𝐴 ∪ 𝐵) ∖ (𝐶 ∖ 𝐴)) |
|
Theorem | difin2 3333 |
Represent a set difference as an intersection with a larger difference.
(Contributed by Jeff Madsen, 2-Sep-2009.)
|
⊢ (𝐴 ⊆ 𝐶 → (𝐴 ∖ 𝐵) = ((𝐶 ∖ 𝐵) ∩ 𝐴)) |
|
Theorem | dif32 3334 |
Swap second and third argument of double difference. (Contributed by NM,
18-Aug-2004.)
|
⊢ ((𝐴 ∖ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∖ 𝐵) |
|
Theorem | difabs 3335 |
Absorption-like law for class difference: you can remove a class only
once. (Contributed by FL, 2-Aug-2009.)
|
⊢ ((𝐴 ∖ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵) |
|
Theorem | symdif1 3336 |
Two ways to express symmetric difference. This theorem shows the
equivalence of the definition of symmetric difference in [Stoll] p. 13 and
the restated definition in Example 4.1 of [Stoll] p. 262. (Contributed by
NM, 17-Aug-2004.)
|
⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐴)) = ((𝐴 ∪ 𝐵) ∖ (𝐴 ∩ 𝐵)) |
|
2.1.13.5 Class abstractions with difference,
union, and intersection of two classes
|
|
Theorem | symdifxor 3337* |
Expressing symmetric difference with exclusive-or or two differences.
(Contributed by Jim Kingdon, 28-Jul-2018.)
|
⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐴)) = {𝑥 ∣ (𝑥 ∈ 𝐴 ⊻ 𝑥 ∈ 𝐵)} |
|
Theorem | unab 3338 |
Union of two class abstractions. (Contributed by NM, 29-Sep-2002.)
(Proof shortened by Andrew Salmon, 26-Jun-2011.)
|
⊢ ({𝑥 ∣ 𝜑} ∪ {𝑥 ∣ 𝜓}) = {𝑥 ∣ (𝜑 ∨ 𝜓)} |
|
Theorem | inab 3339 |
Intersection of two class abstractions. (Contributed by NM,
29-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|
⊢ ({𝑥 ∣ 𝜑} ∩ {𝑥 ∣ 𝜓}) = {𝑥 ∣ (𝜑 ∧ 𝜓)} |
|
Theorem | difab 3340 |
Difference of two class abstractions. (Contributed by NM, 23-Oct-2004.)
(Proof shortened by Andrew Salmon, 26-Jun-2011.)
|
⊢ ({𝑥 ∣ 𝜑} ∖ {𝑥 ∣ 𝜓}) = {𝑥 ∣ (𝜑 ∧ ¬ 𝜓)} |
|
Theorem | notab 3341 |
A class builder defined by a negation. (Contributed by FL,
18-Sep-2010.)
|
⊢ {𝑥 ∣ ¬ 𝜑} = (V ∖ {𝑥 ∣ 𝜑}) |
|
Theorem | unrab 3342 |
Union of two restricted class abstractions. (Contributed by NM,
25-Mar-2004.)
|
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∨ 𝜓)} |
|
Theorem | inrab 3343 |
Intersection of two restricted class abstractions. (Contributed by NM,
1-Sep-2006.)
|
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)} |
|
Theorem | inrab2 3344* |
Intersection with a restricted class abstraction. (Contributed by NM,
19-Nov-2007.)
|
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ 𝐵) = {𝑥 ∈ (𝐴 ∩ 𝐵) ∣ 𝜑} |
|
Theorem | difrab 3345 |
Difference of two restricted class abstractions. (Contributed by NM,
23-Oct-2004.)
|
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∖ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ ¬ 𝜓)} |
|
Theorem | dfrab2 3346* |
Alternate definition of restricted class abstraction. (Contributed by
NM, 20-Sep-2003.)
|
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = ({𝑥 ∣ 𝜑} ∩ 𝐴) |
|
Theorem | dfrab3 3347* |
Alternate definition of restricted class abstraction. (Contributed by
Mario Carneiro, 8-Sep-2013.)
|
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = (𝐴 ∩ {𝑥 ∣ 𝜑}) |
|
Theorem | notrab 3348* |
Complementation of restricted class abstractions. (Contributed by Mario
Carneiro, 3-Sep-2015.)
|
⊢ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝜑}) = {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} |
|
Theorem | dfrab3ss 3349* |
Restricted class abstraction with a common superset. (Contributed by
Stefan O'Rear, 12-Sep-2015.) (Proof shortened by Mario Carneiro,
8-Nov-2015.)
|
⊢ (𝐴 ⊆ 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = (𝐴 ∩ {𝑥 ∈ 𝐵 ∣ 𝜑})) |
|
Theorem | rabun2 3350 |
Abstraction restricted to a union. (Contributed by Stefan O'Rear,
5-Feb-2015.)
|
⊢ {𝑥 ∈ (𝐴 ∪ 𝐵) ∣ 𝜑} = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐵 ∣ 𝜑}) |
|
2.1.13.6 Restricted uniqueness with difference,
union, and intersection
|
|
Theorem | reuss2 3351* |
Transfer uniqueness to a smaller subclass. (Contributed by NM,
20-Oct-2005.)
|
⊢ (((𝐴 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) ∧ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜓)) → ∃!𝑥 ∈ 𝐴 𝜑) |
|
Theorem | reuss 3352* |
Transfer uniqueness to a smaller subclass. (Contributed by NM,
21-Aug-1999.)
|
⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜑) → ∃!𝑥 ∈ 𝐴 𝜑) |
|
Theorem | reuun1 3353* |
Transfer uniqueness to a smaller class. (Contributed by NM,
21-Oct-2005.)
|
⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ (𝐴 ∪ 𝐵)(𝜑 ∨ 𝜓)) → ∃!𝑥 ∈ 𝐴 𝜑) |
|
Theorem | reuun2 3354* |
Transfer uniqueness to a smaller or larger class. (Contributed by NM,
21-Oct-2005.)
|
⊢ (¬ ∃𝑥 ∈ 𝐵 𝜑 → (∃!𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜑)) |
|
Theorem | reupick 3355* |
Restricted uniqueness "picks" a member of a subclass. (Contributed
by
NM, 21-Aug-1999.)
|
⊢ (((𝐴 ⊆ 𝐵 ∧ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜑)) ∧ 𝜑) → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
|
Theorem | reupick3 3356* |
Restricted uniqueness "picks" a member of a subclass. (Contributed
by
Mario Carneiro, 19-Nov-2016.)
|
⊢ ((∃!𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ∧ 𝑥 ∈ 𝐴) → (𝜑 → 𝜓)) |
|
Theorem | reupick2 3357* |
Restricted uniqueness "picks" a member of a subclass. (Contributed
by
Mario Carneiro, 15-Dec-2013.) (Proof shortened by Mario Carneiro,
19-Nov-2016.)
|
⊢ (((∀𝑥 ∈ 𝐴 (𝜓 → 𝜑) ∧ ∃𝑥 ∈ 𝐴 𝜓 ∧ ∃!𝑥 ∈ 𝐴 𝜑) ∧ 𝑥 ∈ 𝐴) → (𝜑 ↔ 𝜓)) |
|
2.1.14 The empty set
|
|
Syntax | c0 3358 |
Extend class notation to include the empty set.
|
class ∅ |
|
Definition | df-nul 3359 |
Define the empty set. Special case of Exercise 4.10(o) of [Mendelson]
p. 231. For a more traditional definition, but requiring a dummy
variable, see dfnul2 3360. (Contributed by NM, 5-Aug-1993.)
|
⊢ ∅ = (V ∖ V) |
|
Theorem | dfnul2 3360 |
Alternate definition of the empty set. Definition 5.14 of [TakeutiZaring]
p. 20. (Contributed by NM, 26-Dec-1996.)
|
⊢ ∅ = {𝑥 ∣ ¬ 𝑥 = 𝑥} |
|
Theorem | dfnul3 3361 |
Alternate definition of the empty set. (Contributed by NM,
25-Mar-2004.)
|
⊢ ∅ = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐴} |
|
Theorem | noel 3362 |
The empty set has no elements. Theorem 6.14 of [Quine] p. 44.
(Contributed by NM, 5-Aug-1993.) (Proof shortened by Mario Carneiro,
1-Sep-2015.)
|
⊢ ¬ 𝐴 ∈ ∅ |
|
Theorem | n0i 3363 |
If a set has elements, it is not empty. A set with elements is also
inhabited, see elex2 2697. (Contributed by NM, 31-Dec-1993.)
|
⊢ (𝐵 ∈ 𝐴 → ¬ 𝐴 = ∅) |
|
Theorem | ne0i 3364 |
If a set has elements, it is not empty. A set with elements is also
inhabited, see elex2 2697. (Contributed by NM, 31-Dec-1993.)
|
⊢ (𝐵 ∈ 𝐴 → 𝐴 ≠ ∅) |
|
Theorem | ne0d 3365 |
Deduction form of ne0i 3364. If a class has elements, then it is
nonempty. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|
⊢ (𝜑 → 𝐵 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ≠ ∅) |
|
Theorem | n0ii 3366 |
If a class has elements, then it is not empty. Inference associated
with n0i 3363. (Contributed by BJ, 15-Jul-2021.)
|
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ ¬ 𝐵 = ∅ |
|
Theorem | ne0ii 3367 |
If a class has elements, then it is nonempty. Inference associated with
ne0i 3364. (Contributed by Glauco Siliprandi,
11-Dec-2019.)
|
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ 𝐵 ≠ ∅ |
|
Theorem | vn0 3368 |
The universal class is not equal to the empty set. (Contributed by NM,
11-Sep-2008.)
|
⊢ V ≠ ∅ |
|
Theorem | vn0m 3369 |
The universal class is inhabited. (Contributed by Jim Kingdon,
17-Dec-2018.)
|
⊢ ∃𝑥 𝑥 ∈ V |
|
Theorem | n0rf 3370 |
An inhabited class is nonempty. Following the Definition of [Bauer],
p. 483, we call a class 𝐴 nonempty if 𝐴 ≠ ∅ and
inhabited if
it has at least one element. In classical logic these two concepts are
equivalent, for example see Proposition 5.17(1) of [TakeutiZaring]
p. 20. This version of n0r 3371 requires only that 𝑥 not be free in,
rather than not occur in, 𝐴. (Contributed by Jim Kingdon,
31-Jul-2018.)
|
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (∃𝑥 𝑥 ∈ 𝐴 → 𝐴 ≠ ∅) |
|
Theorem | n0r 3371* |
An inhabited class is nonempty. See n0rf 3370 for more discussion.
(Contributed by Jim Kingdon, 31-Jul-2018.)
|
⊢ (∃𝑥 𝑥 ∈ 𝐴 → 𝐴 ≠ ∅) |
|
Theorem | neq0r 3372* |
An inhabited class is nonempty. See n0rf 3370 for more discussion.
(Contributed by Jim Kingdon, 31-Jul-2018.)
|
⊢ (∃𝑥 𝑥 ∈ 𝐴 → ¬ 𝐴 = ∅) |
|
Theorem | reximdva0m 3373* |
Restricted existence deduced from inhabited class. (Contributed by Jim
Kingdon, 31-Jul-2018.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓) ⇒ ⊢ ((𝜑 ∧ ∃𝑥 𝑥 ∈ 𝐴) → ∃𝑥 ∈ 𝐴 𝜓) |
|
Theorem | n0mmoeu 3374* |
A case of equivalence of "at most one" and "only one". If
a class is
inhabited, that class having at most one element is equivalent to it
having only one element. (Contributed by Jim Kingdon, 31-Jul-2018.)
|
⊢ (∃𝑥 𝑥 ∈ 𝐴 → (∃*𝑥 𝑥 ∈ 𝐴 ↔ ∃!𝑥 𝑥 ∈ 𝐴)) |
|
Theorem | rex0 3375 |
Vacuous existential quantification is false. (Contributed by NM,
15-Oct-2003.)
|
⊢ ¬ ∃𝑥 ∈ ∅ 𝜑 |
|
Theorem | eq0 3376* |
The empty set has no elements. Theorem 2 of [Suppes] p. 22.
(Contributed by NM, 29-Aug-1993.)
|
⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴) |
|
Theorem | eqv 3377* |
The universe contains every set. (Contributed by NM, 11-Sep-2006.)
|
⊢ (𝐴 = V ↔ ∀𝑥 𝑥 ∈ 𝐴) |
|
Theorem | notm0 3378* |
A class is not inhabited if and only if it is empty. (Contributed by
Jim Kingdon, 1-Jul-2022.)
|
⊢ (¬ ∃𝑥 𝑥 ∈ 𝐴 ↔ 𝐴 = ∅) |
|
Theorem | nel0 3379* |
From the general negation of membership in 𝐴, infer that 𝐴 is
the empty set. (Contributed by BJ, 6-Oct-2018.)
|
⊢ ¬ 𝑥 ∈ 𝐴 ⇒ ⊢ 𝐴 = ∅ |
|
Theorem | 0el 3380* |
Membership of the empty set in another class. (Contributed by NM,
29-Jun-2004.)
|
⊢ (∅ ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ¬ 𝑦 ∈ 𝑥) |
|
Theorem | abvor0dc 3381* |
The class builder of a decidable proposition not containing the
abstraction variable is either the universal class or the empty set.
(Contributed by Jim Kingdon, 1-Aug-2018.)
|
⊢ (DECID 𝜑 → ({𝑥 ∣ 𝜑} = V ∨ {𝑥 ∣ 𝜑} = ∅)) |
|
Theorem | abn0r 3382 |
Nonempty class abstraction. (Contributed by Jim Kingdon, 1-Aug-2018.)
|
⊢ (∃𝑥𝜑 → {𝑥 ∣ 𝜑} ≠ ∅) |
|
Theorem | abn0m 3383* |
Inhabited class abstraction. (Contributed by Jim Kingdon,
8-Jul-2022.)
|
⊢ (∃𝑦 𝑦 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑥𝜑) |
|
Theorem | rabn0r 3384 |
Nonempty restricted class abstraction. (Contributed by Jim Kingdon,
1-Aug-2018.)
|
⊢ (∃𝑥 ∈ 𝐴 𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅) |
|
Theorem | rabn0m 3385* |
Inhabited restricted class abstraction. (Contributed by Jim Kingdon,
18-Sep-2018.)
|
⊢ (∃𝑦 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∃𝑥 ∈ 𝐴 𝜑) |
|
Theorem | rab0 3386 |
Any restricted class abstraction restricted to the empty set is empty.
(Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon,
26-Jun-2011.)
|
⊢ {𝑥 ∈ ∅ ∣ 𝜑} = ∅ |
|
Theorem | rabeq0 3387 |
Condition for a restricted class abstraction to be empty. (Contributed
by Jeff Madsen, 7-Jun-2010.)
|
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑) |
|
Theorem | abeq0 3388 |
Condition for a class abstraction to be empty. (Contributed by Jim
Kingdon, 12-Aug-2018.)
|
⊢ ({𝑥 ∣ 𝜑} = ∅ ↔ ∀𝑥 ¬ 𝜑) |
|
Theorem | rabxmdc 3389* |
Law of excluded middle given decidability, in terms of restricted class
abstractions. (Contributed by Jim Kingdon, 2-Aug-2018.)
|
⊢ (∀𝑥DECID 𝜑 → 𝐴 = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑})) |
|
Theorem | rabnc 3390* |
Law of noncontradiction, in terms of restricted class abstractions.
(Contributed by Jeff Madsen, 20-Jun-2011.)
|
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}) = ∅ |
|
Theorem | un0 3391 |
The union of a class with the empty set is itself. Theorem 24 of
[Suppes] p. 27. (Contributed by NM,
5-Aug-1993.)
|
⊢ (𝐴 ∪ ∅) = 𝐴 |
|
Theorem | in0 3392 |
The intersection of a class with the empty set is the empty set.
Theorem 16 of [Suppes] p. 26.
(Contributed by NM, 5-Aug-1993.)
|
⊢ (𝐴 ∩ ∅) = ∅ |
|
Theorem | 0in 3393 |
The intersection of the empty set with a class is the empty set.
(Contributed by Glauco Siliprandi, 17-Aug-2020.)
|
⊢ (∅ ∩ 𝐴) = ∅ |
|
Theorem | inv1 3394 |
The intersection of a class with the universal class is itself. Exercise
4.10(k) of [Mendelson] p. 231.
(Contributed by NM, 17-May-1998.)
|
⊢ (𝐴 ∩ V) = 𝐴 |
|
Theorem | unv 3395 |
The union of a class with the universal class is the universal class.
Exercise 4.10(l) of [Mendelson] p. 231.
(Contributed by NM,
17-May-1998.)
|
⊢ (𝐴 ∪ V) = V |
|
Theorem | 0ss 3396 |
The null set is a subset of any class. Part of Exercise 1 of
[TakeutiZaring] p. 22.
(Contributed by NM, 5-Aug-1993.)
|
⊢ ∅ ⊆ 𝐴 |
|
Theorem | ss0b 3397 |
Any subset of the empty set is empty. Theorem 5 of [Suppes] p. 23 and its
converse. (Contributed by NM, 17-Sep-2003.)
|
⊢ (𝐴 ⊆ ∅ ↔ 𝐴 = ∅) |
|
Theorem | ss0 3398 |
Any subset of the empty set is empty. Theorem 5 of [Suppes] p. 23.
(Contributed by NM, 13-Aug-1994.)
|
⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅) |
|
Theorem | sseq0 3399 |
A subclass of an empty class is empty. (Contributed by NM, 7-Mar-2007.)
(Proof shortened by Andrew Salmon, 26-Jun-2011.)
|
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅) |
|
Theorem | ssn0 3400 |
A class with a nonempty subclass is nonempty. (Contributed by NM,
17-Feb-2007.)
|
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → 𝐵 ≠ ∅) |