Theorem List for Intuitionistic Logic Explorer - 3301-3400 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | ssrin 3301 |
Add right intersection to subclass relation. (Contributed by NM,
16-Aug-1994.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶)) |
|
Theorem | sslin 3302 |
Add left intersection to subclass relation. (Contributed by NM,
19-Oct-1999.)
|
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∩ 𝐴) ⊆ (𝐶 ∩ 𝐵)) |
|
Theorem | ssrind 3303 |
Add right intersection to subclass relation. (Contributed by Glauco
Siliprandi, 2-Jan-2022.)
|
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶)) |
|
Theorem | ss2in 3304 |
Intersection of subclasses. (Contributed by NM, 5-May-2000.)
|
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐷)) |
|
Theorem | ssinss1 3305 |
Intersection preserves subclass relationship. (Contributed by NM,
14-Sep-1999.)
|
⊢ (𝐴 ⊆ 𝐶 → (𝐴 ∩ 𝐵) ⊆ 𝐶) |
|
Theorem | inss 3306 |
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 3307 |
Absorption law for union. (Contributed by NM, 16-Apr-2006.)
|
⊢ (𝐴 ∪ (𝐴 ∩ 𝐵)) = 𝐴 |
|
Theorem | inabs 3308 |
Absorption law for intersection. (Contributed by NM, 16-Apr-2006.)
|
⊢ (𝐴 ∩ (𝐴 ∪ 𝐵)) = 𝐴 |
|
Theorem | dfss4st 3309* |
Subclass defined in terms of class difference. (Contributed by NM,
22-Mar-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|
⊢ (∀𝑥STAB 𝑥 ∈ 𝐴 → (𝐴 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝐴)) = 𝐴)) |
|
Theorem | ssddif 3310 |
Double complement and subset. Similar to ddifss 3314 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 3311 |
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 3312 |
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 3313 |
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 3314 |
Double complement under universal class. In classical logic (or given an
additional hypothesis, as in ddifnel 3207), this is equality rather than
subset. (Contributed by Jim Kingdon, 24-Jul-2018.)
|
⊢ 𝐴 ⊆ (V ∖ (V ∖ 𝐴)) |
|
Theorem | unssin 3315 |
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 3316 |
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 3317 |
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 3318 |
Intersection with universal complement. Remark in [Stoll] p. 20.
(Contributed by NM, 17-Aug-2004.)
|
⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵) |
|
Theorem | indif 3319 |
Intersection with class difference. Theorem 34 of [Suppes] p. 29.
(Contributed by NM, 17-Aug-2004.)
|
⊢ (𝐴 ∩ (𝐴 ∖ 𝐵)) = (𝐴 ∖ 𝐵) |
|
Theorem | indif2 3320 |
Bring an intersection in and out of a class difference. (Contributed by
Jeff Hankins, 15-Jul-2009.)
|
⊢ (𝐴 ∩ (𝐵 ∖ 𝐶)) = ((𝐴 ∩ 𝐵) ∖ 𝐶) |
|
Theorem | indif1 3321 |
Bring an intersection in and out of a class difference. (Contributed by
Mario Carneiro, 15-May-2015.)
|
⊢ ((𝐴 ∖ 𝐶) ∩ 𝐵) = ((𝐴 ∩ 𝐵) ∖ 𝐶) |
|
Theorem | indifcom 3322 |
Commutation law for intersection and difference. (Contributed by Scott
Fenton, 18-Feb-2013.)
|
⊢ (𝐴 ∩ (𝐵 ∖ 𝐶)) = (𝐵 ∩ (𝐴 ∖ 𝐶)) |
|
Theorem | indi 3323 |
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 3324 |
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 3325 |
Distributive law for intersection over union. Theorem 28 of [Suppes]
p. 27. (Contributed by NM, 30-Sep-2002.)
|
⊢ ((𝐴 ∪ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∪ (𝐵 ∩ 𝐶)) |
|
Theorem | undir 3326 |
Distributive law for union over intersection. Theorem 29 of [Suppes]
p. 27. (Contributed by NM, 30-Sep-2002.)
|
⊢ ((𝐴 ∩ 𝐵) ∪ 𝐶) = ((𝐴 ∪ 𝐶) ∩ (𝐵 ∪ 𝐶)) |
|
Theorem | uneqin 3327 |
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 3328 |
Distributive law for class difference. Theorem 39 of [Suppes] p. 29.
(Contributed by NM, 17-Aug-2004.)
|
⊢ (𝐴 ∖ (𝐵 ∪ 𝐶)) = ((𝐴 ∖ 𝐵) ∩ (𝐴 ∖ 𝐶)) |
|
Theorem | difundir 3329 |
Distributive law for class difference. (Contributed by NM,
17-Aug-2004.)
|
⊢ ((𝐴 ∪ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶)) |
|
Theorem | difindiss 3330 |
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 3331 |
Distributive law for class difference. (Contributed by NM,
17-Aug-2004.)
|
⊢ ((𝐴 ∩ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∩ (𝐵 ∖ 𝐶)) |
|
Theorem | indifdir 3332 |
Distribute intersection over difference. (Contributed by Scott Fenton,
14-Apr-2011.)
|
⊢ ((𝐴 ∖ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∖ (𝐵 ∩ 𝐶)) |
|
Theorem | difdif2ss 3333 |
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 3334 |
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 3335 |
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 3336 |
A relationship involving double difference and union. (Contributed by NM,
29-Aug-2004.)
|
⊢ (𝐴 ∖ (𝐵 ∪ 𝐶)) = ((𝐴 ∖ 𝐵) ∖ 𝐶) |
|
Theorem | undif3ss 3337 |
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 3338 |
Represent a set difference as an intersection with a larger difference.
(Contributed by Jeff Madsen, 2-Sep-2009.)
|
⊢ (𝐴 ⊆ 𝐶 → (𝐴 ∖ 𝐵) = ((𝐶 ∖ 𝐵) ∩ 𝐴)) |
|
Theorem | dif32 3339 |
Swap second and third argument of double difference. (Contributed by NM,
18-Aug-2004.)
|
⊢ ((𝐴 ∖ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∖ 𝐵) |
|
Theorem | difabs 3340 |
Absorption-like law for class difference: you can remove a class only
once. (Contributed by FL, 2-Aug-2009.)
|
⊢ ((𝐴 ∖ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵) |
|
Theorem | symdif1 3341 |
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 3342* |
Expressing symmetric difference with exclusive-or or two differences.
(Contributed by Jim Kingdon, 28-Jul-2018.)
|
⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐴)) = {𝑥 ∣ (𝑥 ∈ 𝐴 ⊻ 𝑥 ∈ 𝐵)} |
|
Theorem | unab 3343 |
Union of two class abstractions. (Contributed by NM, 29-Sep-2002.)
(Proof shortened by Andrew Salmon, 26-Jun-2011.)
|
⊢ ({𝑥 ∣ 𝜑} ∪ {𝑥 ∣ 𝜓}) = {𝑥 ∣ (𝜑 ∨ 𝜓)} |
|
Theorem | inab 3344 |
Intersection of two class abstractions. (Contributed by NM,
29-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|
⊢ ({𝑥 ∣ 𝜑} ∩ {𝑥 ∣ 𝜓}) = {𝑥 ∣ (𝜑 ∧ 𝜓)} |
|
Theorem | difab 3345 |
Difference of two class abstractions. (Contributed by NM, 23-Oct-2004.)
(Proof shortened by Andrew Salmon, 26-Jun-2011.)
|
⊢ ({𝑥 ∣ 𝜑} ∖ {𝑥 ∣ 𝜓}) = {𝑥 ∣ (𝜑 ∧ ¬ 𝜓)} |
|
Theorem | notab 3346 |
A class builder defined by a negation. (Contributed by FL,
18-Sep-2010.)
|
⊢ {𝑥 ∣ ¬ 𝜑} = (V ∖ {𝑥 ∣ 𝜑}) |
|
Theorem | unrab 3347 |
Union of two restricted class abstractions. (Contributed by NM,
25-Mar-2004.)
|
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∨ 𝜓)} |
|
Theorem | inrab 3348 |
Intersection of two restricted class abstractions. (Contributed by NM,
1-Sep-2006.)
|
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)} |
|
Theorem | inrab2 3349* |
Intersection with a restricted class abstraction. (Contributed by NM,
19-Nov-2007.)
|
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ 𝐵) = {𝑥 ∈ (𝐴 ∩ 𝐵) ∣ 𝜑} |
|
Theorem | difrab 3350 |
Difference of two restricted class abstractions. (Contributed by NM,
23-Oct-2004.)
|
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∖ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ ¬ 𝜓)} |
|
Theorem | dfrab2 3351* |
Alternate definition of restricted class abstraction. (Contributed by
NM, 20-Sep-2003.)
|
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = ({𝑥 ∣ 𝜑} ∩ 𝐴) |
|
Theorem | dfrab3 3352* |
Alternate definition of restricted class abstraction. (Contributed by
Mario Carneiro, 8-Sep-2013.)
|
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = (𝐴 ∩ {𝑥 ∣ 𝜑}) |
|
Theorem | notrab 3353* |
Complementation of restricted class abstractions. (Contributed by Mario
Carneiro, 3-Sep-2015.)
|
⊢ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝜑}) = {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} |
|
Theorem | dfrab3ss 3354* |
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 3355 |
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 3356* |
Transfer uniqueness to a smaller subclass. (Contributed by NM,
20-Oct-2005.)
|
⊢ (((𝐴 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) ∧ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜓)) → ∃!𝑥 ∈ 𝐴 𝜑) |
|
Theorem | reuss 3357* |
Transfer uniqueness to a smaller subclass. (Contributed by NM,
21-Aug-1999.)
|
⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜑) → ∃!𝑥 ∈ 𝐴 𝜑) |
|
Theorem | reuun1 3358* |
Transfer uniqueness to a smaller class. (Contributed by NM,
21-Oct-2005.)
|
⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ (𝐴 ∪ 𝐵)(𝜑 ∨ 𝜓)) → ∃!𝑥 ∈ 𝐴 𝜑) |
|
Theorem | reuun2 3359* |
Transfer uniqueness to a smaller or larger class. (Contributed by NM,
21-Oct-2005.)
|
⊢ (¬ ∃𝑥 ∈ 𝐵 𝜑 → (∃!𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜑)) |
|
Theorem | reupick 3360* |
Restricted uniqueness "picks" a member of a subclass. (Contributed
by
NM, 21-Aug-1999.)
|
⊢ (((𝐴 ⊆ 𝐵 ∧ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜑)) ∧ 𝜑) → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
|
Theorem | reupick3 3361* |
Restricted uniqueness "picks" a member of a subclass. (Contributed
by
Mario Carneiro, 19-Nov-2016.)
|
⊢ ((∃!𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ∧ 𝑥 ∈ 𝐴) → (𝜑 → 𝜓)) |
|
Theorem | reupick2 3362* |
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 3363 |
Extend class notation to include the empty set.
|
class ∅ |
|
Definition | df-nul 3364 |
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 3365. (Contributed by NM, 5-Aug-1993.)
|
⊢ ∅ = (V ∖ V) |
|
Theorem | dfnul2 3365 |
Alternate definition of the empty set. Definition 5.14 of [TakeutiZaring]
p. 20. (Contributed by NM, 26-Dec-1996.)
|
⊢ ∅ = {𝑥 ∣ ¬ 𝑥 = 𝑥} |
|
Theorem | dfnul3 3366 |
Alternate definition of the empty set. (Contributed by NM,
25-Mar-2004.)
|
⊢ ∅ = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐴} |
|
Theorem | noel 3367 |
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 3368 |
If a set has elements, it is not empty. A set with elements is also
inhabited, see elex2 2702. (Contributed by NM, 31-Dec-1993.)
|
⊢ (𝐵 ∈ 𝐴 → ¬ 𝐴 = ∅) |
|
Theorem | ne0i 3369 |
If a set has elements, it is not empty. A set with elements is also
inhabited, see elex2 2702. (Contributed by NM, 31-Dec-1993.)
|
⊢ (𝐵 ∈ 𝐴 → 𝐴 ≠ ∅) |
|
Theorem | ne0d 3370 |
Deduction form of ne0i 3369. If a class has elements, then it is
nonempty. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|
⊢ (𝜑 → 𝐵 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ≠ ∅) |
|
Theorem | n0ii 3371 |
If a class has elements, then it is not empty. Inference associated
with n0i 3368. (Contributed by BJ, 15-Jul-2021.)
|
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ ¬ 𝐵 = ∅ |
|
Theorem | ne0ii 3372 |
If a class has elements, then it is nonempty. Inference associated with
ne0i 3369. (Contributed by Glauco Siliprandi,
11-Dec-2019.)
|
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ 𝐵 ≠ ∅ |
|
Theorem | vn0 3373 |
The universal class is not equal to the empty set. (Contributed by NM,
11-Sep-2008.)
|
⊢ V ≠ ∅ |
|
Theorem | vn0m 3374 |
The universal class is inhabited. (Contributed by Jim Kingdon,
17-Dec-2018.)
|
⊢ ∃𝑥 𝑥 ∈ V |
|
Theorem | n0rf 3375 |
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 3376 requires only that 𝑥 not be free in,
rather than not occur in, 𝐴. (Contributed by Jim Kingdon,
31-Jul-2018.)
|
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (∃𝑥 𝑥 ∈ 𝐴 → 𝐴 ≠ ∅) |
|
Theorem | n0r 3376* |
An inhabited class is nonempty. See n0rf 3375 for more discussion.
(Contributed by Jim Kingdon, 31-Jul-2018.)
|
⊢ (∃𝑥 𝑥 ∈ 𝐴 → 𝐴 ≠ ∅) |
|
Theorem | neq0r 3377* |
An inhabited class is nonempty. See n0rf 3375 for more discussion.
(Contributed by Jim Kingdon, 31-Jul-2018.)
|
⊢ (∃𝑥 𝑥 ∈ 𝐴 → ¬ 𝐴 = ∅) |
|
Theorem | reximdva0m 3378* |
Restricted existence deduced from inhabited class. (Contributed by Jim
Kingdon, 31-Jul-2018.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓) ⇒ ⊢ ((𝜑 ∧ ∃𝑥 𝑥 ∈ 𝐴) → ∃𝑥 ∈ 𝐴 𝜓) |
|
Theorem | n0mmoeu 3379* |
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 3380 |
Vacuous existential quantification is false. (Contributed by NM,
15-Oct-2003.)
|
⊢ ¬ ∃𝑥 ∈ ∅ 𝜑 |
|
Theorem | eq0 3381* |
The empty set has no elements. Theorem 2 of [Suppes] p. 22.
(Contributed by NM, 29-Aug-1993.)
|
⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴) |
|
Theorem | eqv 3382* |
The universe contains every set. (Contributed by NM, 11-Sep-2006.)
|
⊢ (𝐴 = V ↔ ∀𝑥 𝑥 ∈ 𝐴) |
|
Theorem | notm0 3383* |
A class is not inhabited if and only if it is empty. (Contributed by
Jim Kingdon, 1-Jul-2022.)
|
⊢ (¬ ∃𝑥 𝑥 ∈ 𝐴 ↔ 𝐴 = ∅) |
|
Theorem | nel0 3384* |
From the general negation of membership in 𝐴, infer that 𝐴 is
the empty set. (Contributed by BJ, 6-Oct-2018.)
|
⊢ ¬ 𝑥 ∈ 𝐴 ⇒ ⊢ 𝐴 = ∅ |
|
Theorem | 0el 3385* |
Membership of the empty set in another class. (Contributed by NM,
29-Jun-2004.)
|
⊢ (∅ ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ¬ 𝑦 ∈ 𝑥) |
|
Theorem | abvor0dc 3386* |
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 3387 |
Nonempty class abstraction. (Contributed by Jim Kingdon, 1-Aug-2018.)
|
⊢ (∃𝑥𝜑 → {𝑥 ∣ 𝜑} ≠ ∅) |
|
Theorem | abn0m 3388* |
Inhabited class abstraction. (Contributed by Jim Kingdon,
8-Jul-2022.)
|
⊢ (∃𝑦 𝑦 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑥𝜑) |
|
Theorem | rabn0r 3389 |
Nonempty restricted class abstraction. (Contributed by Jim Kingdon,
1-Aug-2018.)
|
⊢ (∃𝑥 ∈ 𝐴 𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅) |
|
Theorem | rabn0m 3390* |
Inhabited restricted class abstraction. (Contributed by Jim Kingdon,
18-Sep-2018.)
|
⊢ (∃𝑦 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∃𝑥 ∈ 𝐴 𝜑) |
|
Theorem | rab0 3391 |
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 3392 |
Condition for a restricted class abstraction to be empty. (Contributed
by Jeff Madsen, 7-Jun-2010.)
|
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑) |
|
Theorem | abeq0 3393 |
Condition for a class abstraction to be empty. (Contributed by Jim
Kingdon, 12-Aug-2018.)
|
⊢ ({𝑥 ∣ 𝜑} = ∅ ↔ ∀𝑥 ¬ 𝜑) |
|
Theorem | rabxmdc 3394* |
Law of excluded middle given decidability, in terms of restricted class
abstractions. (Contributed by Jim Kingdon, 2-Aug-2018.)
|
⊢ (∀𝑥DECID 𝜑 → 𝐴 = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑})) |
|
Theorem | rabnc 3395* |
Law of noncontradiction, in terms of restricted class abstractions.
(Contributed by Jeff Madsen, 20-Jun-2011.)
|
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}) = ∅ |
|
Theorem | un0 3396 |
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 3397 |
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 3398 |
The intersection of the empty set with a class is the empty set.
(Contributed by Glauco Siliprandi, 17-Aug-2020.)
|
⊢ (∅ ∩ 𝐴) = ∅ |
|
Theorem | inv1 3399 |
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 3400 |
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 |