Home Intuitionistic Logic ExplorerTheorem List (p. 40 of 133) < Previous  Next > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 3901-4000   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theorempwpwssunieq 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.)
{𝑥 𝑥 = 𝐴} ⊆ 𝒫 𝒫 𝐴

Theoremelpwuni 3902 Relationship for power class and union. (Contributed by NM, 18-Jul-2006.)
(𝐵𝐴 → (𝐴 ⊆ 𝒫 𝐵 𝐴 = 𝐵))

Theoremiinpw 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.)
𝒫 𝐴 = 𝑥𝐴 𝒫 𝑥

Theoremiunpwss 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.)
𝑥𝐴 𝒫 𝑥 ⊆ 𝒫 𝐴

Theoremrintm 3905* Relative intersection of an inhabited class. (Contributed by Jim Kingdon, 19-Aug-2018.)
((𝑋 ⊆ 𝒫 𝐴 ∧ ∃𝑥 𝑥𝑋) → (𝐴 𝑋) = 𝑋)

2.1.21  Disjointness

Syntaxwdisj 3906 Extend wff notation to include the statement that a family of classes 𝐵(𝑥), for 𝑥𝐴, is a disjoint family.
wff Disj 𝑥𝐴 𝐵

Definitiondf-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 𝑥𝐴 𝐵 ↔ ∀𝑦∃*𝑥𝐴 𝑦𝐵)

Theoremdfdisj2 3908* Alternate definition for disjoint classes. (Contributed by NM, 17-Jun-2017.)
(Disj 𝑥𝐴 𝐵 ↔ ∀𝑦∃*𝑥(𝑥𝐴𝑦𝐵))

Theoremdisjss2 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 𝑥𝐴 𝐵))

Theoremdisjeq2 3910 Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
(∀𝑥𝐴 𝐵 = 𝐶 → (Disj 𝑥𝐴 𝐵Disj 𝑥𝐴 𝐶))

Theoremdisjeq2dv 3911* Equality deduction for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
((𝜑𝑥𝐴) → 𝐵 = 𝐶)       (𝜑 → (Disj 𝑥𝐴 𝐵Disj 𝑥𝐴 𝐶))

Theoremdisjss1 3912* A subset of a disjoint collection is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
(𝐴𝐵 → (Disj 𝑥𝐵 𝐶Disj 𝑥𝐴 𝐶))

Theoremdisjeq1 3913* Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
(𝐴 = 𝐵 → (Disj 𝑥𝐴 𝐶Disj 𝑥𝐵 𝐶))

Theoremdisjeq1d 3914* Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
(𝜑𝐴 = 𝐵)       (𝜑 → (Disj 𝑥𝐴 𝐶Disj 𝑥𝐵 𝐶))

Theoremdisjeq12d 3915* Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐶 = 𝐷)       (𝜑 → (Disj 𝑥𝐴 𝐶Disj 𝑥𝐵 𝐷))

Theoremcbvdisj 3916* Change bound variables in a disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
𝑦𝐵    &   𝑥𝐶    &   (𝑥 = 𝑦𝐵 = 𝐶)       (Disj 𝑥𝐴 𝐵Disj 𝑦𝐴 𝐶)

Theoremcbvdisjv 3917* Change bound variables in a disjoint collection. (Contributed by Mario Carneiro, 11-Dec-2016.)
(𝑥 = 𝑦𝐵 = 𝐶)       (Disj 𝑥𝐴 𝐵Disj 𝑦𝐴 𝐶)

Theoremnfdisjv 3918* Bound-variable hypothesis builder for disjoint collection. (Contributed by Jim Kingdon, 19-Aug-2018.)
𝑦𝐴    &   𝑦𝐵       𝑦Disj 𝑥𝐴 𝐵

Theoremnfdisj1 3919 Bound-variable hypothesis builder for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
𝑥Disj 𝑥𝐴 𝐵

Theoremdisjnim 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 𝑖𝐴 𝐵 → ∀𝑖𝐴𝑗𝐴 (𝑖𝑗 → (𝐵𝐶) = ∅))

Theoremdisjnims 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 𝑥𝐴 𝐵 → ∀𝑖𝐴𝑗𝐴 (𝑖𝑗 → (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))

Theoremdisji2 3922* Property of a disjoint collection: if 𝐵(𝑋) = 𝐶 and 𝐵(𝑌) = 𝐷, and 𝑋𝑌, then 𝐶 and 𝐷 are disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
(𝑥 = 𝑋𝐵 = 𝐶)    &   (𝑥 = 𝑌𝐵 = 𝐷)       ((Disj 𝑥𝐴 𝐵 ∧ (𝑋𝐴𝑌𝐴) ∧ 𝑋𝑌) → (𝐶𝐷) = ∅)

Theoreminvdisj 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 𝑥𝐴 𝐵)

Theoremdisjiun 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 𝑥𝐴 𝐵 ∧ (𝐶𝐴𝐷𝐴 ∧ (𝐶𝐷) = ∅)) → ( 𝑥𝐶 𝐵 𝑥𝐷 𝐵) = ∅)

Theoremsndisj 3925 Any collection of singletons is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
Disj 𝑥𝐴 {𝑥}

Theorem0disj 3926 Any collection of empty sets is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
Disj 𝑥𝐴

Theoremdisjxsn 3927* A singleton collection is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
Disj 𝑥 ∈ {𝐴}𝐵

Theoremdisjx0 3928 An empty collection is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
Disj 𝑥 ∈ ∅ 𝐵

2.1.22  Binary relations

Syntaxwbr 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 𝐴𝑅𝐵

Definitiondf-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.)
(𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)

Theorembreq 3931 Equality theorem for binary relations. (Contributed by NM, 4-Jun-1995.)
(𝑅 = 𝑆 → (𝐴𝑅𝐵𝐴𝑆𝐵))

Theorembreq1 3932 Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.)
(𝐴 = 𝐵 → (𝐴𝑅𝐶𝐵𝑅𝐶))

Theorembreq2 3933 Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.)
(𝐴 = 𝐵 → (𝐶𝑅𝐴𝐶𝑅𝐵))

Theorembreq12 3934 Equality theorem for a binary relation. (Contributed by NM, 8-Feb-1996.)
((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝑅𝐶𝐵𝑅𝐷))

Theorembreqi 3935 Equality inference for binary relations. (Contributed by NM, 19-Feb-2005.)
𝑅 = 𝑆       (𝐴𝑅𝐵𝐴𝑆𝐵)

Theorembreq1i 3936 Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.)
𝐴 = 𝐵       (𝐴𝑅𝐶𝐵𝑅𝐶)

Theorembreq2i 3937 Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.)
𝐴 = 𝐵       (𝐶𝑅𝐴𝐶𝑅𝐵)

Theorembreq12i 3938 Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Eric Schmidt, 4-Apr-2007.)
𝐴 = 𝐵    &   𝐶 = 𝐷       (𝐴𝑅𝐶𝐵𝑅𝐷)

Theorembreq1d 3939 Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
(𝜑𝐴 = 𝐵)       (𝜑 → (𝐴𝑅𝐶𝐵𝑅𝐶))

Theorembreqd 3940 Equality deduction for a binary relation. (Contributed by NM, 29-Oct-2011.)
(𝜑𝐴 = 𝐵)       (𝜑 → (𝐶𝐴𝐷𝐶𝐵𝐷))

Theorembreq2d 3941 Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
(𝜑𝐴 = 𝐵)       (𝜑 → (𝐶𝑅𝐴𝐶𝑅𝐵))

Theorembreq12d 3942 Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐶 = 𝐷)       (𝜑 → (𝐴𝑅𝐶𝐵𝑅𝐷))

Theorembreq123d 3943 Equality deduction for a binary relation. (Contributed by NM, 29-Oct-2011.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝑅 = 𝑆)    &   (𝜑𝐶 = 𝐷)       (𝜑 → (𝐴𝑅𝐶𝐵𝑆𝐷))

Theorembreqdi 3944 Equality deduction for a binary relation. (Contributed by Thierry Arnoux, 5-Oct-2020.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐶𝐴𝐷)       (𝜑𝐶𝐵𝐷)

Theorembreqan12d 3945 Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
(𝜑𝐴 = 𝐵)    &   (𝜓𝐶 = 𝐷)       ((𝜑𝜓) → (𝐴𝑅𝐶𝐵𝑅𝐷))

Theorembreqan12rd 3946 Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
(𝜑𝐴 = 𝐵)    &   (𝜓𝐶 = 𝐷)       ((𝜓𝜑) → (𝐴𝑅𝐶𝐵𝑅𝐷))

Theoremnbrne1 3947 Two classes are different if they don't have the same relationship to a third class. (Contributed by NM, 3-Jun-2012.)
((𝐴𝑅𝐵 ∧ ¬ 𝐴𝑅𝐶) → 𝐵𝐶)

Theoremnbrne2 3948 Two classes are different if they don't have the same relationship to a third class. (Contributed by NM, 3-Jun-2012.)
((𝐴𝑅𝐶 ∧ ¬ 𝐵𝑅𝐶) → 𝐴𝐵)

Theoremeqbrtri 3949 Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.)
𝐴 = 𝐵    &   𝐵𝑅𝐶       𝐴𝑅𝐶

Theoremeqbrtrd 3950 Substitution of equal classes into a binary relation. (Contributed by NM, 8-Oct-1999.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐵𝑅𝐶)       (𝜑𝐴𝑅𝐶)

Theoremeqbrtrri 3951 Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.)
𝐴 = 𝐵    &   𝐴𝑅𝐶       𝐵𝑅𝐶

Theoremeqbrtrrd 3952 Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐴𝑅𝐶)       (𝜑𝐵𝑅𝐶)

Theorembreqtri 3953 Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.)
𝐴𝑅𝐵    &   𝐵 = 𝐶       𝐴𝑅𝐶

Theorembreqtrd 3954 Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
(𝜑𝐴𝑅𝐵)    &   (𝜑𝐵 = 𝐶)       (𝜑𝐴𝑅𝐶)

Theorembreqtrri 3955 Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.)
𝐴𝑅𝐵    &   𝐶 = 𝐵       𝐴𝑅𝐶

Theorembreqtrrd 3956 Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
(𝜑𝐴𝑅𝐵)    &   (𝜑𝐶 = 𝐵)       (𝜑𝐴𝑅𝐶)

Theorem3brtr3i 3957 Substitution of equality into both sides of a binary relation. (Contributed by NM, 11-Aug-1999.)
𝐴𝑅𝐵    &   𝐴 = 𝐶    &   𝐵 = 𝐷       𝐶𝑅𝐷

Theorem3brtr4i 3958 Substitution of equality into both sides of a binary relation. (Contributed by NM, 11-Aug-1999.)
𝐴𝑅𝐵    &   𝐶 = 𝐴    &   𝐷 = 𝐵       𝐶𝑅𝐷

Theorem3brtr3d 3959 Substitution of equality into both sides of a binary relation. (Contributed by NM, 18-Oct-1999.)
(𝜑𝐴𝑅𝐵)    &   (𝜑𝐴 = 𝐶)    &   (𝜑𝐵 = 𝐷)       (𝜑𝐶𝑅𝐷)

Theorem3brtr4d 3960 Substitution of equality into both sides of a binary relation. (Contributed by NM, 21-Feb-2005.)
(𝜑𝐴𝑅𝐵)    &   (𝜑𝐶 = 𝐴)    &   (𝜑𝐷 = 𝐵)       (𝜑𝐶𝑅𝐷)

Theorem3brtr3g 3961 Substitution of equality into both sides of a binary relation. (Contributed by NM, 16-Jan-1997.)
(𝜑𝐴𝑅𝐵)    &   𝐴 = 𝐶    &   𝐵 = 𝐷       (𝜑𝐶𝑅𝐷)

Theorem3brtr4g 3962 Substitution of equality into both sides of a binary relation. (Contributed by NM, 16-Jan-1997.)
(𝜑𝐴𝑅𝐵)    &   𝐶 = 𝐴    &   𝐷 = 𝐵       (𝜑𝐶𝑅𝐷)

Theoremeqbrtrid 3963 B chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)
𝐴 = 𝐵    &   (𝜑𝐵𝑅𝐶)       (𝜑𝐴𝑅𝐶)

Theoremeqbrtrrid 3964 B chained equality inference for a binary relation. (Contributed by NM, 17-Sep-2004.)
𝐵 = 𝐴    &   (𝜑𝐵𝑅𝐶)       (𝜑𝐴𝑅𝐶)

Theorembreqtrid 3965 B chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)
𝐴𝑅𝐵    &   (𝜑𝐵 = 𝐶)       (𝜑𝐴𝑅𝐶)

Theorembreqtrrid 3966 B chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.)
𝐴𝑅𝐵    &   (𝜑𝐶 = 𝐵)       (𝜑𝐴𝑅𝐶)

Theoremeqbrtrdi 3967 A chained equality inference for a binary relation. (Contributed by NM, 12-Oct-1999.)
(𝜑𝐴 = 𝐵)    &   𝐵𝑅𝐶       (𝜑𝐴𝑅𝐶)

Theoremeqbrtrrdi 3968 A chained equality inference for a binary relation. (Contributed by NM, 4-Jan-2006.)
(𝜑𝐵 = 𝐴)    &   𝐵𝑅𝐶       (𝜑𝐴𝑅𝐶)

Theorembreqtrdi 3969 A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)
(𝜑𝐴𝑅𝐵)    &   𝐵 = 𝐶       (𝜑𝐴𝑅𝐶)

Theorembreqtrrdi 3970 A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.)
(𝜑𝐴𝑅𝐵)    &   𝐶 = 𝐵       (𝜑𝐴𝑅𝐶)

Theoremssbrd 3971 Deduction from a subclass relationship of binary relations. (Contributed by NM, 30-Apr-2004.)
(𝜑𝐴𝐵)       (𝜑 → (𝐶𝐴𝐷𝐶𝐵𝐷))

Theoremssbri 3972 Inference from a subclass relationship of binary relations. (Contributed by NM, 28-Mar-2007.) (Revised by Mario Carneiro, 8-Feb-2015.)
𝐴𝐵       (𝐶𝐴𝐷𝐶𝐵𝐷)

Theoremnfbrd 3973 Deduction version of bound-variable hypothesis builder nfbr 3974. (Contributed by NM, 13-Dec-2005.) (Revised by Mario Carneiro, 14-Oct-2016.)
(𝜑𝑥𝐴)    &   (𝜑𝑥𝑅)    &   (𝜑𝑥𝐵)       (𝜑 → Ⅎ𝑥 𝐴𝑅𝐵)

Theoremnfbr 3974 Bound-variable hypothesis builder for binary relation. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 14-Oct-2016.)
𝑥𝐴    &   𝑥𝑅    &   𝑥𝐵       𝑥 𝐴𝑅𝐵

Theorembrab1 3975* Relationship between a binary relation and a class abstraction. (Contributed by Andrew Salmon, 8-Jul-2011.)
(𝑥𝑅𝐴𝑥 ∈ {𝑧𝑧𝑅𝐴})

Theorembr0 3976 The empty binary relation never holds. (Contributed by NM, 23-Aug-2018.)
¬ 𝐴𝐵

Theorembrne0 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.)
(𝐴𝑅𝐵𝑅 ≠ ∅)

Theorembrm 3978* If two sets are in a binary relation, the relation is inhabited. (Contributed by Jim Kingdon, 31-Dec-2023.)
(𝐴𝑅𝐵 → ∃𝑥 𝑥𝑅)

Theorembrun 3979 The union of two binary relations. (Contributed by NM, 21-Dec-2008.)
(𝐴(𝑅𝑆)𝐵 ↔ (𝐴𝑅𝐵𝐴𝑆𝐵))

Theorembrin 3980 The intersection of two relations. (Contributed by FL, 7-Oct-2008.)
(𝐴(𝑅𝑆)𝐵 ↔ (𝐴𝑅𝐵𝐴𝑆𝐵))

Theorembrdif 3981 The difference of two binary relations. (Contributed by Scott Fenton, 11-Apr-2011.)
(𝐴(𝑅𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ ¬ 𝐴𝑆𝐵))

Theoremsbcbrg 3982 Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
(𝐴𝐷 → ([𝐴 / 𝑥]𝐵𝑅𝐶𝐴 / 𝑥𝐵𝐴 / 𝑥𝑅𝐴 / 𝑥𝐶))

Theoremsbcbr12g 3983* Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.)
(𝐴𝐷 → ([𝐴 / 𝑥]𝐵𝑅𝐶𝐴 / 𝑥𝐵𝑅𝐴 / 𝑥𝐶))

Theoremsbcbr1g 3984* Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.)
(𝐴𝐷 → ([𝐴 / 𝑥]𝐵𝑅𝐶𝐴 / 𝑥𝐵𝑅𝐶))

Theoremsbcbr2g 3985* Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.)
(𝐴𝐷 → ([𝐴 / 𝑥]𝐵𝑅𝐶𝐵𝑅𝐴 / 𝑥𝐶))

Theorembrralrspcev 3986* Restricted existential specialization with a restricted universal quantifier over a relation, closed form. (Contributed by AV, 20-Aug-2022.)
((𝐵𝑋 ∧ ∀𝑦𝑌 𝐴𝑅𝐵) → ∃𝑥𝑋𝑦𝑌 𝐴𝑅𝑥)

Theorembrimralrspcev 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)

Syntaxcopab 3988 Extend class notation to include ordered-pair class abstraction (class builder).
class {⟨𝑥, 𝑦⟩ ∣ 𝜑}

Syntaxcmpt 3989 Extend the definition of a class to include maps-to notation for defining a function via a rule.
class (𝑥𝐴𝐵)

Definitiondf-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.)
{⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}

Definitiondf-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.)
(𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}

Theoremopabss 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.)
{⟨𝑥, 𝑦⟩ ∣ 𝑥𝑅𝑦} ⊆ 𝑅

Theoremopabbid 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.)
𝑥𝜑    &   𝑦𝜑    &   (𝜑 → (𝜓𝜒))       (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑥, 𝑦⟩ ∣ 𝜒})

Theoremopabbidv 3994* Equivalent wff's yield equal ordered-pair class abstractions (deduction form). (Contributed by NM, 15-May-1995.)
(𝜑 → (𝜓𝜒))       (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑥, 𝑦⟩ ∣ 𝜒})

Theoremopabbii 3995 Equivalent wff's yield equal class abstractions. (Contributed by NM, 15-May-1995.)
(𝜑𝜓)       {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓}

Theoremnfopab 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.)
𝑧𝜑       𝑧{⟨𝑥, 𝑦⟩ ∣ 𝜑}

Theoremnfopab1 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.)
𝑥{⟨𝑥, 𝑦⟩ ∣ 𝜑}

Theoremnfopab2 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.)
𝑦{⟨𝑥, 𝑦⟩ ∣ 𝜑}

Theoremcbvopab 3999* Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 14-Sep-2003.)
𝑧𝜑    &   𝑤𝜑    &   𝑥𝜓    &   𝑦𝜓    &   ((𝑥 = 𝑧𝑦 = 𝑤) → (𝜑𝜓))       {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑧, 𝑤⟩ ∣ 𝜓}

Theoremcbvopabv 4000* Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 15-Oct-1996.)
((𝑥 = 𝑧𝑦 = 𝑤) → (𝜑𝜓))       {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑧, 𝑤⟩ ∣ 𝜓}

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13283
 Copyright terms: Public domain < Previous  Next >