Theorem List for Intuitionistic Logic Explorer - 3901-4000 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | breq 3901 |
Equality theorem for binary relations. (Contributed by NM,
4-Jun-1995.)
|
⊢ (𝑅 = 𝑆 → (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵)) |
|
Theorem | breq1 3902 |
Equality theorem for a binary relation. (Contributed by NM,
31-Dec-1993.)
|
⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)) |
|
Theorem | breq2 3903 |
Equality theorem for a binary relation. (Contributed by NM,
31-Dec-1993.)
|
⊢ (𝐴 = 𝐵 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵)) |
|
Theorem | breq12 3904 |
Equality theorem for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)) |
|
Theorem | breqi 3905 |
Equality inference for binary relations. (Contributed by NM,
19-Feb-2005.)
|
⊢ 𝑅 = 𝑆 ⇒ ⊢ (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵) |
|
Theorem | breq1i 3906 |
Equality inference for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶) |
|
Theorem | breq2i 3907 |
Equality inference for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵) |
|
Theorem | breq12i 3908 |
Equality inference for a binary relation. (Contributed by NM,
8-Feb-1996.) (Proof shortened by Eric Schmidt, 4-Apr-2007.)
|
⊢ 𝐴 = 𝐵
& ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷) |
|
Theorem | breq1d 3909 |
Equality deduction for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)) |
|
Theorem | breqd 3910 |
Equality deduction for a binary relation. (Contributed by NM,
29-Oct-2011.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶𝐴𝐷 ↔ 𝐶𝐵𝐷)) |
|
Theorem | breq2d 3911 |
Equality deduction for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵)) |
|
Theorem | breq12d 3912 |
Equality deduction for a binary relation. (Contributed by NM,
8-Feb-1996.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)) |
|
Theorem | breq123d 3913 |
Equality deduction for a binary relation. (Contributed by NM,
29-Oct-2011.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝑅 = 𝑆)
& ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑆𝐷)) |
|
Theorem | breqdi 3914 |
Equality deduction for a binary relation. (Contributed by Thierry
Arnoux, 5-Oct-2020.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐶𝐴𝐷) ⇒ ⊢ (𝜑 → 𝐶𝐵𝐷) |
|
Theorem | breqan12d 3915 |
Equality deduction for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜓 → 𝐶 = 𝐷) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)) |
|
Theorem | breqan12rd 3916 |
Equality deduction for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜓 → 𝐶 = 𝐷) ⇒ ⊢ ((𝜓 ∧ 𝜑) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)) |
|
Theorem | nbrne1 3917 |
Two classes are different if they don't have the same relationship to a
third class. (Contributed by NM, 3-Jun-2012.)
|
⊢ ((𝐴𝑅𝐵 ∧ ¬ 𝐴𝑅𝐶) → 𝐵 ≠ 𝐶) |
|
Theorem | nbrne2 3918 |
Two classes are different if they don't have the same relationship to a
third class. (Contributed by NM, 3-Jun-2012.)
|
⊢ ((𝐴𝑅𝐶 ∧ ¬ 𝐵𝑅𝐶) → 𝐴 ≠ 𝐵) |
|
Theorem | eqbrtri 3919 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 5-Aug-1993.)
|
⊢ 𝐴 = 𝐵
& ⊢ 𝐵𝑅𝐶 ⇒ ⊢ 𝐴𝑅𝐶 |
|
Theorem | eqbrtrd 3920 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 8-Oct-1999.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
|
Theorem | eqbrtrri 3921 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 5-Aug-1993.)
|
⊢ 𝐴 = 𝐵
& ⊢ 𝐴𝑅𝐶 ⇒ ⊢ 𝐵𝑅𝐶 |
|
Theorem | eqbrtrrd 3922 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 24-Oct-1999.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐴𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐵𝑅𝐶) |
|
Theorem | breqtri 3923 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 5-Aug-1993.)
|
⊢ 𝐴𝑅𝐵
& ⊢ 𝐵 = 𝐶 ⇒ ⊢ 𝐴𝑅𝐶 |
|
Theorem | breqtrd 3924 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 24-Oct-1999.)
|
⊢ (𝜑 → 𝐴𝑅𝐵)
& ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
|
Theorem | breqtrri 3925 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 5-Aug-1993.)
|
⊢ 𝐴𝑅𝐵
& ⊢ 𝐶 = 𝐵 ⇒ ⊢ 𝐴𝑅𝐶 |
|
Theorem | breqtrrd 3926 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 24-Oct-1999.)
|
⊢ (𝜑 → 𝐴𝑅𝐵)
& ⊢ (𝜑 → 𝐶 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
|
Theorem | 3brtr3i 3927 |
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 11-Aug-1999.)
|
⊢ 𝐴𝑅𝐵
& ⊢ 𝐴 = 𝐶
& ⊢ 𝐵 = 𝐷 ⇒ ⊢ 𝐶𝑅𝐷 |
|
Theorem | 3brtr4i 3928 |
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 11-Aug-1999.)
|
⊢ 𝐴𝑅𝐵
& ⊢ 𝐶 = 𝐴
& ⊢ 𝐷 = 𝐵 ⇒ ⊢ 𝐶𝑅𝐷 |
|
Theorem | 3brtr3d 3929 |
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 18-Oct-1999.)
|
⊢ (𝜑 → 𝐴𝑅𝐵)
& ⊢ (𝜑 → 𝐴 = 𝐶)
& ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → 𝐶𝑅𝐷) |
|
Theorem | 3brtr4d 3930 |
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 21-Feb-2005.)
|
⊢ (𝜑 → 𝐴𝑅𝐵)
& ⊢ (𝜑 → 𝐶 = 𝐴)
& ⊢ (𝜑 → 𝐷 = 𝐵) ⇒ ⊢ (𝜑 → 𝐶𝑅𝐷) |
|
Theorem | 3brtr3g 3931 |
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 16-Jan-1997.)
|
⊢ (𝜑 → 𝐴𝑅𝐵)
& ⊢ 𝐴 = 𝐶
& ⊢ 𝐵 = 𝐷 ⇒ ⊢ (𝜑 → 𝐶𝑅𝐷) |
|
Theorem | 3brtr4g 3932 |
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 16-Jan-1997.)
|
⊢ (𝜑 → 𝐴𝑅𝐵)
& ⊢ 𝐶 = 𝐴
& ⊢ 𝐷 = 𝐵 ⇒ ⊢ (𝜑 → 𝐶𝑅𝐷) |
|
Theorem | eqbrtrid 3933 |
B chained equality inference for a binary relation. (Contributed by NM,
11-Oct-1999.)
|
⊢ 𝐴 = 𝐵
& ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
|
Theorem | eqbrtrrid 3934 |
B chained equality inference for a binary relation. (Contributed by NM,
17-Sep-2004.)
|
⊢ 𝐵 = 𝐴
& ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
|
Theorem | breqtrid 3935 |
B chained equality inference for a binary relation. (Contributed by NM,
11-Oct-1999.)
|
⊢ 𝐴𝑅𝐵
& ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
|
Theorem | breqtrrid 3936 |
B chained equality inference for a binary relation. (Contributed by NM,
24-Apr-2005.)
|
⊢ 𝐴𝑅𝐵
& ⊢ (𝜑 → 𝐶 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
|
Theorem | eqbrtrdi 3937 |
A chained equality inference for a binary relation. (Contributed by NM,
12-Oct-1999.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ 𝐵𝑅𝐶 ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
|
Theorem | eqbrtrrdi 3938 |
A chained equality inference for a binary relation. (Contributed by NM,
4-Jan-2006.)
|
⊢ (𝜑 → 𝐵 = 𝐴)
& ⊢ 𝐵𝑅𝐶 ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
|
Theorem | breqtrdi 3939 |
A chained equality inference for a binary relation. (Contributed by NM,
11-Oct-1999.)
|
⊢ (𝜑 → 𝐴𝑅𝐵)
& ⊢ 𝐵 = 𝐶 ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
|
Theorem | breqtrrdi 3940 |
A chained equality inference for a binary relation. (Contributed by NM,
24-Apr-2005.)
|
⊢ (𝜑 → 𝐴𝑅𝐵)
& ⊢ 𝐶 = 𝐵 ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
|
Theorem | ssbrd 3941 |
Deduction from a subclass relationship of binary relations.
(Contributed by NM, 30-Apr-2004.)
|
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐶𝐴𝐷 → 𝐶𝐵𝐷)) |
|
Theorem | ssbri 3942 |
Inference from a subclass relationship of binary relations.
(Contributed by NM, 28-Mar-2007.) (Revised by Mario Carneiro,
8-Feb-2015.)
|
⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ (𝐶𝐴𝐷 → 𝐶𝐵𝐷) |
|
Theorem | nfbrd 3943 |
Deduction version of bound-variable hypothesis builder nfbr 3944.
(Contributed by NM, 13-Dec-2005.) (Revised by Mario Carneiro,
14-Oct-2016.)
|
⊢ (𝜑 → Ⅎ𝑥𝐴)
& ⊢ (𝜑 → Ⅎ𝑥𝑅)
& ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥 𝐴𝑅𝐵) |
|
Theorem | nfbr 3944 |
Bound-variable hypothesis builder for binary relation. (Contributed by
NM, 1-Sep-1999.) (Revised by Mario Carneiro, 14-Oct-2016.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝑅
& ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐴𝑅𝐵 |
|
Theorem | brab1 3945* |
Relationship between a binary relation and a class abstraction.
(Contributed by Andrew Salmon, 8-Jul-2011.)
|
⊢ (𝑥𝑅𝐴 ↔ 𝑥 ∈ {𝑧 ∣ 𝑧𝑅𝐴}) |
|
Theorem | br0 3946 |
The empty binary relation never holds. (Contributed by NM,
23-Aug-2018.)
|
⊢ ¬ 𝐴∅𝐵 |
|
Theorem | brne0 3947 |
If two sets are in a binary relation, the relation cannot be empty. In
fact, the relation is also inhabited, as seen at brm 3948.
(Contributed by
Alexander van der Vekens, 7-Jul-2018.)
|
⊢ (𝐴𝑅𝐵 → 𝑅 ≠ ∅) |
|
Theorem | brm 3948* |
If two sets are in a binary relation, the relation is inhabited.
(Contributed by Jim Kingdon, 31-Dec-2023.)
|
⊢ (𝐴𝑅𝐵 → ∃𝑥 𝑥 ∈ 𝑅) |
|
Theorem | brun 3949 |
The union of two binary relations. (Contributed by NM, 21-Dec-2008.)
|
⊢ (𝐴(𝑅 ∪ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∨ 𝐴𝑆𝐵)) |
|
Theorem | brin 3950 |
The intersection of two relations. (Contributed by FL, 7-Oct-2008.)
|
⊢ (𝐴(𝑅 ∩ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ 𝐴𝑆𝐵)) |
|
Theorem | brdif 3951 |
The difference of two binary relations. (Contributed by Scott Fenton,
11-Apr-2011.)
|
⊢ (𝐴(𝑅 ∖ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ ¬ 𝐴𝑆𝐵)) |
|
Theorem | sbcbrg 3952 |
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 3953* |
Move substitution in and out of a binary relation. (Contributed by NM,
13-Dec-2005.)
|
⊢ (𝐴 ∈ 𝐷 → ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵𝑅⦋𝐴 / 𝑥⦌𝐶)) |
|
Theorem | sbcbr1g 3954* |
Move substitution in and out of a binary relation. (Contributed by NM,
13-Dec-2005.)
|
⊢ (𝐴 ∈ 𝐷 → ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵𝑅𝐶)) |
|
Theorem | sbcbr2g 3955* |
Move substitution in and out of a binary relation. (Contributed by NM,
13-Dec-2005.)
|
⊢ (𝐴 ∈ 𝐷 → ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ 𝐵𝑅⦋𝐴 / 𝑥⦌𝐶)) |
|
Theorem | brralrspcev 3956* |
Restricted existential specialization with a restricted universal
quantifier over a relation, closed form. (Contributed by AV,
20-Aug-2022.)
|
⊢ ((𝐵 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝑌 𝐴𝑅𝐵) → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐴𝑅𝑥) |
|
Theorem | brimralrspcev 3957* |
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 3958 |
Extend class notation to include ordered-pair class abstraction (class
builder).
|
class {〈𝑥, 𝑦〉 ∣ 𝜑} |
|
Syntax | cmpt 3959 |
Extend the definition of a class to include maps-to notation for defining
a function via a rule.
|
class (𝑥 ∈ 𝐴 ↦ 𝐵) |
|
Definition | df-opab 3960* |
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 3961* |
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 3962* |
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 3963 |
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 3964* |
Equivalent wff's yield equal ordered-pair class abstractions (deduction
form). (Contributed by NM, 15-May-1995.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝜓} = {〈𝑥, 𝑦〉 ∣ 𝜒}) |
|
Theorem | opabbii 3965 |
Equivalent wff's yield equal class abstractions. (Contributed by NM,
15-May-1995.)
|
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑦〉 ∣ 𝜓} |
|
Theorem | nfopab 3966* |
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 3967 |
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 3968 |
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 3969* |
Rule used to change bound variables in an ordered-pair class
abstraction, using implicit substitution. (Contributed by NM,
14-Sep-2003.)
|
⊢ Ⅎ𝑧𝜑
& ⊢ Ⅎ𝑤𝜑
& ⊢ Ⅎ𝑥𝜓
& ⊢ Ⅎ𝑦𝜓
& ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑧, 𝑤〉 ∣ 𝜓} |
|
Theorem | cbvopabv 3970* |
Rule used to change bound variables in an ordered-pair class
abstraction, using implicit substitution. (Contributed by NM,
15-Oct-1996.)
|
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑧, 𝑤〉 ∣ 𝜓} |
|
Theorem | cbvopab1 3971* |
Change first bound variable in an ordered-pair class abstraction, using
explicit substitution. (Contributed by NM, 6-Oct-2004.) (Revised by
Mario Carneiro, 14-Oct-2016.)
|
⊢ Ⅎ𝑧𝜑
& ⊢ Ⅎ𝑥𝜓
& ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑧, 𝑦〉 ∣ 𝜓} |
|
Theorem | cbvopab2 3972* |
Change second bound variable in an ordered-pair class abstraction, using
explicit substitution. (Contributed by NM, 22-Aug-2013.)
|
⊢ Ⅎ𝑧𝜑
& ⊢ Ⅎ𝑦𝜓
& ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑧〉 ∣ 𝜓} |
|
Theorem | cbvopab1s 3973* |
Change first bound variable in an ordered-pair class abstraction, using
explicit substitution. (Contributed by NM, 31-Jul-2003.)
|
⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑧, 𝑦〉 ∣ [𝑧 / 𝑥]𝜑} |
|
Theorem | cbvopab1v 3974* |
Rule used to change the first bound variable in an ordered pair
abstraction, using implicit substitution. (Contributed by NM,
31-Jul-2003.) (Proof shortened by Eric Schmidt, 4-Apr-2007.)
|
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑧, 𝑦〉 ∣ 𝜓} |
|
Theorem | cbvopab2v 3975* |
Rule used to change the second bound variable in an ordered pair
abstraction, using implicit substitution. (Contributed by NM,
2-Sep-1999.)
|
⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑧〉 ∣ 𝜓} |
|
Theorem | csbopabg 3976* |
Move substitution into a class abstraction. (Contributed by NM,
6-Aug-2007.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
|
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{〈𝑦, 𝑧〉 ∣ 𝜑} = {〈𝑦, 𝑧〉 ∣ [𝐴 / 𝑥]𝜑}) |
|
Theorem | unopab 3977 |
Union of two ordered pair class abstractions. (Contributed by NM,
30-Sep-2002.)
|
⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} ∪ {〈𝑥, 𝑦〉 ∣ 𝜓}) = {〈𝑥, 𝑦〉 ∣ (𝜑 ∨ 𝜓)} |
|
Theorem | mpteq12f 3978 |
An equality theorem for the maps-to notation. (Contributed by Mario
Carneiro, 16-Dec-2013.)
|
⊢ ((∀𝑥 𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐷) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) |
|
Theorem | mpteq12dva 3979* |
An equality inference for the maps-to notation. (Contributed by Mario
Carneiro, 26-Jan-2017.)
|
⊢ (𝜑 → 𝐴 = 𝐶)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) |
|
Theorem | mpteq12dv 3980* |
An equality inference for the maps-to notation. (Contributed by NM,
24-Aug-2011.) (Revised by Mario Carneiro, 16-Dec-2013.)
|
⊢ (𝜑 → 𝐴 = 𝐶)
& ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) |
|
Theorem | mpteq12 3981* |
An equality theorem for the maps-to notation. (Contributed by NM,
16-Dec-2013.)
|
⊢ ((𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐷) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) |
|
Theorem | mpteq1 3982* |
An equality theorem for the maps-to notation. (Contributed by Mario
Carneiro, 16-Dec-2013.)
|
⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶)) |
|
Theorem | mpteq1d 3983* |
An equality theorem for the maps-to notation. (Contributed by Mario
Carneiro, 11-Jun-2016.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶)) |
|
Theorem | mpteq2ia 3984 |
An equality inference for the maps-to notation. (Contributed by Mario
Carneiro, 16-Dec-2013.)
|
⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶) |
|
Theorem | mpteq2i 3985 |
An equality inference for the maps-to notation. (Contributed by Mario
Carneiro, 16-Dec-2013.)
|
⊢ 𝐵 = 𝐶 ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶) |
|
Theorem | mpteq12i 3986 |
An equality inference for the maps-to notation. (Contributed by Scott
Fenton, 27-Oct-2010.) (Revised by Mario Carneiro, 16-Dec-2013.)
|
⊢ 𝐴 = 𝐶
& ⊢ 𝐵 = 𝐷 ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷) |
|
Theorem | mpteq2da 3987 |
Slightly more general equality inference for the maps-to notation.
(Contributed by FL, 14-Sep-2013.) (Revised by Mario Carneiro,
16-Dec-2013.)
|
⊢ Ⅎ𝑥𝜑
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)) |
|
Theorem | mpteq2dva 3988* |
Slightly more general equality inference for the maps-to notation.
(Contributed by Scott Fenton, 25-Apr-2012.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)) |
|
Theorem | mpteq2dv 3989* |
An equality inference for the maps-to notation. (Contributed by Mario
Carneiro, 23-Aug-2014.)
|
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)) |
|
Theorem | nfmpt 3990* |
Bound-variable hypothesis builder for the maps-to notation.
(Contributed by NM, 20-Feb-2013.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ↦ 𝐵) |
|
Theorem | nfmpt1 3991 |
Bound-variable hypothesis builder for the maps-to notation.
(Contributed by FL, 17-Feb-2008.)
|
⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵) |
|
Theorem | cbvmptf 3992* |
Rule to change the bound variable in a maps-to function, using implicit
substitution. This version has bound-variable hypotheses in place of
distinct variable conditions. (Contributed by Thierry Arnoux,
9-Mar-2017.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑦𝐴
& ⊢ Ⅎ𝑦𝐵
& ⊢ Ⅎ𝑥𝐶
& ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶) |
|
Theorem | cbvmpt 3993* |
Rule to change the bound variable in a maps-to function, using implicit
substitution. This version has bound-variable hypotheses in place of
distinct variable conditions. (Contributed by NM, 11-Sep-2011.)
|
⊢ Ⅎ𝑦𝐵
& ⊢ Ⅎ𝑥𝐶
& ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶) |
|
Theorem | cbvmptv 3994* |
Rule to change the bound variable in a maps-to function, using implicit
substitution. (Contributed by Mario Carneiro, 19-Feb-2013.)
|
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶) |
|
Theorem | mptv 3995* |
Function with universal domain in maps-to notation. (Contributed by NM,
16-Aug-2013.)
|
⊢ (𝑥 ∈ V ↦ 𝐵) = {〈𝑥, 𝑦〉 ∣ 𝑦 = 𝐵} |
|
2.1.24 Transitive classes
|
|
Syntax | wtr 3996 |
Extend wff notation to include transitive classes. Notation from
[TakeutiZaring] p. 35.
|
wff Tr 𝐴 |
|
Definition | df-tr 3997 |
Define the transitive class predicate. Definition of [Enderton] p. 71
extended to arbitrary classes. For alternate definitions, see dftr2 3998
(which is suggestive of the word "transitive"), dftr3 4000, dftr4 4001, and
dftr5 3999. The term "complete" is used
instead of "transitive" in
Definition 3 of [Suppes] p. 130.
(Contributed by NM, 29-Aug-1993.)
|
⊢ (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴) |
|
Theorem | dftr2 3998* |
An alternate way of defining a transitive class. Exercise 7 of
[TakeutiZaring] p. 40.
(Contributed by NM, 24-Apr-1994.)
|
⊢ (Tr 𝐴 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴)) |
|
Theorem | dftr5 3999* |
An alternate way of defining a transitive class. (Contributed by NM,
20-Mar-2004.)
|
⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 𝑦 ∈ 𝐴) |
|
Theorem | dftr3 4000* |
An alternate way of defining a transitive class. Definition 7.1 of
[TakeutiZaring] p. 35.
(Contributed by NM, 29-Aug-1993.)
|
⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴) |