Type | Label | Description |
Statement |
|
Theorem | 0disj 4001 |
Any collection of empty sets is disjoint. (Contributed by Mario Carneiro,
14-Nov-2016.)
|
⊢ Disj 𝑥 ∈ 𝐴 ∅ |
|
Theorem | disjxsn 4002* |
A singleton collection is disjoint. (Contributed by Mario Carneiro,
14-Nov-2016.)
|
⊢ Disj 𝑥 ∈ {𝐴}𝐵 |
|
Theorem | disjx0 4003 |
An empty collection is disjoint. (Contributed by Mario Carneiro,
14-Nov-2016.)
|
⊢ Disj 𝑥 ∈ ∅ 𝐵 |
|
2.1.22 Binary relations
|
|
Syntax | wbr 4004 |
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 4005 |
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 4896). (Contributed by NM, 31-Dec-1993.)
|
⊢ (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅) |
|
Theorem | breq 4006 |
Equality theorem for binary relations. (Contributed by NM,
4-Jun-1995.)
|
⊢ (𝑅 = 𝑆 → (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵)) |
|
Theorem | breq1 4007 |
Equality theorem for a binary relation. (Contributed by NM,
31-Dec-1993.)
|
⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)) |
|
Theorem | breq2 4008 |
Equality theorem for a binary relation. (Contributed by NM,
31-Dec-1993.)
|
⊢ (𝐴 = 𝐵 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵)) |
|
Theorem | breq12 4009 |
Equality theorem for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)) |
|
Theorem | breqi 4010 |
Equality inference for binary relations. (Contributed by NM,
19-Feb-2005.)
|
⊢ 𝑅 = 𝑆 ⇒ ⊢ (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵) |
|
Theorem | breq1i 4011 |
Equality inference for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶) |
|
Theorem | breq2i 4012 |
Equality inference for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵) |
|
Theorem | breq12i 4013 |
Equality inference for a binary relation. (Contributed by NM,
8-Feb-1996.) (Proof shortened by Eric Schmidt, 4-Apr-2007.)
|
⊢ 𝐴 = 𝐵
& ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷) |
|
Theorem | breq1d 4014 |
Equality deduction for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)) |
|
Theorem | breqd 4015 |
Equality deduction for a binary relation. (Contributed by NM,
29-Oct-2011.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶𝐴𝐷 ↔ 𝐶𝐵𝐷)) |
|
Theorem | breq2d 4016 |
Equality deduction for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵)) |
|
Theorem | breq12d 4017 |
Equality deduction for a binary relation. (Contributed by NM,
8-Feb-1996.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)) |
|
Theorem | breq123d 4018 |
Equality deduction for a binary relation. (Contributed by NM,
29-Oct-2011.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝑅 = 𝑆)
& ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑆𝐷)) |
|
Theorem | breqdi 4019 |
Equality deduction for a binary relation. (Contributed by Thierry
Arnoux, 5-Oct-2020.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐶𝐴𝐷) ⇒ ⊢ (𝜑 → 𝐶𝐵𝐷) |
|
Theorem | breqan12d 4020 |
Equality deduction for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜓 → 𝐶 = 𝐷) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)) |
|
Theorem | breqan12rd 4021 |
Equality deduction for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜓 → 𝐶 = 𝐷) ⇒ ⊢ ((𝜓 ∧ 𝜑) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)) |
|
Theorem | eqnbrtrd 4022 |
Substitution of equal classes into the negation of a binary relation.
(Contributed by Glauco Siliprandi, 3-Jan-2021.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → ¬ 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → ¬ 𝐴𝑅𝐶) |
|
Theorem | nbrne1 4023 |
Two classes are different if they don't have the same relationship to a
third class. (Contributed by NM, 3-Jun-2012.)
|
⊢ ((𝐴𝑅𝐵 ∧ ¬ 𝐴𝑅𝐶) → 𝐵 ≠ 𝐶) |
|
Theorem | nbrne2 4024 |
Two classes are different if they don't have the same relationship to a
third class. (Contributed by NM, 3-Jun-2012.)
|
⊢ ((𝐴𝑅𝐶 ∧ ¬ 𝐵𝑅𝐶) → 𝐴 ≠ 𝐵) |
|
Theorem | eqbrtri 4025 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 5-Aug-1993.)
|
⊢ 𝐴 = 𝐵
& ⊢ 𝐵𝑅𝐶 ⇒ ⊢ 𝐴𝑅𝐶 |
|
Theorem | eqbrtrd 4026 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 8-Oct-1999.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
|
Theorem | eqbrtrri 4027 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 5-Aug-1993.)
|
⊢ 𝐴 = 𝐵
& ⊢ 𝐴𝑅𝐶 ⇒ ⊢ 𝐵𝑅𝐶 |
|
Theorem | eqbrtrrd 4028 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 24-Oct-1999.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐴𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐵𝑅𝐶) |
|
Theorem | breqtri 4029 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 5-Aug-1993.)
|
⊢ 𝐴𝑅𝐵
& ⊢ 𝐵 = 𝐶 ⇒ ⊢ 𝐴𝑅𝐶 |
|
Theorem | breqtrd 4030 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 24-Oct-1999.)
|
⊢ (𝜑 → 𝐴𝑅𝐵)
& ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
|
Theorem | breqtrri 4031 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 5-Aug-1993.)
|
⊢ 𝐴𝑅𝐵
& ⊢ 𝐶 = 𝐵 ⇒ ⊢ 𝐴𝑅𝐶 |
|
Theorem | breqtrrd 4032 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 24-Oct-1999.)
|
⊢ (𝜑 → 𝐴𝑅𝐵)
& ⊢ (𝜑 → 𝐶 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
|
Theorem | 3brtr3i 4033 |
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 11-Aug-1999.)
|
⊢ 𝐴𝑅𝐵
& ⊢ 𝐴 = 𝐶
& ⊢ 𝐵 = 𝐷 ⇒ ⊢ 𝐶𝑅𝐷 |
|
Theorem | 3brtr4i 4034 |
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 11-Aug-1999.)
|
⊢ 𝐴𝑅𝐵
& ⊢ 𝐶 = 𝐴
& ⊢ 𝐷 = 𝐵 ⇒ ⊢ 𝐶𝑅𝐷 |
|
Theorem | 3brtr3d 4035 |
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 18-Oct-1999.)
|
⊢ (𝜑 → 𝐴𝑅𝐵)
& ⊢ (𝜑 → 𝐴 = 𝐶)
& ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → 𝐶𝑅𝐷) |
|
Theorem | 3brtr4d 4036 |
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 21-Feb-2005.)
|
⊢ (𝜑 → 𝐴𝑅𝐵)
& ⊢ (𝜑 → 𝐶 = 𝐴)
& ⊢ (𝜑 → 𝐷 = 𝐵) ⇒ ⊢ (𝜑 → 𝐶𝑅𝐷) |
|
Theorem | 3brtr3g 4037 |
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 16-Jan-1997.)
|
⊢ (𝜑 → 𝐴𝑅𝐵)
& ⊢ 𝐴 = 𝐶
& ⊢ 𝐵 = 𝐷 ⇒ ⊢ (𝜑 → 𝐶𝑅𝐷) |
|
Theorem | 3brtr4g 4038 |
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 16-Jan-1997.)
|
⊢ (𝜑 → 𝐴𝑅𝐵)
& ⊢ 𝐶 = 𝐴
& ⊢ 𝐷 = 𝐵 ⇒ ⊢ (𝜑 → 𝐶𝑅𝐷) |
|
Theorem | eqbrtrid 4039 |
B chained equality inference for a binary relation. (Contributed by NM,
11-Oct-1999.)
|
⊢ 𝐴 = 𝐵
& ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
|
Theorem | eqbrtrrid 4040 |
B chained equality inference for a binary relation. (Contributed by NM,
17-Sep-2004.)
|
⊢ 𝐵 = 𝐴
& ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
|
Theorem | breqtrid 4041 |
B chained equality inference for a binary relation. (Contributed by NM,
11-Oct-1999.)
|
⊢ 𝐴𝑅𝐵
& ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
|
Theorem | breqtrrid 4042 |
B chained equality inference for a binary relation. (Contributed by NM,
24-Apr-2005.)
|
⊢ 𝐴𝑅𝐵
& ⊢ (𝜑 → 𝐶 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
|
Theorem | eqbrtrdi 4043 |
A chained equality inference for a binary relation. (Contributed by NM,
12-Oct-1999.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ 𝐵𝑅𝐶 ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
|
Theorem | eqbrtrrdi 4044 |
A chained equality inference for a binary relation. (Contributed by NM,
4-Jan-2006.)
|
⊢ (𝜑 → 𝐵 = 𝐴)
& ⊢ 𝐵𝑅𝐶 ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
|
Theorem | breqtrdi 4045 |
A chained equality inference for a binary relation. (Contributed by NM,
11-Oct-1999.)
|
⊢ (𝜑 → 𝐴𝑅𝐵)
& ⊢ 𝐵 = 𝐶 ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
|
Theorem | breqtrrdi 4046 |
A chained equality inference for a binary relation. (Contributed by NM,
24-Apr-2005.)
|
⊢ (𝜑 → 𝐴𝑅𝐵)
& ⊢ 𝐶 = 𝐵 ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
|
Theorem | ssbrd 4047 |
Deduction from a subclass relationship of binary relations.
(Contributed by NM, 30-Apr-2004.)
|
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐶𝐴𝐷 → 𝐶𝐵𝐷)) |
|
Theorem | ssbri 4048 |
Inference from a subclass relationship of binary relations.
(Contributed by NM, 28-Mar-2007.) (Revised by Mario Carneiro,
8-Feb-2015.)
|
⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ (𝐶𝐴𝐷 → 𝐶𝐵𝐷) |
|
Theorem | nfbrd 4049 |
Deduction version of bound-variable hypothesis builder nfbr 4050.
(Contributed by NM, 13-Dec-2005.) (Revised by Mario Carneiro,
14-Oct-2016.)
|
⊢ (𝜑 → Ⅎ𝑥𝐴)
& ⊢ (𝜑 → Ⅎ𝑥𝑅)
& ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥 𝐴𝑅𝐵) |
|
Theorem | nfbr 4050 |
Bound-variable hypothesis builder for binary relation. (Contributed by
NM, 1-Sep-1999.) (Revised by Mario Carneiro, 14-Oct-2016.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝑅
& ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐴𝑅𝐵 |
|
Theorem | brab1 4051* |
Relationship between a binary relation and a class abstraction.
(Contributed by Andrew Salmon, 8-Jul-2011.)
|
⊢ (𝑥𝑅𝐴 ↔ 𝑥 ∈ {𝑧 ∣ 𝑧𝑅𝐴}) |
|
Theorem | br0 4052 |
The empty binary relation never holds. (Contributed by NM,
23-Aug-2018.)
|
⊢ ¬ 𝐴∅𝐵 |
|
Theorem | brne0 4053 |
If two sets are in a binary relation, the relation cannot be empty. In
fact, the relation is also inhabited, as seen at brm 4054.
(Contributed by
Alexander van der Vekens, 7-Jul-2018.)
|
⊢ (𝐴𝑅𝐵 → 𝑅 ≠ ∅) |
|
Theorem | brm 4054* |
If two sets are in a binary relation, the relation is inhabited.
(Contributed by Jim Kingdon, 31-Dec-2023.)
|
⊢ (𝐴𝑅𝐵 → ∃𝑥 𝑥 ∈ 𝑅) |
|
Theorem | brun 4055 |
The union of two binary relations. (Contributed by NM, 21-Dec-2008.)
|
⊢ (𝐴(𝑅 ∪ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∨ 𝐴𝑆𝐵)) |
|
Theorem | brin 4056 |
The intersection of two relations. (Contributed by FL, 7-Oct-2008.)
|
⊢ (𝐴(𝑅 ∩ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ 𝐴𝑆𝐵)) |
|
Theorem | brdif 4057 |
The difference of two binary relations. (Contributed by Scott Fenton,
11-Apr-2011.)
|
⊢ (𝐴(𝑅 ∖ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ ¬ 𝐴𝑆𝐵)) |
|
Theorem | sbcbrg 4058 |
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 4059* |
Move substitution in and out of a binary relation. (Contributed by NM,
13-Dec-2005.)
|
⊢ (𝐴 ∈ 𝐷 → ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵𝑅⦋𝐴 / 𝑥⦌𝐶)) |
|
Theorem | sbcbr1g 4060* |
Move substitution in and out of a binary relation. (Contributed by NM,
13-Dec-2005.)
|
⊢ (𝐴 ∈ 𝐷 → ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵𝑅𝐶)) |
|
Theorem | sbcbr2g 4061* |
Move substitution in and out of a binary relation. (Contributed by NM,
13-Dec-2005.)
|
⊢ (𝐴 ∈ 𝐷 → ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ 𝐵𝑅⦋𝐴 / 𝑥⦌𝐶)) |
|
Theorem | brralrspcev 4062* |
Restricted existential specialization with a restricted universal
quantifier over a relation, closed form. (Contributed by AV,
20-Aug-2022.)
|
⊢ ((𝐵 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝑌 𝐴𝑅𝐵) → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐴𝑅𝑥) |
|
Theorem | brimralrspcev 4063* |
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 4064 |
Extend class notation to include ordered-pair class abstraction (class
builder).
|
class {⟨𝑥, 𝑦⟩ ∣ 𝜑} |
|
Syntax | cmpt 4065 |
Extend the definition of a class to include maps-to notation for defining
a function via a rule.
|
class (𝑥 ∈ 𝐴 ↦ 𝐵) |
|
Definition | df-opab 4066* |
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 4067* |
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 4068* |
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 4069 |
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 4070* |
Equivalent wff's yield equal ordered-pair class abstractions (deduction
form). (Contributed by NM, 15-May-1995.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑥, 𝑦⟩ ∣ 𝜒}) |
|
Theorem | opabbii 4071 |
Equivalent wff's yield equal class abstractions. (Contributed by NM,
15-May-1995.)
|
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓} |
|
Theorem | nfopab 4072* |
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 4073 |
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 4074 |
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 4075* |
Rule used to change bound variables in an ordered-pair class
abstraction, using implicit substitution. (Contributed by NM,
14-Sep-2003.)
|
⊢ Ⅎ𝑧𝜑
& ⊢ Ⅎ𝑤𝜑
& ⊢ Ⅎ𝑥𝜓
& ⊢ Ⅎ𝑦𝜓
& ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑧, 𝑤⟩ ∣ 𝜓} |
|
Theorem | cbvopabv 4076* |
Rule used to change bound variables in an ordered-pair class
abstraction, using implicit substitution. (Contributed by NM,
15-Oct-1996.)
|
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑧, 𝑤⟩ ∣ 𝜓} |
|
Theorem | cbvopab1 4077* |
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 4078* |
Change second bound variable in an ordered-pair class abstraction, using
explicit substitution. (Contributed by NM, 22-Aug-2013.)
|
⊢ Ⅎ𝑧𝜑
& ⊢ Ⅎ𝑦𝜓
& ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑧⟩ ∣ 𝜓} |
|
Theorem | cbvopab1s 4079* |
Change first bound variable in an ordered-pair class abstraction, using
explicit substitution. (Contributed by NM, 31-Jul-2003.)
|
⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑧, 𝑦⟩ ∣ [𝑧 / 𝑥]𝜑} |
|
Theorem | cbvopab1v 4080* |
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 4081* |
Rule used to change the second bound variable in an ordered pair
abstraction, using implicit substitution. (Contributed by NM,
2-Sep-1999.)
|
⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑧⟩ ∣ 𝜓} |
|
Theorem | csbopabg 4082* |
Move substitution into a class abstraction. (Contributed by NM,
6-Aug-2007.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
|
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{⟨𝑦, 𝑧⟩ ∣ 𝜑} = {⟨𝑦, 𝑧⟩ ∣ [𝐴 / 𝑥]𝜑}) |
|
Theorem | unopab 4083 |
Union of two ordered pair class abstractions. (Contributed by NM,
30-Sep-2002.)
|
⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ∪ {⟨𝑥, 𝑦⟩ ∣ 𝜓}) = {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∨ 𝜓)} |
|
Theorem | mpteq12f 4084 |
An equality theorem for the maps-to notation. (Contributed by Mario
Carneiro, 16-Dec-2013.)
|
⊢ ((∀𝑥 𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐷) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) |
|
Theorem | mpteq12dva 4085* |
An equality inference for the maps-to notation. (Contributed by Mario
Carneiro, 26-Jan-2017.)
|
⊢ (𝜑 → 𝐴 = 𝐶)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) |
|
Theorem | mpteq12dv 4086* |
An equality inference for the maps-to notation. (Contributed by NM,
24-Aug-2011.) (Revised by Mario Carneiro, 16-Dec-2013.)
|
⊢ (𝜑 → 𝐴 = 𝐶)
& ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) |
|
Theorem | mpteq12 4087* |
An equality theorem for the maps-to notation. (Contributed by NM,
16-Dec-2013.)
|
⊢ ((𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐷) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) |
|
Theorem | mpteq1 4088* |
An equality theorem for the maps-to notation. (Contributed by Mario
Carneiro, 16-Dec-2013.)
|
⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶)) |
|
Theorem | mpteq1d 4089* |
An equality theorem for the maps-to notation. (Contributed by Mario
Carneiro, 11-Jun-2016.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶)) |
|
Theorem | mpteq2ia 4090 |
An equality inference for the maps-to notation. (Contributed by Mario
Carneiro, 16-Dec-2013.)
|
⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶) |
|
Theorem | mpteq2i 4091 |
An equality inference for the maps-to notation. (Contributed by Mario
Carneiro, 16-Dec-2013.)
|
⊢ 𝐵 = 𝐶 ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶) |
|
Theorem | mpteq12i 4092 |
An equality inference for the maps-to notation. (Contributed by Scott
Fenton, 27-Oct-2010.) (Revised by Mario Carneiro, 16-Dec-2013.)
|
⊢ 𝐴 = 𝐶
& ⊢ 𝐵 = 𝐷 ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷) |
|
Theorem | mpteq2da 4093 |
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 4094* |
Slightly more general equality inference for the maps-to notation.
(Contributed by Scott Fenton, 25-Apr-2012.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)) |
|
Theorem | mpteq2dv 4095* |
An equality inference for the maps-to notation. (Contributed by Mario
Carneiro, 23-Aug-2014.)
|
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)) |
|
Theorem | nfmpt 4096* |
Bound-variable hypothesis builder for the maps-to notation.
(Contributed by NM, 20-Feb-2013.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ↦ 𝐵) |
|
Theorem | nfmpt1 4097 |
Bound-variable hypothesis builder for the maps-to notation.
(Contributed by FL, 17-Feb-2008.)
|
⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵) |
|
Theorem | cbvmptf 4098* |
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 4099* |
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 4100* |
Rule to change the bound variable in a maps-to function, using implicit
substitution. (Contributed by Mario Carneiro, 19-Feb-2013.)
|
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶) |