Theorem List for Intuitionistic Logic Explorer - 3701-3800 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | prneimg 3701 |
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.)
|
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → (((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∨ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)) → {𝐴, 𝐵} ≠ {𝐶, 𝐷})) |
|
Theorem | preqsn 3702 |
Equivalence for a pair equal to a singleton. (Contributed by NM,
3-Jun-2008.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈
V ⇒ ⊢ ({𝐴, 𝐵} = {𝐶} ↔ (𝐴 = 𝐵 ∧ 𝐵 = 𝐶)) |
|
Theorem | dfopg 3703 |
Value of the ordered pair when the arguments are sets. (Contributed by
Mario Carneiro, 26-Apr-2015.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 〈𝐴, 𝐵〉 = {{𝐴}, {𝐴, 𝐵}}) |
|
Theorem | dfop 3704 |
Value of an ordered pair when the arguments are sets, with the
conclusion corresponding to Kuratowski's original definition.
(Contributed by NM, 25-Jun-1998.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ 〈𝐴, 𝐵〉 = {{𝐴}, {𝐴, 𝐵}} |
|
Theorem | opeq1 3705 |
Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.)
(Revised by Mario Carneiro, 26-Apr-2015.)
|
⊢ (𝐴 = 𝐵 → 〈𝐴, 𝐶〉 = 〈𝐵, 𝐶〉) |
|
Theorem | opeq2 3706 |
Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.)
(Revised by Mario Carneiro, 26-Apr-2015.)
|
⊢ (𝐴 = 𝐵 → 〈𝐶, 𝐴〉 = 〈𝐶, 𝐵〉) |
|
Theorem | opeq12 3707 |
Equality theorem for ordered pairs. (Contributed by NM, 28-May-1995.)
|
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → 〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉) |
|
Theorem | opeq1i 3708 |
Equality inference for ordered pairs. (Contributed by NM,
16-Dec-2006.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ 〈𝐴, 𝐶〉 = 〈𝐵, 𝐶〉 |
|
Theorem | opeq2i 3709 |
Equality inference for ordered pairs. (Contributed by NM,
16-Dec-2006.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ 〈𝐶, 𝐴〉 = 〈𝐶, 𝐵〉 |
|
Theorem | opeq12i 3710 |
Equality inference for ordered pairs. (Contributed by NM,
16-Dec-2006.) (Proof shortened by Eric Schmidt, 4-Apr-2007.)
|
⊢ 𝐴 = 𝐵
& ⊢ 𝐶 = 𝐷 ⇒ ⊢ 〈𝐴, 𝐶〉 = 〈𝐵, 𝐷〉 |
|
Theorem | opeq1d 3711 |
Equality deduction for ordered pairs. (Contributed by NM,
16-Dec-2006.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 〈𝐴, 𝐶〉 = 〈𝐵, 𝐶〉) |
|
Theorem | opeq2d 3712 |
Equality deduction for ordered pairs. (Contributed by NM,
16-Dec-2006.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 〈𝐶, 𝐴〉 = 〈𝐶, 𝐵〉) |
|
Theorem | opeq12d 3713 |
Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.)
(Proof shortened by Andrew Salmon, 29-Jun-2011.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → 〈𝐴, 𝐶〉 = 〈𝐵, 𝐷〉) |
|
Theorem | oteq1 3714 |
Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015.)
|
⊢ (𝐴 = 𝐵 → 〈𝐴, 𝐶, 𝐷〉 = 〈𝐵, 𝐶, 𝐷〉) |
|
Theorem | oteq2 3715 |
Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015.)
|
⊢ (𝐴 = 𝐵 → 〈𝐶, 𝐴, 𝐷〉 = 〈𝐶, 𝐵, 𝐷〉) |
|
Theorem | oteq3 3716 |
Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015.)
|
⊢ (𝐴 = 𝐵 → 〈𝐶, 𝐷, 𝐴〉 = 〈𝐶, 𝐷, 𝐵〉) |
|
Theorem | oteq1d 3717 |
Equality deduction for ordered triples. (Contributed by Mario Carneiro,
11-Jan-2017.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 〈𝐴, 𝐶, 𝐷〉 = 〈𝐵, 𝐶, 𝐷〉) |
|
Theorem | oteq2d 3718 |
Equality deduction for ordered triples. (Contributed by Mario Carneiro,
11-Jan-2017.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 〈𝐶, 𝐴, 𝐷〉 = 〈𝐶, 𝐵, 𝐷〉) |
|
Theorem | oteq3d 3719 |
Equality deduction for ordered triples. (Contributed by Mario Carneiro,
11-Jan-2017.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 〈𝐶, 𝐷, 𝐴〉 = 〈𝐶, 𝐷, 𝐵〉) |
|
Theorem | oteq123d 3720 |
Equality deduction for ordered triples. (Contributed by Mario Carneiro,
11-Jan-2017.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐶 = 𝐷)
& ⊢ (𝜑 → 𝐸 = 𝐹) ⇒ ⊢ (𝜑 → 〈𝐴, 𝐶, 𝐸〉 = 〈𝐵, 𝐷, 𝐹〉) |
|
Theorem | nfop 3721 |
Bound-variable hypothesis builder for ordered pairs. (Contributed by
NM, 14-Nov-1995.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥〈𝐴, 𝐵〉 |
|
Theorem | nfopd 3722 |
Deduction version of bound-variable hypothesis builder nfop 3721.
This
shows how the deduction version of a not-free theorem such as nfop 3721
can
be created from the corresponding not-free inference theorem.
(Contributed by NM, 4-Feb-2008.)
|
⊢ (𝜑 → Ⅎ𝑥𝐴)
& ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥〈𝐴, 𝐵〉) |
|
Theorem | opid 3723 |
The ordered pair 〈𝐴, 𝐴〉 in Kuratowski's
representation.
(Contributed by FL, 28-Dec-2011.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ 〈𝐴, 𝐴〉 = {{𝐴}} |
|
Theorem | ralunsn 3724* |
Restricted quantification over the union of a set and a singleton, using
implicit substitution. (Contributed by Paul Chapman, 17-Nov-2012.)
(Revised by Mario Carneiro, 23-Apr-2015.)
|
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐵 ∈ 𝐶 → (∀𝑥 ∈ (𝐴 ∪ {𝐵})𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))) |
|
Theorem | 2ralunsn 3725* |
Double restricted quantification over the union of a set and a
singleton, using implicit substitution. (Contributed by Paul Chapman,
17-Nov-2012.)
|
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝐵 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝐵 ∈ 𝐶 → (∀𝑥 ∈ (𝐴 ∪ {𝐵})∀𝑦 ∈ (𝐴 ∪ {𝐵})𝜑 ↔ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) ∧ (∀𝑦 ∈ 𝐴 𝜒 ∧ 𝜃)))) |
|
Theorem | opprc 3726 |
Expansion of an ordered pair when either member is a proper class.
(Contributed by Mario Carneiro, 26-Apr-2015.)
|
⊢ (¬ (𝐴 ∈ V ∧ 𝐵 ∈ V) → 〈𝐴, 𝐵〉 = ∅) |
|
Theorem | opprc1 3727 |
Expansion of an ordered pair when the first member is a proper class. See
also opprc 3726. (Contributed by NM, 10-Apr-2004.) (Revised
by Mario
Carneiro, 26-Apr-2015.)
|
⊢ (¬ 𝐴 ∈ V → 〈𝐴, 𝐵〉 = ∅) |
|
Theorem | opprc2 3728 |
Expansion of an ordered pair when the second member is a proper class.
See also opprc 3726. (Contributed by NM, 15-Nov-1994.) (Revised
by Mario
Carneiro, 26-Apr-2015.)
|
⊢ (¬ 𝐵 ∈ V → 〈𝐴, 𝐵〉 = ∅) |
|
Theorem | oprcl 3729 |
If an ordered pair has an element, then its arguments are sets.
(Contributed by Mario Carneiro, 26-Apr-2015.)
|
⊢ (𝐶 ∈ 〈𝐴, 𝐵〉 → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
|
Theorem | pwsnss 3730 |
The power set of a singleton. (Contributed by Jim Kingdon,
12-Aug-2018.)
|
⊢ {∅, {𝐴}} ⊆ 𝒫 {𝐴} |
|
Theorem | pwpw0ss 3731 |
Compute the power set of the power set of the empty set. (See pw0 3667
for
the power set of the empty set.) Theorem 90 of [Suppes] p. 48 (but with
subset in place of equality). (Contributed by Jim Kingdon,
12-Aug-2018.)
|
⊢ {∅, {∅}} ⊆ 𝒫
{∅} |
|
Theorem | pwprss 3732 |
The power set of an unordered pair. (Contributed by Jim Kingdon,
13-Aug-2018.)
|
⊢ ({∅, {𝐴}} ∪ {{𝐵}, {𝐴, 𝐵}}) ⊆ 𝒫 {𝐴, 𝐵} |
|
Theorem | pwtpss 3733 |
The power set of an unordered triple. (Contributed by Jim Kingdon,
13-Aug-2018.)
|
⊢ (({∅, {𝐴}} ∪ {{𝐵}, {𝐴, 𝐵}}) ∪ ({{𝐶}, {𝐴, 𝐶}} ∪ {{𝐵, 𝐶}, {𝐴, 𝐵, 𝐶}})) ⊆ 𝒫 {𝐴, 𝐵, 𝐶} |
|
Theorem | pwpwpw0ss 3734 |
Compute the power set of the power set of the power set of the empty set.
(See also pw0 3667 and pwpw0ss 3731.) (Contributed by Jim Kingdon,
13-Aug-2018.)
|
⊢ ({∅, {∅}} ∪ {{{∅}},
{∅, {∅}}}) ⊆ 𝒫 {∅, {∅}} |
|
Theorem | pwv 3735 |
The power class of the universe is the universe. Exercise 4.12(d) of
[Mendelson] p. 235. (Contributed by NM,
14-Sep-2003.)
|
⊢ 𝒫 V = V |
|
2.1.18 The union of a class
|
|
Syntax | cuni 3736 |
Extend class notation to include the union of a class (read: 'union
𝐴')
|
class ∪ 𝐴 |
|
Definition | df-uni 3737* |
Define the union of a class i.e. the collection of all members of the
members of the class. Definition 5.5 of [TakeutiZaring] p. 16. For
example, { { 1 , 3 } , { 1 , 8 } } = { 1 , 3 , 8 } . This is similar to
the union of two classes df-un 3075. (Contributed by NM, 23-Aug-1993.)
|
⊢ ∪ 𝐴 = {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴)} |
|
Theorem | dfuni2 3738* |
Alternate definition of class union. (Contributed by NM,
28-Jun-1998.)
|
⊢ ∪ 𝐴 = {𝑥 ∣ ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦} |
|
Theorem | eluni 3739* |
Membership in class union. (Contributed by NM, 22-May-1994.)
|
⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)) |
|
Theorem | eluni2 3740* |
Membership in class union. Restricted quantifier version. (Contributed
by NM, 31-Aug-1999.)
|
⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥) |
|
Theorem | elunii 3741 |
Membership in class union. (Contributed by NM, 24-Mar-1995.)
|
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ ∪ 𝐶) |
|
Theorem | nfuni 3742 |
Bound-variable hypothesis builder for union. (Contributed by NM,
30-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥∪
𝐴 |
|
Theorem | nfunid 3743 |
Deduction version of nfuni 3742. (Contributed by NM, 18-Feb-2013.)
|
⊢ (𝜑 → Ⅎ𝑥𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥∪ 𝐴) |
|
Theorem | csbunig 3744 |
Distribute proper substitution through the union of a class.
(Contributed by Alan Sare, 10-Nov-2012.)
|
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌∪
𝐵 = ∪ ⦋𝐴 / 𝑥⦌𝐵) |
|
Theorem | unieq 3745 |
Equality theorem for class union. Exercise 15 of [TakeutiZaring] p. 18.
(Contributed by NM, 10-Aug-1993.) (Proof shortened by Andrew Salmon,
29-Jun-2011.)
|
⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪
𝐵) |
|
Theorem | unieqi 3746 |
Inference of equality of two class unions. (Contributed by NM,
30-Aug-1993.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ ∪
𝐴 = ∪ 𝐵 |
|
Theorem | unieqd 3747 |
Deduction of equality of two class unions. (Contributed by NM,
21-Apr-1995.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ∪ 𝐴 = ∪
𝐵) |
|
Theorem | eluniab 3748* |
Membership in union of a class abstraction. (Contributed by NM,
11-Aug-1994.) (Revised by Mario Carneiro, 14-Nov-2016.)
|
⊢ (𝐴 ∈ ∪ {𝑥 ∣ 𝜑} ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝜑)) |
|
Theorem | elunirab 3749* |
Membership in union of a class abstraction. (Contributed by NM,
4-Oct-2006.)
|
⊢ (𝐴 ∈ ∪ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ ∃𝑥 ∈ 𝐵 (𝐴 ∈ 𝑥 ∧ 𝜑)) |
|
Theorem | unipr 3750 |
The union of a pair is the union of its members. Proposition 5.7 of
[TakeutiZaring] p. 16.
(Contributed by NM, 23-Aug-1993.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ ∪
{𝐴, 𝐵} = (𝐴 ∪ 𝐵) |
|
Theorem | uniprg 3751 |
The union of a pair is the union of its members. Proposition 5.7 of
[TakeutiZaring] p. 16.
(Contributed by NM, 25-Aug-2006.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∪
{𝐴, 𝐵} = (𝐴 ∪ 𝐵)) |
|
Theorem | unisn 3752 |
A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53.
(Contributed by NM, 30-Aug-1993.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ ∪
{𝐴} = 𝐴 |
|
Theorem | unisng 3753 |
A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53.
(Contributed by NM, 13-Aug-2002.)
|
⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴) |
|
Theorem | dfnfc2 3754* |
An alternate statement of the effective freeness of a class 𝐴, when
it is a set. (Contributed by Mario Carneiro, 14-Oct-2016.)
|
⊢ (∀𝑥 𝐴 ∈ 𝑉 → (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 = 𝐴)) |
|
Theorem | uniun 3755 |
The class union of the union of two classes. Theorem 8.3 of [Quine]
p. 53. (Contributed by NM, 20-Aug-1993.)
|
⊢ ∪ (𝐴 ∪ 𝐵) = (∪ 𝐴 ∪ ∪ 𝐵) |
|
Theorem | uniin 3756 |
The class union of the intersection of two classes. Exercise 4.12(n) of
[Mendelson] p. 235. (Contributed by
NM, 4-Dec-2003.) (Proof shortened
by Andrew Salmon, 29-Jun-2011.)
|
⊢ ∪ (𝐴 ∩ 𝐵) ⊆ (∪
𝐴 ∩ ∪ 𝐵) |
|
Theorem | uniss 3757 |
Subclass relationship for class union. Theorem 61 of [Suppes] p. 39.
(Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon,
29-Jun-2011.)
|
⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵) |
|
Theorem | ssuni 3758 |
Subclass relationship for class union. (Contributed by NM,
24-May-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ⊆ ∪ 𝐶) |
|
Theorem | unissi 3759 |
Subclass relationship for subclass union. Inference form of uniss 3757.
(Contributed by David Moews, 1-May-2017.)
|
⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ ∪
𝐴 ⊆ ∪ 𝐵 |
|
Theorem | unissd 3760 |
Subclass relationship for subclass union. Deduction form of uniss 3757.
(Contributed by David Moews, 1-May-2017.)
|
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → ∪ 𝐴 ⊆ ∪ 𝐵) |
|
Theorem | uni0b 3761 |
The union of a set is empty iff the set is included in the singleton of
the empty set. (Contributed by NM, 12-Sep-2004.)
|
⊢ (∪ 𝐴 = ∅ ↔ 𝐴 ⊆
{∅}) |
|
Theorem | uni0c 3762* |
The union of a set is empty iff all of its members are empty.
(Contributed by NM, 16-Aug-2006.)
|
⊢ (∪ 𝐴 = ∅ ↔ ∀𝑥 ∈ 𝐴 𝑥 = ∅) |
|
Theorem | uni0 3763 |
The union of the empty set is the empty set. Theorem 8.7 of [Quine]
p. 54. (Reproved without relying on ax-nul by Eric Schmidt.)
(Contributed by NM, 16-Sep-1993.) (Revised by Eric Schmidt,
4-Apr-2007.)
|
⊢ ∪ ∅ =
∅ |
|
Theorem | elssuni 3764 |
An element of a class is a subclass of its union. Theorem 8.6 of [Quine]
p. 54. Also the basis for Proposition 7.20 of [TakeutiZaring] p. 40.
(Contributed by NM, 6-Jun-1994.)
|
⊢ (𝐴 ∈ 𝐵 → 𝐴 ⊆ ∪ 𝐵) |
|
Theorem | unissel 3765 |
Condition turning a subclass relationship for union into an equality.
(Contributed by NM, 18-Jul-2006.)
|
⊢ ((∪ 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐴) → ∪ 𝐴 = 𝐵) |
|
Theorem | unissb 3766* |
Relationship involving membership, subset, and union. Exercise 5 of
[Enderton] p. 26 and its converse.
(Contributed by NM, 20-Sep-2003.)
|
⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵) |
|
Theorem | uniss2 3767* |
A subclass condition on the members of two classes that implies a
subclass relation on their unions. Proposition 8.6 of [TakeutiZaring]
p. 59. (Contributed by NM, 22-Mar-2004.)
|
⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 → ∪ 𝐴 ⊆ ∪ 𝐵) |
|
Theorem | unidif 3768* |
If the difference 𝐴 ∖ 𝐵 contains the largest members of
𝐴,
then
the union of the difference is the union of 𝐴. (Contributed by NM,
22-Mar-2004.)
|
⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ (𝐴 ∖ 𝐵)𝑥 ⊆ 𝑦 → ∪ (𝐴 ∖ 𝐵) = ∪ 𝐴) |
|
Theorem | ssunieq 3769* |
Relationship implying union. (Contributed by NM, 10-Nov-1999.)
|
⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝑥 ⊆ 𝐴) → 𝐴 = ∪ 𝐵) |
|
Theorem | unimax 3770* |
Any member of a class is the largest of those members that it includes.
(Contributed by NM, 13-Aug-2002.)
|
⊢ (𝐴 ∈ 𝐵 → ∪ {𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴} = 𝐴) |
|
2.1.19 The intersection of a class
|
|
Syntax | cint 3771 |
Extend class notation to include the intersection of a class (read:
'intersect 𝐴').
|
class ∩ 𝐴 |
|
Definition | df-int 3772* |
Define the intersection of a class. Definition 7.35 of [TakeutiZaring]
p. 44. For example, ∩ { { 1 , 3 } , { 1 , 8 } } = { 1 } .
Compare this with the intersection of two classes, df-in 3077.
(Contributed by NM, 18-Aug-1993.)
|
⊢ ∩ 𝐴 = {𝑥 ∣ ∀𝑦(𝑦 ∈ 𝐴 → 𝑥 ∈ 𝑦)} |
|
Theorem | dfint2 3773* |
Alternate definition of class intersection. (Contributed by NM,
28-Jun-1998.)
|
⊢ ∩ 𝐴 = {𝑥 ∣ ∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦} |
|
Theorem | inteq 3774 |
Equality law for intersection. (Contributed by NM, 13-Sep-1999.)
|
⊢ (𝐴 = 𝐵 → ∩ 𝐴 = ∩
𝐵) |
|
Theorem | inteqi 3775 |
Equality inference for class intersection. (Contributed by NM,
2-Sep-2003.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ ∩
𝐴 = ∩ 𝐵 |
|
Theorem | inteqd 3776 |
Equality deduction for class intersection. (Contributed by NM,
2-Sep-2003.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ∩ 𝐴 = ∩
𝐵) |
|
Theorem | elint 3777* |
Membership in class intersection. (Contributed by NM, 21-May-1994.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝐴 ∈ 𝑥)) |
|
Theorem | elint2 3778* |
Membership in class intersection. (Contributed by NM, 14-Oct-1999.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝑥) |
|
Theorem | elintg 3779* |
Membership in class intersection, with the sethood requirement expressed
as an antecedent. (Contributed by NM, 20-Nov-2003.)
|
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)) |
|
Theorem | elinti 3780 |
Membership in class intersection. (Contributed by NM, 14-Oct-1999.)
(Proof shortened by Andrew Salmon, 9-Jul-2011.)
|
⊢ (𝐴 ∈ ∩ 𝐵 → (𝐶 ∈ 𝐵 → 𝐴 ∈ 𝐶)) |
|
Theorem | nfint 3781 |
Bound-variable hypothesis builder for intersection. (Contributed by NM,
2-Feb-1997.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
|
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥∩
𝐴 |
|
Theorem | elintab 3782* |
Membership in the intersection of a class abstraction. (Contributed by
NM, 30-Aug-1993.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥)) |
|
Theorem | elintrab 3783* |
Membership in the intersection of a class abstraction. (Contributed by
NM, 17-Oct-1999.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ ∩ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐵 (𝜑 → 𝐴 ∈ 𝑥)) |
|
Theorem | elintrabg 3784* |
Membership in the intersection of a class abstraction. (Contributed by
NM, 17-Feb-2007.)
|
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐵 (𝜑 → 𝐴 ∈ 𝑥))) |
|
Theorem | int0 3785 |
The intersection of the empty set is the universal class. Exercise 2 of
[TakeutiZaring] p. 44.
(Contributed by NM, 18-Aug-1993.)
|
⊢ ∩ ∅ =
V |
|
Theorem | intss1 3786 |
An element of a class includes the intersection of the class. Exercise
4 of [TakeutiZaring] p. 44 (with
correction), generalized to classes.
(Contributed by NM, 18-Nov-1995.)
|
⊢ (𝐴 ∈ 𝐵 → ∩ 𝐵 ⊆ 𝐴) |
|
Theorem | ssint 3787* |
Subclass of a class intersection. Theorem 5.11(viii) of [Monk1] p. 52
and its converse. (Contributed by NM, 14-Oct-1999.)
|
⊢ (𝐴 ⊆ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ⊆ 𝑥) |
|
Theorem | ssintab 3788* |
Subclass of the intersection of a class abstraction. (Contributed by
NM, 31-Jul-2006.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|
⊢ (𝐴 ⊆ ∩
{𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ⊆ 𝑥)) |
|
Theorem | ssintub 3789* |
Subclass of the least upper bound. (Contributed by NM, 8-Aug-2000.)
|
⊢ 𝐴 ⊆ ∩
{𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} |
|
Theorem | ssmin 3790* |
Subclass of the minimum value of class of supersets. (Contributed by
NM, 10-Aug-2006.)
|
⊢ 𝐴 ⊆ ∩
{𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ 𝜑)} |
|
Theorem | intmin 3791* |
Any member of a class is the smallest of those members that include it.
(Contributed by NM, 13-Aug-2002.) (Proof shortened by Andrew Salmon,
9-Jul-2011.)
|
⊢ (𝐴 ∈ 𝐵 → ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} = 𝐴) |
|
Theorem | intss 3792 |
Intersection of subclasses. (Contributed by NM, 14-Oct-1999.)
|
⊢ (𝐴 ⊆ 𝐵 → ∩ 𝐵 ⊆ ∩ 𝐴) |
|
Theorem | intssunim 3793* |
The intersection of an inhabited set is a subclass of its union.
(Contributed by NM, 29-Jul-2006.)
|
⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ ∪ 𝐴) |
|
Theorem | ssintrab 3794* |
Subclass of the intersection of a restricted class builder.
(Contributed by NM, 30-Jan-2015.)
|
⊢ (𝐴 ⊆ ∩
{𝑥 ∈ 𝐵 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐵 (𝜑 → 𝐴 ⊆ 𝑥)) |
|
Theorem | intssuni2m 3795* |
Subclass relationship for intersection and union. (Contributed by Jim
Kingdon, 14-Aug-2018.)
|
⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 𝑥 ∈ 𝐴) → ∩ 𝐴 ⊆ ∪ 𝐵) |
|
Theorem | intminss 3796* |
Under subset ordering, the intersection of a restricted class
abstraction is less than or equal to any of its members. (Contributed
by NM, 7-Sep-2013.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∩
{𝑥 ∈ 𝐵 ∣ 𝜑} ⊆ 𝐴) |
|
Theorem | intmin2 3797* |
Any set is the smallest of all sets that include it. (Contributed by
NM, 20-Sep-2003.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ ∩
{𝑥 ∣ 𝐴 ⊆ 𝑥} = 𝐴 |
|
Theorem | intmin3 3798* |
Under subset ordering, the intersection of a class abstraction is less
than or equal to any of its members. (Contributed by NM,
3-Jul-2005.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝜓 ⇒ ⊢ (𝐴 ∈ 𝑉 → ∩ {𝑥 ∣ 𝜑} ⊆ 𝐴) |
|
Theorem | intmin4 3799* |
Elimination of a conjunct in a class intersection. (Contributed by NM,
31-Jul-2006.)
|
⊢ (𝐴 ⊆ ∩
{𝑥 ∣ 𝜑} → ∩
{𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ 𝜑)} = ∩ {𝑥 ∣ 𝜑}) |
|
Theorem | intab 3800* |
The intersection of a special case of a class abstraction. 𝑦 may be
free in 𝜑 and 𝐴, which can be thought of
a 𝜑(𝑦) and
𝐴(𝑦). (Contributed by NM, 28-Jul-2006.)
(Proof shortened by
Mario Carneiro, 14-Nov-2016.)
|
⊢ 𝐴 ∈ V & ⊢ {𝑥 ∣ ∃𝑦(𝜑 ∧ 𝑥 = 𝐴)} ∈ V ⇒ ⊢ ∩
{𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} = {𝑥 ∣ ∃𝑦(𝜑 ∧ 𝑥 = 𝐴)} |