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