Theorem List for Intuitionistic Logic Explorer - 3901-4000 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | pwpwssunieq 3901* |
The class of sets whose union is equal to a given class is included in
the double power class of that class. (Contributed by BJ,
29-Apr-2021.)
|
⊢ {𝑥 ∣ ∪ 𝑥 = 𝐴} ⊆ 𝒫 𝒫 𝐴 |
|
Theorem | elpwuni 3902 |
Relationship for power class and union. (Contributed by NM,
18-Jul-2006.)
|
⊢ (𝐵 ∈ 𝐴 → (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 = 𝐵)) |
|
Theorem | iinpw 3903* |
The power class of an intersection in terms of indexed intersection.
Exercise 24(a) of [Enderton] p. 33.
(Contributed by NM,
29-Nov-2003.)
|
⊢ 𝒫 ∩ 𝐴 = ∩ 𝑥 ∈ 𝐴 𝒫 𝑥 |
|
Theorem | iunpwss 3904* |
Inclusion of an indexed union of a power class in the power class of the
union of its index. Part of Exercise 24(b) of [Enderton] p. 33.
(Contributed by NM, 25-Nov-2003.)
|
⊢ ∪ 𝑥 ∈ 𝐴 𝒫 𝑥 ⊆ 𝒫 ∪ 𝐴 |
|
Theorem | rintm 3905* |
Relative intersection of an inhabited class. (Contributed by Jim
Kingdon, 19-Aug-2018.)
|
⊢ ((𝑋 ⊆ 𝒫 𝐴 ∧ ∃𝑥 𝑥 ∈ 𝑋) → (𝐴 ∩ ∩ 𝑋) = ∩ 𝑋) |
|
2.1.21 Disjointness
|
|
Syntax | wdisj 3906 |
Extend wff notation to include the statement that a family of classes
𝐵(𝑥), for 𝑥 ∈ 𝐴, is a disjoint family.
|
wff Disj 𝑥 ∈ 𝐴 𝐵 |
|
Definition | df-disj 3907* |
A collection of classes 𝐵(𝑥) is disjoint when for each element
𝑦, it is in 𝐵(𝑥) for at most one 𝑥.
(Contributed by
Mario Carneiro, 14-Nov-2016.) (Revised by NM, 16-Jun-2017.)
|
⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
|
Theorem | dfdisj2 3908* |
Alternate definition for disjoint classes. (Contributed by NM,
17-Jun-2017.)
|
⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑦∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
|
Theorem | disjss2 3909 |
If each element of a collection is contained in a disjoint collection,
the original collection is also disjoint. (Contributed by Mario
Carneiro, 14-Nov-2016.)
|
⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → (Disj 𝑥 ∈ 𝐴 𝐶 → Disj 𝑥 ∈ 𝐴 𝐵)) |
|
Theorem | disjeq2 3910 |
Equality theorem for disjoint collection. (Contributed by Mario Carneiro,
14-Nov-2016.)
|
⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑥 ∈ 𝐴 𝐶)) |
|
Theorem | disjeq2dv 3911* |
Equality deduction for disjoint collection. (Contributed by Mario
Carneiro, 14-Nov-2016.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑥 ∈ 𝐴 𝐶)) |
|
Theorem | disjss1 3912* |
A subset of a disjoint collection is disjoint. (Contributed by Mario
Carneiro, 14-Nov-2016.)
|
⊢ (𝐴 ⊆ 𝐵 → (Disj 𝑥 ∈ 𝐵 𝐶 → Disj 𝑥 ∈ 𝐴 𝐶)) |
|
Theorem | disjeq1 3913* |
Equality theorem for disjoint collection. (Contributed by Mario
Carneiro, 14-Nov-2016.)
|
⊢ (𝐴 = 𝐵 → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐶)) |
|
Theorem | disjeq1d 3914* |
Equality theorem for disjoint collection. (Contributed by Mario
Carneiro, 14-Nov-2016.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐶)) |
|
Theorem | disjeq12d 3915* |
Equality theorem for disjoint collection. (Contributed by Mario
Carneiro, 14-Nov-2016.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐷)) |
|
Theorem | cbvdisj 3916* |
Change bound variables in a disjoint collection. (Contributed by Mario
Carneiro, 14-Nov-2016.)
|
⊢ Ⅎ𝑦𝐵
& ⊢ Ⅎ𝑥𝐶
& ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐴 𝐶) |
|
Theorem | cbvdisjv 3917* |
Change bound variables in a disjoint collection. (Contributed by Mario
Carneiro, 11-Dec-2016.)
|
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐴 𝐶) |
|
Theorem | nfdisjv 3918* |
Bound-variable hypothesis builder for disjoint collection. (Contributed
by Jim Kingdon, 19-Aug-2018.)
|
⊢ Ⅎ𝑦𝐴
& ⊢ Ⅎ𝑦𝐵 ⇒ ⊢ Ⅎ𝑦Disj 𝑥 ∈ 𝐴 𝐵 |
|
Theorem | nfdisj1 3919 |
Bound-variable hypothesis builder for disjoint collection. (Contributed
by Mario Carneiro, 14-Nov-2016.)
|
⊢ Ⅎ𝑥Disj 𝑥 ∈ 𝐴 𝐵 |
|
Theorem | disjnim 3920* |
If a collection 𝐵(𝑖) for 𝑖 ∈ 𝐴 is disjoint, then pairs are
disjoint. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by
Jim Kingdon, 6-Oct-2022.)
|
⊢ (𝑖 = 𝑗 → 𝐵 = 𝐶) ⇒ ⊢ (Disj 𝑖 ∈ 𝐴 𝐵 → ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 ≠ 𝑗 → (𝐵 ∩ 𝐶) = ∅)) |
|
Theorem | disjnims 3921* |
If a collection 𝐵(𝑖) for 𝑖 ∈ 𝐴 is disjoint, then pairs are
disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.) (Revised by
Jim Kingdon, 7-Oct-2022.)
|
⊢ (Disj 𝑥 ∈ 𝐴 𝐵 → ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 ≠ 𝑗 → (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)) |
|
Theorem | disji2 3922* |
Property of a disjoint collection: if 𝐵(𝑋) = 𝐶 and
𝐵(𝑌) = 𝐷, and 𝑋 ≠ 𝑌, then 𝐶 and 𝐷 are
disjoint.
(Contributed by Mario Carneiro, 14-Nov-2016.)
|
⊢ (𝑥 = 𝑋 → 𝐵 = 𝐶)
& ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐷) ⇒ ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ 𝑋 ≠ 𝑌) → (𝐶 ∩ 𝐷) = ∅) |
|
Theorem | invdisj 3923* |
If there is a function 𝐶(𝑦) such that 𝐶(𝑦) = 𝑥 for all
𝑦
∈ 𝐵(𝑥), then the sets 𝐵(𝑥) for distinct 𝑥 ∈ 𝐴 are
disjoint. (Contributed by Mario Carneiro, 10-Dec-2016.)
|
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 = 𝑥 → Disj 𝑥 ∈ 𝐴 𝐵) |
|
Theorem | disjiun 3924* |
A disjoint collection yields disjoint indexed unions for disjoint index
sets. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by Mario
Carneiro, 14-Nov-2016.)
|
⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ∧ (𝐶 ∩ 𝐷) = ∅)) → (∪ 𝑥 ∈ 𝐶 𝐵 ∩ ∪
𝑥 ∈ 𝐷 𝐵) = ∅) |
|
Theorem | sndisj 3925 |
Any collection of singletons is disjoint. (Contributed by Mario
Carneiro, 14-Nov-2016.)
|
⊢ Disj 𝑥 ∈ 𝐴 {𝑥} |
|
Theorem | 0disj 3926 |
Any collection of empty sets is disjoint. (Contributed by Mario Carneiro,
14-Nov-2016.)
|
⊢ Disj 𝑥 ∈ 𝐴 ∅ |
|
Theorem | disjxsn 3927* |
A singleton collection is disjoint. (Contributed by Mario Carneiro,
14-Nov-2016.)
|
⊢ Disj 𝑥 ∈ {𝐴}𝐵 |
|
Theorem | disjx0 3928 |
An empty collection is disjoint. (Contributed by Mario Carneiro,
14-Nov-2016.)
|
⊢ Disj 𝑥 ∈ ∅ 𝐵 |
|
2.1.22 Binary relations
|
|
Syntax | wbr 3929 |
Extend wff notation to include the general binary relation predicate.
Note that the syntax is simply three class symbols in a row. Since binary
relations are the only possible wff expressions consisting of three class
expressions in a row, the syntax is unambiguous.
|
wff 𝐴𝑅𝐵 |
|
Definition | df-br 3930 |
Define a general binary relation. Note that the syntax is simply three
class symbols in a row. Definition 6.18 of [TakeutiZaring] p. 29
generalized to arbitrary classes. This definition of relations is
well-defined, although not very meaningful, when classes 𝐴 and/or
𝐵 are proper classes (i.e. are not
sets). On the other hand, we often
find uses for this definition when 𝑅 is a proper class (see for
example iprc 4807). (Contributed by NM, 31-Dec-1993.)
|
⊢ (𝐴𝑅𝐵 ↔ 〈𝐴, 𝐵〉 ∈ 𝑅) |
|
Theorem | breq 3931 |
Equality theorem for binary relations. (Contributed by NM,
4-Jun-1995.)
|
⊢ (𝑅 = 𝑆 → (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵)) |
|
Theorem | breq1 3932 |
Equality theorem for a binary relation. (Contributed by NM,
31-Dec-1993.)
|
⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)) |
|
Theorem | breq2 3933 |
Equality theorem for a binary relation. (Contributed by NM,
31-Dec-1993.)
|
⊢ (𝐴 = 𝐵 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵)) |
|
Theorem | breq12 3934 |
Equality theorem for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)) |
|
Theorem | breqi 3935 |
Equality inference for binary relations. (Contributed by NM,
19-Feb-2005.)
|
⊢ 𝑅 = 𝑆 ⇒ ⊢ (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵) |
|
Theorem | breq1i 3936 |
Equality inference for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶) |
|
Theorem | breq2i 3937 |
Equality inference for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵) |
|
Theorem | breq12i 3938 |
Equality inference for a binary relation. (Contributed by NM,
8-Feb-1996.) (Proof shortened by Eric Schmidt, 4-Apr-2007.)
|
⊢ 𝐴 = 𝐵
& ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷) |
|
Theorem | breq1d 3939 |
Equality deduction for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)) |
|
Theorem | breqd 3940 |
Equality deduction for a binary relation. (Contributed by NM,
29-Oct-2011.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶𝐴𝐷 ↔ 𝐶𝐵𝐷)) |
|
Theorem | breq2d 3941 |
Equality deduction for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵)) |
|
Theorem | breq12d 3942 |
Equality deduction for a binary relation. (Contributed by NM,
8-Feb-1996.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)) |
|
Theorem | breq123d 3943 |
Equality deduction for a binary relation. (Contributed by NM,
29-Oct-2011.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝑅 = 𝑆)
& ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑆𝐷)) |
|
Theorem | breqdi 3944 |
Equality deduction for a binary relation. (Contributed by Thierry
Arnoux, 5-Oct-2020.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐶𝐴𝐷) ⇒ ⊢ (𝜑 → 𝐶𝐵𝐷) |
|
Theorem | breqan12d 3945 |
Equality deduction for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜓 → 𝐶 = 𝐷) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)) |
|
Theorem | breqan12rd 3946 |
Equality deduction for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜓 → 𝐶 = 𝐷) ⇒ ⊢ ((𝜓 ∧ 𝜑) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)) |
|
Theorem | nbrne1 3947 |
Two classes are different if they don't have the same relationship to a
third class. (Contributed by NM, 3-Jun-2012.)
|
⊢ ((𝐴𝑅𝐵 ∧ ¬ 𝐴𝑅𝐶) → 𝐵 ≠ 𝐶) |
|
Theorem | nbrne2 3948 |
Two classes are different if they don't have the same relationship to a
third class. (Contributed by NM, 3-Jun-2012.)
|
⊢ ((𝐴𝑅𝐶 ∧ ¬ 𝐵𝑅𝐶) → 𝐴 ≠ 𝐵) |
|
Theorem | eqbrtri 3949 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 5-Aug-1993.)
|
⊢ 𝐴 = 𝐵
& ⊢ 𝐵𝑅𝐶 ⇒ ⊢ 𝐴𝑅𝐶 |
|
Theorem | eqbrtrd 3950 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 8-Oct-1999.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
|
Theorem | eqbrtrri 3951 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 5-Aug-1993.)
|
⊢ 𝐴 = 𝐵
& ⊢ 𝐴𝑅𝐶 ⇒ ⊢ 𝐵𝑅𝐶 |
|
Theorem | eqbrtrrd 3952 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 24-Oct-1999.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐴𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐵𝑅𝐶) |
|
Theorem | breqtri 3953 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 5-Aug-1993.)
|
⊢ 𝐴𝑅𝐵
& ⊢ 𝐵 = 𝐶 ⇒ ⊢ 𝐴𝑅𝐶 |
|
Theorem | breqtrd 3954 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 24-Oct-1999.)
|
⊢ (𝜑 → 𝐴𝑅𝐵)
& ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
|
Theorem | breqtrri 3955 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 5-Aug-1993.)
|
⊢ 𝐴𝑅𝐵
& ⊢ 𝐶 = 𝐵 ⇒ ⊢ 𝐴𝑅𝐶 |
|
Theorem | breqtrrd 3956 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 24-Oct-1999.)
|
⊢ (𝜑 → 𝐴𝑅𝐵)
& ⊢ (𝜑 → 𝐶 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
|
Theorem | 3brtr3i 3957 |
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 11-Aug-1999.)
|
⊢ 𝐴𝑅𝐵
& ⊢ 𝐴 = 𝐶
& ⊢ 𝐵 = 𝐷 ⇒ ⊢ 𝐶𝑅𝐷 |
|
Theorem | 3brtr4i 3958 |
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 11-Aug-1999.)
|
⊢ 𝐴𝑅𝐵
& ⊢ 𝐶 = 𝐴
& ⊢ 𝐷 = 𝐵 ⇒ ⊢ 𝐶𝑅𝐷 |
|
Theorem | 3brtr3d 3959 |
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 18-Oct-1999.)
|
⊢ (𝜑 → 𝐴𝑅𝐵)
& ⊢ (𝜑 → 𝐴 = 𝐶)
& ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → 𝐶𝑅𝐷) |
|
Theorem | 3brtr4d 3960 |
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 21-Feb-2005.)
|
⊢ (𝜑 → 𝐴𝑅𝐵)
& ⊢ (𝜑 → 𝐶 = 𝐴)
& ⊢ (𝜑 → 𝐷 = 𝐵) ⇒ ⊢ (𝜑 → 𝐶𝑅𝐷) |
|
Theorem | 3brtr3g 3961 |
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 16-Jan-1997.)
|
⊢ (𝜑 → 𝐴𝑅𝐵)
& ⊢ 𝐴 = 𝐶
& ⊢ 𝐵 = 𝐷 ⇒ ⊢ (𝜑 → 𝐶𝑅𝐷) |
|
Theorem | 3brtr4g 3962 |
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 16-Jan-1997.)
|
⊢ (𝜑 → 𝐴𝑅𝐵)
& ⊢ 𝐶 = 𝐴
& ⊢ 𝐷 = 𝐵 ⇒ ⊢ (𝜑 → 𝐶𝑅𝐷) |
|
Theorem | eqbrtrid 3963 |
B chained equality inference for a binary relation. (Contributed by NM,
11-Oct-1999.)
|
⊢ 𝐴 = 𝐵
& ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
|
Theorem | eqbrtrrid 3964 |
B chained equality inference for a binary relation. (Contributed by NM,
17-Sep-2004.)
|
⊢ 𝐵 = 𝐴
& ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
|
Theorem | breqtrid 3965 |
B chained equality inference for a binary relation. (Contributed by NM,
11-Oct-1999.)
|
⊢ 𝐴𝑅𝐵
& ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
|
Theorem | breqtrrid 3966 |
B chained equality inference for a binary relation. (Contributed by NM,
24-Apr-2005.)
|
⊢ 𝐴𝑅𝐵
& ⊢ (𝜑 → 𝐶 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
|
Theorem | eqbrtrdi 3967 |
A chained equality inference for a binary relation. (Contributed by NM,
12-Oct-1999.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ 𝐵𝑅𝐶 ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
|
Theorem | eqbrtrrdi 3968 |
A chained equality inference for a binary relation. (Contributed by NM,
4-Jan-2006.)
|
⊢ (𝜑 → 𝐵 = 𝐴)
& ⊢ 𝐵𝑅𝐶 ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
|
Theorem | breqtrdi 3969 |
A chained equality inference for a binary relation. (Contributed by NM,
11-Oct-1999.)
|
⊢ (𝜑 → 𝐴𝑅𝐵)
& ⊢ 𝐵 = 𝐶 ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
|
Theorem | breqtrrdi 3970 |
A chained equality inference for a binary relation. (Contributed by NM,
24-Apr-2005.)
|
⊢ (𝜑 → 𝐴𝑅𝐵)
& ⊢ 𝐶 = 𝐵 ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
|
Theorem | ssbrd 3971 |
Deduction from a subclass relationship of binary relations.
(Contributed by NM, 30-Apr-2004.)
|
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐶𝐴𝐷 → 𝐶𝐵𝐷)) |
|
Theorem | ssbri 3972 |
Inference from a subclass relationship of binary relations.
(Contributed by NM, 28-Mar-2007.) (Revised by Mario Carneiro,
8-Feb-2015.)
|
⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ (𝐶𝐴𝐷 → 𝐶𝐵𝐷) |
|
Theorem | nfbrd 3973 |
Deduction version of bound-variable hypothesis builder nfbr 3974.
(Contributed by NM, 13-Dec-2005.) (Revised by Mario Carneiro,
14-Oct-2016.)
|
⊢ (𝜑 → Ⅎ𝑥𝐴)
& ⊢ (𝜑 → Ⅎ𝑥𝑅)
& ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥 𝐴𝑅𝐵) |
|
Theorem | nfbr 3974 |
Bound-variable hypothesis builder for binary relation. (Contributed by
NM, 1-Sep-1999.) (Revised by Mario Carneiro, 14-Oct-2016.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝑅
& ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐴𝑅𝐵 |
|
Theorem | brab1 3975* |
Relationship between a binary relation and a class abstraction.
(Contributed by Andrew Salmon, 8-Jul-2011.)
|
⊢ (𝑥𝑅𝐴 ↔ 𝑥 ∈ {𝑧 ∣ 𝑧𝑅𝐴}) |
|
Theorem | br0 3976 |
The empty binary relation never holds. (Contributed by NM,
23-Aug-2018.)
|
⊢ ¬ 𝐴∅𝐵 |
|
Theorem | brne0 3977 |
If two sets are in a binary relation, the relation cannot be empty. In
fact, the relation is also inhabited, as seen at brm 3978.
(Contributed by
Alexander van der Vekens, 7-Jul-2018.)
|
⊢ (𝐴𝑅𝐵 → 𝑅 ≠ ∅) |
|
Theorem | brm 3978* |
If two sets are in a binary relation, the relation is inhabited.
(Contributed by Jim Kingdon, 31-Dec-2023.)
|
⊢ (𝐴𝑅𝐵 → ∃𝑥 𝑥 ∈ 𝑅) |
|
Theorem | brun 3979 |
The union of two binary relations. (Contributed by NM, 21-Dec-2008.)
|
⊢ (𝐴(𝑅 ∪ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∨ 𝐴𝑆𝐵)) |
|
Theorem | brin 3980 |
The intersection of two relations. (Contributed by FL, 7-Oct-2008.)
|
⊢ (𝐴(𝑅 ∩ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ 𝐴𝑆𝐵)) |
|
Theorem | brdif 3981 |
The difference of two binary relations. (Contributed by Scott Fenton,
11-Apr-2011.)
|
⊢ (𝐴(𝑅 ∖ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ ¬ 𝐴𝑆𝐵)) |
|
Theorem | sbcbrg 3982 |
Move substitution in and out of a binary relation. (Contributed by NM,
13-Dec-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|
⊢ (𝐴 ∈ 𝐷 → ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵⦋𝐴 / 𝑥⦌𝑅⦋𝐴 / 𝑥⦌𝐶)) |
|
Theorem | sbcbr12g 3983* |
Move substitution in and out of a binary relation. (Contributed by NM,
13-Dec-2005.)
|
⊢ (𝐴 ∈ 𝐷 → ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵𝑅⦋𝐴 / 𝑥⦌𝐶)) |
|
Theorem | sbcbr1g 3984* |
Move substitution in and out of a binary relation. (Contributed by NM,
13-Dec-2005.)
|
⊢ (𝐴 ∈ 𝐷 → ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵𝑅𝐶)) |
|
Theorem | sbcbr2g 3985* |
Move substitution in and out of a binary relation. (Contributed by NM,
13-Dec-2005.)
|
⊢ (𝐴 ∈ 𝐷 → ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ 𝐵𝑅⦋𝐴 / 𝑥⦌𝐶)) |
|
Theorem | brralrspcev 3986* |
Restricted existential specialization with a restricted universal
quantifier over a relation, closed form. (Contributed by AV,
20-Aug-2022.)
|
⊢ ((𝐵 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝑌 𝐴𝑅𝐵) → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐴𝑅𝑥) |
|
Theorem | brimralrspcev 3987* |
Restricted existential specialization with a restricted universal
quantifier over an implication with a relation in the antecedent, closed
form. (Contributed by AV, 20-Aug-2022.)
|
⊢ ((𝐵 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝑌 ((𝜑 ∧ 𝐴𝑅𝐵) → 𝜓)) → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝜑 ∧ 𝐴𝑅𝑥) → 𝜓)) |
|
2.1.23 Ordered-pair class abstractions (class
builders)
|
|
Syntax | copab 3988 |
Extend class notation to include ordered-pair class abstraction (class
builder).
|
class {〈𝑥, 𝑦〉 ∣ 𝜑} |
|
Syntax | cmpt 3989 |
Extend the definition of a class to include maps-to notation for defining
a function via a rule.
|
class (𝑥 ∈ 𝐴 ↦ 𝐵) |
|
Definition | df-opab 3990* |
Define the class abstraction of a collection of ordered pairs.
Definition 3.3 of [Monk1] p. 34. Usually
𝑥
and 𝑦 are distinct,
although the definition doesn't strictly require it. The brace notation
is called "class abstraction" by Quine; it is also (more
commonly)
called a "class builder" in the literature. (Contributed by
NM,
4-Jul-1994.)
|
⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)} |
|
Definition | df-mpt 3991* |
Define maps-to notation for defining a function via a rule. Read as
"the function defined by the map from 𝑥 (in 𝐴) to
𝐵(𝑥)." The class expression 𝐵 is the
value of the function
at 𝑥 and normally contains the variable
𝑥.
Similar to the
definition of mapping in [ChoquetDD]
p. 2. (Contributed by NM,
17-Feb-2008.)
|
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} |
|
Theorem | opabss 3992* |
The collection of ordered pairs in a class is a subclass of it.
(Contributed by NM, 27-Dec-1996.) (Proof shortened by Andrew Salmon,
9-Jul-2011.)
|
⊢ {〈𝑥, 𝑦〉 ∣ 𝑥𝑅𝑦} ⊆ 𝑅 |
|
Theorem | opabbid 3993 |
Equivalent wff's yield equal ordered-pair class abstractions (deduction
form). (Contributed by NM, 21-Feb-2004.) (Proof shortened by Andrew
Salmon, 9-Jul-2011.)
|
⊢ Ⅎ𝑥𝜑
& ⊢ Ⅎ𝑦𝜑
& ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝜓} = {〈𝑥, 𝑦〉 ∣ 𝜒}) |
|
Theorem | opabbidv 3994* |
Equivalent wff's yield equal ordered-pair class abstractions (deduction
form). (Contributed by NM, 15-May-1995.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝜓} = {〈𝑥, 𝑦〉 ∣ 𝜒}) |
|
Theorem | opabbii 3995 |
Equivalent wff's yield equal class abstractions. (Contributed by NM,
15-May-1995.)
|
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑦〉 ∣ 𝜓} |
|
Theorem | nfopab 3996* |
Bound-variable hypothesis builder for class abstraction. (Contributed
by NM, 1-Sep-1999.) Remove disjoint variable conditions. (Revised by
Andrew Salmon, 11-Jul-2011.)
|
⊢ Ⅎ𝑧𝜑 ⇒ ⊢ Ⅎ𝑧{〈𝑥, 𝑦〉 ∣ 𝜑} |
|
Theorem | nfopab1 3997 |
The first abstraction variable in an ordered-pair class abstraction
(class builder) is effectively not free. (Contributed by NM,
16-May-1995.) (Revised by Mario Carneiro, 14-Oct-2016.)
|
⊢ Ⅎ𝑥{〈𝑥, 𝑦〉 ∣ 𝜑} |
|
Theorem | nfopab2 3998 |
The second abstraction variable in an ordered-pair class abstraction
(class builder) is effectively not free. (Contributed by NM,
16-May-1995.) (Revised by Mario Carneiro, 14-Oct-2016.)
|
⊢ Ⅎ𝑦{〈𝑥, 𝑦〉 ∣ 𝜑} |
|
Theorem | cbvopab 3999* |
Rule used to change bound variables in an ordered-pair class
abstraction, using implicit substitution. (Contributed by NM,
14-Sep-2003.)
|
⊢ Ⅎ𝑧𝜑
& ⊢ Ⅎ𝑤𝜑
& ⊢ Ⅎ𝑥𝜓
& ⊢ Ⅎ𝑦𝜓
& ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑧, 𝑤〉 ∣ 𝜓} |
|
Theorem | cbvopabv 4000* |
Rule used to change bound variables in an ordered-pair class
abstraction, using implicit substitution. (Contributed by NM,
15-Oct-1996.)
|
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑧, 𝑤〉 ∣ 𝜓} |