Theorem List for Intuitionistic Logic Explorer - 2801-2900 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | spcedv 2801* |
Existential specialization, using implicit substitution, deduction
version. (Contributed by RP, 12-Aug-2020.)
|
⊢ (𝜑 → 𝑋 ∈ V) & ⊢ (𝜑 → 𝜒)
& ⊢ (𝑥 = 𝑋 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ∃𝑥𝜓) |
|
Theorem | spc2egv 2802* |
Existential specialization with 2 quantifiers, using implicit
substitution. (Contributed by NM, 3-Aug-1995.)
|
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝜓 → ∃𝑥∃𝑦𝜑)) |
|
Theorem | spc2gv 2803* |
Specialization with 2 quantifiers, using implicit substitution.
(Contributed by NM, 27-Apr-2004.)
|
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥∀𝑦𝜑 → 𝜓)) |
|
Theorem | spc3egv 2804* |
Existential specialization with 3 quantifiers, using implicit
substitution. (Contributed by NM, 12-May-2008.)
|
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝜓 → ∃𝑥∃𝑦∃𝑧𝜑)) |
|
Theorem | spc3gv 2805* |
Specialization with 3 quantifiers, using implicit substitution.
(Contributed by NM, 12-May-2008.)
|
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (∀𝑥∀𝑦∀𝑧𝜑 → 𝜓)) |
|
Theorem | spcv 2806* |
Rule of specialization, using implicit substitution. (Contributed by
NM, 22-Jun-1994.)
|
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) |
|
Theorem | spcev 2807* |
Existential specialization, using implicit substitution. (Contributed
by NM, 31-Dec-1993.) (Proof shortened by Eric Schmidt, 22-Dec-2006.)
|
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝜓 → ∃𝑥𝜑) |
|
Theorem | spc2ev 2808* |
Existential specialization, using implicit substitution. (Contributed
by NM, 3-Aug-1995.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝜓 → ∃𝑥∃𝑦𝜑) |
|
Theorem | rspct 2809* |
A closed version of rspc 2810. (Contributed by Andrew Salmon,
6-Jun-2011.)
|
⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))) |
|
Theorem | rspc 2810* |
Restricted specialization, using implicit substitution. (Contributed by
NM, 19-Apr-2005.) (Revised by Mario Carneiro, 11-Oct-2016.)
|
⊢ Ⅎ𝑥𝜓
& ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓)) |
|
Theorem | rspce 2811* |
Restricted existential specialization, using implicit substitution.
(Contributed by NM, 26-May-1998.) (Revised by Mario Carneiro,
11-Oct-2016.)
|
⊢ Ⅎ𝑥𝜓
& ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑) |
|
Theorem | rspcv 2812* |
Restricted specialization, using implicit substitution. (Contributed by
NM, 26-May-1998.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓)) |
|
Theorem | rspccv 2813* |
Restricted specialization, using implicit substitution. (Contributed by
NM, 2-Feb-2006.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐵 𝜑 → (𝐴 ∈ 𝐵 → 𝜓)) |
|
Theorem | rspcva 2814* |
Restricted specialization, using implicit substitution. (Contributed by
NM, 13-Sep-2005.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝜑) → 𝜓) |
|
Theorem | rspccva 2815* |
Restricted specialization, using implicit substitution. (Contributed by
NM, 26-Jul-2006.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((∀𝑥 ∈ 𝐵 𝜑 ∧ 𝐴 ∈ 𝐵) → 𝜓) |
|
Theorem | rspcev 2816* |
Restricted existential specialization, using implicit substitution.
(Contributed by NM, 26-May-1998.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑) |
|
Theorem | rspcimdv 2817* |
Restricted specialization, using implicit substitution. (Contributed
by Mario Carneiro, 4-Jan-2017.)
|
⊢ (𝜑 → 𝐴 ∈ 𝐵)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 → 𝜒)) |
|
Theorem | rspcimedv 2818* |
Restricted existential specialization, using implicit substitution.
(Contributed by Mario Carneiro, 4-Jan-2017.)
|
⊢ (𝜑 → 𝐴 ∈ 𝐵)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜒 → 𝜓)) ⇒ ⊢ (𝜑 → (𝜒 → ∃𝑥 ∈ 𝐵 𝜓)) |
|
Theorem | rspcdv 2819* |
Restricted specialization, using implicit substitution. (Contributed by
NM, 17-Feb-2007.) (Revised by Mario Carneiro, 4-Jan-2017.)
|
⊢ (𝜑 → 𝐴 ∈ 𝐵)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 → 𝜒)) |
|
Theorem | rspcedv 2820* |
Restricted existential specialization, using implicit substitution.
(Contributed by FL, 17-Apr-2007.) (Revised by Mario Carneiro,
4-Jan-2017.)
|
⊢ (𝜑 → 𝐴 ∈ 𝐵)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝜒 → ∃𝑥 ∈ 𝐵 𝜓)) |
|
Theorem | rspcdva 2821* |
Restricted specialization, using implicit substitution. (Contributed by
Thierry Arnoux, 21-Jun-2020.)
|
⊢ (𝑥 = 𝐶 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)
& ⊢ (𝜑 → 𝐶 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝜒) |
|
Theorem | rspcedvd 2822* |
Restricted existential specialization, using implicit substitution.
Variant of rspcedv 2820. (Contributed by AV, 27-Nov-2019.)
|
⊢ (𝜑 → 𝐴 ∈ 𝐵)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝜒) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓) |
|
Theorem | rspcime 2823* |
Prove a restricted existential. (Contributed by Rohan Ridenour,
3-Aug-2023.)
|
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝜓)
& ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓) |
|
Theorem | rspceaimv 2824* |
Restricted existential specialization of a universally quantified
implication. (Contributed by BJ, 24-Aug-2022.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐶 (𝜓 → 𝜒)) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 (𝜑 → 𝜒)) |
|
Theorem | rspcedeq1vd 2825* |
Restricted existential specialization, using implicit substitution.
Variant of rspcedvd 2822 for equations, in which the left hand side
depends on the quantified variable. (Contributed by AV,
24-Dec-2019.)
|
⊢ (𝜑 → 𝐴 ∈ 𝐵)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝐶 = 𝐷) |
|
Theorem | rspcedeq2vd 2826* |
Restricted existential specialization, using implicit substitution.
Variant of rspcedvd 2822 for equations, in which the right hand side
depends on the quantified variable. (Contributed by AV,
24-Dec-2019.)
|
⊢ (𝜑 → 𝐴 ∈ 𝐵)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝐶 = 𝐷) |
|
Theorem | rspc2 2827* |
2-variable restricted specialization, using implicit substitution.
(Contributed by NM, 9-Nov-2012.)
|
⊢ Ⅎ𝑥𝜒
& ⊢ Ⅎ𝑦𝜓
& ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓)) |
|
Theorem | rspc2gv 2828* |
Restricted specialization with two quantifiers, using implicit
substitution. (Contributed by BJ, 2-Dec-2021.)
|
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑊 𝜑 → 𝜓)) |
|
Theorem | rspc2v 2829* |
2-variable restricted specialization, using implicit substitution.
(Contributed by NM, 13-Sep-1999.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓)) |
|
Theorem | rspc2va 2830* |
2-variable restricted specialization, using implicit substitution.
(Contributed by NM, 18-Jun-2014.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓)) ⇒ ⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑) → 𝜓) |
|
Theorem | rspc2ev 2831* |
2-variable restricted existential specialization, using implicit
substitution. (Contributed by NM, 16-Oct-1999.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 𝜑) |
|
Theorem | rspc3v 2832* |
3-variable restricted specialization, using implicit substitution.
(Contributed by NM, 10-May-2005.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜃)) & ⊢ (𝑧 = 𝐶 → (𝜃 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑇 𝜑 → 𝜓)) |
|
Theorem | rspc3ev 2833* |
3-variable restricted existentional specialization, using implicit
substitution. (Contributed by NM, 25-Jul-2012.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜃)) & ⊢ (𝑧 = 𝐶 → (𝜃 ↔ 𝜓)) ⇒ ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ 𝜓) → ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑆 ∃𝑧 ∈ 𝑇 𝜑) |
|
Theorem | rspceeqv 2834* |
Restricted existential specialization in an equality, using implicit
substitution. (Contributed by BJ, 2-Sep-2022.)
|
⊢ (𝑥 = 𝐴 → 𝐶 = 𝐷) ⇒ ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐸 = 𝐷) → ∃𝑥 ∈ 𝐵 𝐸 = 𝐶) |
|
Theorem | eqvinc 2835* |
A variable introduction law for class equality. (Contributed by NM,
14-Apr-1995.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 = 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 = 𝐵)) |
|
Theorem | eqvincg 2836* |
A variable introduction law for class equality, deduction version.
(Contributed by Thierry Arnoux, 2-Mar-2017.)
|
⊢ (𝐴 ∈ 𝑉 → (𝐴 = 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 = 𝐵))) |
|
Theorem | eqvincf 2837 |
A variable introduction law for class equality, using bound-variable
hypotheses instead of distinct variable conditions. (Contributed by NM,
14-Sep-2003.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝐵
& ⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 = 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 = 𝐵)) |
|
Theorem | alexeq 2838* |
Two ways to express substitution of 𝐴 for 𝑥 in 𝜑.
(Contributed by NM, 2-Mar-1995.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) |
|
Theorem | ceqex 2839* |
Equality implies equivalence with substitution. (Contributed by NM,
2-Mar-1995.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑))) |
|
Theorem | ceqsexg 2840* |
A representation of explicit substitution of a class for a variable,
inferred from an implicit substitution hypothesis. (Contributed by NM,
11-Oct-2004.)
|
⊢ Ⅎ𝑥𝜓
& ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓)) |
|
Theorem | ceqsexgv 2841* |
Elimination of an existential quantifier, using implicit substitution.
(Contributed by NM, 29-Dec-1996.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓)) |
|
Theorem | ceqsrexv 2842* |
Elimination of a restricted existential quantifier, using implicit
substitution. (Contributed by NM, 30-Apr-2004.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝐵 → (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓)) |
|
Theorem | ceqsrexbv 2843* |
Elimination of a restricted existential quantifier, using implicit
substitution. (Contributed by Mario Carneiro, 14-Mar-2014.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜑) ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)) |
|
Theorem | ceqsrex2v 2844* |
Elimination of a restricted existential quantifier, using implicit
substitution. (Contributed by NM, 29-Oct-2005.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ 𝜑) ↔ 𝜒)) |
|
Theorem | clel2 2845* |
An alternate definition of class membership when the class is a set.
(Contributed by NM, 18-Aug-1993.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ 𝐵 ↔ ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵)) |
|
Theorem | clel3g 2846* |
An alternate definition of class membership when the class is a set.
(Contributed by NM, 13-Aug-2005.)
|
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝐴 ∈ 𝑥))) |
|
Theorem | clel3 2847* |
An alternate definition of class membership when the class is a set.
(Contributed by NM, 18-Aug-1993.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝐴 ∈ 𝑥)) |
|
Theorem | clel4 2848* |
An alternate definition of class membership when the class is a set.
(Contributed by NM, 18-Aug-1993.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∈ 𝐵 ↔ ∀𝑥(𝑥 = 𝐵 → 𝐴 ∈ 𝑥)) |
|
Theorem | clel5 2849* |
Alternate definition of class membership: a class 𝑋 is an element of
another class 𝐴 iff there is an element of 𝐴 equal
to 𝑋.
(Contributed by AV, 13-Nov-2020.) (Revised by Steven Nguyen,
19-May-2023.)
|
⊢ (𝑋 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑋 = 𝑥) |
|
Theorem | pm13.183 2850* |
Compare theorem *13.183 in [WhiteheadRussell] p. 178. Only 𝐴 is
required to be a set. (Contributed by Andrew Salmon, 3-Jun-2011.)
|
⊢ (𝐴 ∈ 𝑉 → (𝐴 = 𝐵 ↔ ∀𝑧(𝑧 = 𝐴 ↔ 𝑧 = 𝐵))) |
|
Theorem | rr19.3v 2851* |
Restricted quantifier version of Theorem 19.3 of [Margaris] p. 89.
(Contributed by NM, 25-Oct-2012.)
|
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑) |
|
Theorem | rr19.28v 2852* |
Restricted quantifier version of Theorem 19.28 of [Margaris] p. 90.
(Contributed by NM, 29-Oct-2012.)
|
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∀𝑥 ∈ 𝐴 (𝜑 ∧ ∀𝑦 ∈ 𝐴 𝜓)) |
|
Theorem | elabgt 2853* |
Membership in a class abstraction, using implicit substitution. (Closed
theorem version of elabg 2858.) (Contributed by NM, 7-Nov-2005.) (Proof
shortened by Andrew Salmon, 8-Jun-2011.)
|
⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) |
|
Theorem | elabgf 2854 |
Membership in a class abstraction, using implicit substitution. Compare
Theorem 6.13 of [Quine] p. 44. This
version has bound-variable
hypotheses in place of distinct variable restrictions. (Contributed by
NM, 21-Sep-2003.) (Revised by Mario Carneiro, 12-Oct-2016.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝜓
& ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) |
|
Theorem | elabf 2855* |
Membership in a class abstraction, using implicit substitution.
(Contributed by NM, 1-Aug-1994.) (Revised by Mario Carneiro,
12-Oct-2016.)
|
⊢ Ⅎ𝑥𝜓
& ⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓) |
|
Theorem | elab 2856* |
Membership in a class abstraction, using implicit substitution. Compare
Theorem 6.13 of [Quine] p. 44.
(Contributed by NM, 1-Aug-1994.)
|
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓) |
|
Theorem | elabd 2857* |
Explicit demonstration the class {𝑥 ∣ 𝜓} is not empty by the
example 𝑋. (Contributed by RP, 12-Aug-2020.)
|
⊢ (𝜑 → 𝑋 ∈ V) & ⊢ (𝜑 → 𝜒)
& ⊢ (𝑥 = 𝑋 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ∃𝑥𝜓) |
|
Theorem | elabg 2858* |
Membership in a class abstraction, using implicit substitution. Compare
Theorem 6.13 of [Quine] p. 44.
(Contributed by NM, 14-Apr-1995.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) |
|
Theorem | elab2g 2859* |
Membership in a class abstraction, using implicit substitution.
(Contributed by NM, 13-Sep-1995.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝐵 = {𝑥 ∣ 𝜑} ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ 𝜓)) |
|
Theorem | elab2 2860* |
Membership in a class abstraction, using implicit substitution.
(Contributed by NM, 13-Sep-1995.)
|
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝐵 = {𝑥 ∣ 𝜑} ⇒ ⊢ (𝐴 ∈ 𝐵 ↔ 𝜓) |
|
Theorem | elab4g 2861* |
Membership in a class abstraction, using implicit substitution.
(Contributed by NM, 17-Oct-2012.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝐵 = {𝑥 ∣ 𝜑} ⇒ ⊢ (𝐴 ∈ 𝐵 ↔ (𝐴 ∈ V ∧ 𝜓)) |
|
Theorem | elab3gf 2862 |
Membership in a class abstraction, with a weaker antecedent than
elabgf 2854. (Contributed by NM, 6-Sep-2011.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝜓
& ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝜓 → 𝐴 ∈ 𝐵) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) |
|
Theorem | elab3g 2863* |
Membership in a class abstraction, with a weaker antecedent than
elabg 2858. (Contributed by NM, 29-Aug-2006.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝜓 → 𝐴 ∈ 𝐵) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) |
|
Theorem | elab3 2864* |
Membership in a class abstraction using implicit substitution.
(Contributed by NM, 10-Nov-2000.)
|
⊢ (𝜓 → 𝐴 ∈ V) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓) |
|
Theorem | elrabi 2865* |
Implication for the membership in a restricted class abstraction.
(Contributed by Alexander van der Vekens, 31-Dec-2017.)
|
⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉) |
|
Theorem | elrabf 2866 |
Membership in a restricted class abstraction, using implicit
substitution. This version has bound-variable hypotheses in place of
distinct variable restrictions. (Contributed by NM, 21-Sep-2003.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝐵
& ⊢ Ⅎ𝑥𝜓
& ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)) |
|
Theorem | elrab3t 2867* |
Membership in a restricted class abstraction, using implicit
substitution. (Closed theorem version of elrab3 2869.) (Contributed by
Thierry Arnoux, 31-Aug-2017.)
|
⊢ ((∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝐵) → (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ 𝜓)) |
|
Theorem | elrab 2868* |
Membership in a restricted class abstraction, using implicit
substitution. (Contributed by NM, 21-May-1999.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)) |
|
Theorem | elrab3 2869* |
Membership in a restricted class abstraction, using implicit
substitution. (Contributed by NM, 5-Oct-2006.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ 𝜓)) |
|
Theorem | elrabd 2870* |
Membership in a restricted class abstraction, using implicit
substitution. Deduction version of elrab 2868. (Contributed by Glauco
Siliprandi, 23-Oct-2021.)
|
⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝐴 ∈ 𝐵)
& ⊢ (𝜑 → 𝜒) ⇒ ⊢ (𝜑 → 𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜓}) |
|
Theorem | elrab2 2871* |
Membership in a class abstraction, using implicit substitution.
(Contributed by NM, 2-Nov-2006.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝐶 = {𝑥 ∈ 𝐵 ∣ 𝜑} ⇒ ⊢ (𝐴 ∈ 𝐶 ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)) |
|
Theorem | ralab 2872* |
Universal quantification over a class abstraction. (Contributed by Jeff
Madsen, 10-Jun-2010.)
|
⊢ (𝑦 = 𝑥 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ∀𝑥(𝜓 → 𝜒)) |
|
Theorem | ralrab 2873* |
Universal quantification over a restricted class abstraction.
(Contributed by Jeff Madsen, 10-Jun-2010.)
|
⊢ (𝑦 = 𝑥 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑}𝜒 ↔ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒)) |
|
Theorem | rexab 2874* |
Existential quantification over a class abstraction. (Contributed by
Mario Carneiro, 23-Jan-2014.) (Revised by Mario Carneiro,
3-Sep-2015.)
|
⊢ (𝑦 = 𝑥 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ∃𝑥(𝜓 ∧ 𝜒)) |
|
Theorem | rexrab 2875* |
Existential quantification over a class abstraction. (Contributed by
Jeff Madsen, 17-Jun-2011.) (Revised by Mario Carneiro, 3-Sep-2015.)
|
⊢ (𝑦 = 𝑥 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑}𝜒 ↔ ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜒)) |
|
Theorem | ralab2 2876* |
Universal quantification over a class abstraction. (Contributed by
Mario Carneiro, 3-Sep-2015.)
|
⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∀𝑥 ∈ {𝑦 ∣ 𝜑}𝜓 ↔ ∀𝑦(𝜑 → 𝜒)) |
|
Theorem | ralrab2 2877* |
Universal quantification over a restricted class abstraction.
(Contributed by Mario Carneiro, 3-Sep-2015.)
|
⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∀𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑}𝜓 ↔ ∀𝑦 ∈ 𝐴 (𝜑 → 𝜒)) |
|
Theorem | rexab2 2878* |
Existential quantification over a class abstraction. (Contributed by
Mario Carneiro, 3-Sep-2015.)
|
⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∃𝑥 ∈ {𝑦 ∣ 𝜑}𝜓 ↔ ∃𝑦(𝜑 ∧ 𝜒)) |
|
Theorem | rexrab2 2879* |
Existential quantification over a class abstraction. (Contributed by
Mario Carneiro, 3-Sep-2015.)
|
⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∃𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑}𝜓 ↔ ∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝜒)) |
|
Theorem | abidnf 2880* |
Identity used to create closed-form versions of bound-variable
hypothesis builders for class expressions. (Contributed by NM,
10-Nov-2005.) (Proof shortened by Mario Carneiro, 12-Oct-2016.)
|
⊢ (Ⅎ𝑥𝐴 → {𝑧 ∣ ∀𝑥 𝑧 ∈ 𝐴} = 𝐴) |
|
Theorem | dedhb 2881* |
A deduction theorem for converting the inference ⊢ Ⅎ𝑥𝐴 =>
⊢
𝜑 into a closed
theorem. Use nfa1 1521 and nfab 2304 to eliminate the
hypothesis of the substitution instance 𝜓 of the inference. For
converting the inference form into a deduction form, abidnf 2880 is useful.
(Contributed by NM, 8-Dec-2006.)
|
⊢ (𝐴 = {𝑧 ∣ ∀𝑥 𝑧 ∈ 𝐴} → (𝜑 ↔ 𝜓)) & ⊢ 𝜓 ⇒ ⊢ (Ⅎ𝑥𝐴 → 𝜑) |
|
Theorem | eqeu 2882* |
A condition which implies existential uniqueness. (Contributed by Jeff
Hankins, 8-Sep-2009.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓 ∧ ∀𝑥(𝜑 → 𝑥 = 𝐴)) → ∃!𝑥𝜑) |
|
Theorem | eueq 2883* |
Equality has existential uniqueness. (Contributed by NM,
25-Nov-1994.)
|
⊢ (𝐴 ∈ V ↔ ∃!𝑥 𝑥 = 𝐴) |
|
Theorem | eueq1 2884* |
Equality has existential uniqueness. (Contributed by NM,
5-Apr-1995.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ ∃!𝑥 𝑥 = 𝐴 |
|
Theorem | eueq2dc 2885* |
Equality has existential uniqueness (split into 2 cases). (Contributed
by NM, 5-Apr-1995.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (DECID 𝜑 → ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ 𝜑 ∧ 𝑥 = 𝐵))) |
|
Theorem | eueq3dc 2886* |
Equality has existential uniqueness (split into 3 cases). (Contributed
by NM, 5-Apr-1995.) (Proof shortened by Mario Carneiro,
28-Sep-2015.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ ¬ (𝜑 ∧ 𝜓) ⇒ ⊢ (DECID 𝜑 → (DECID
𝜓 → ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)))) |
|
Theorem | moeq 2887* |
There is at most one set equal to a class. (Contributed by NM,
8-Mar-1995.)
|
⊢ ∃*𝑥 𝑥 = 𝐴 |
|
Theorem | moeq3dc 2888* |
"At most one" property of equality (split into 3 cases).
(Contributed
by Jim Kingdon, 7-Jul-2018.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ ¬ (𝜑 ∧ 𝜓) ⇒ ⊢ (DECID 𝜑 → (DECID
𝜓 → ∃*𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)))) |
|
Theorem | mosubt 2889* |
"At most one" remains true after substitution. (Contributed by Jim
Kingdon, 18-Jan-2019.)
|
⊢ (∀𝑦∃*𝑥𝜑 → ∃*𝑥∃𝑦(𝑦 = 𝐴 ∧ 𝜑)) |
|
Theorem | mosub 2890* |
"At most one" remains true after substitution. (Contributed by NM,
9-Mar-1995.)
|
⊢ ∃*𝑥𝜑 ⇒ ⊢ ∃*𝑥∃𝑦(𝑦 = 𝐴 ∧ 𝜑) |
|
Theorem | mo2icl 2891* |
Theorem for inferring "at most one." (Contributed by NM,
17-Oct-1996.)
|
⊢ (∀𝑥(𝜑 → 𝑥 = 𝐴) → ∃*𝑥𝜑) |
|
Theorem | mob2 2892* |
Consequence of "at most one." (Contributed by NM, 2-Jan-2015.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐵 ∧ ∃*𝑥𝜑 ∧ 𝜑) → (𝑥 = 𝐴 ↔ 𝜓)) |
|
Theorem | moi2 2893* |
Consequence of "at most one." (Contributed by NM, 29-Jun-2008.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (((𝐴 ∈ 𝐵 ∧ ∃*𝑥𝜑) ∧ (𝜑 ∧ 𝜓)) → 𝑥 = 𝐴) |
|
Theorem | mob 2894* |
Equality implied by "at most one." (Contributed by NM, 18-Feb-2006.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) ⇒ ⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ∧ ∃*𝑥𝜑 ∧ 𝜓) → (𝐴 = 𝐵 ↔ 𝜒)) |
|
Theorem | moi 2895* |
Equality implied by "at most one." (Contributed by NM, 18-Feb-2006.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) ⇒ ⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ∧ ∃*𝑥𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝐴 = 𝐵) |
|
Theorem | morex 2896* |
Derive membership from uniqueness. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
⊢ 𝐵 ∈ V & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥𝜑) → (𝜓 → 𝐵 ∈ 𝐴)) |
|
Theorem | euxfr2dc 2897* |
Transfer existential uniqueness from a variable 𝑥 to another
variable 𝑦 contained in expression 𝐴.
(Contributed by NM,
14-Nov-2004.)
|
⊢ 𝐴 ∈ V & ⊢ ∃*𝑦 𝑥 = 𝐴 ⇒ ⊢ (DECID
∃𝑦∃𝑥(𝑥 = 𝐴 ∧ 𝜑) → (∃!𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝜑) ↔ ∃!𝑦𝜑)) |
|
Theorem | euxfrdc 2898* |
Transfer existential uniqueness from a variable 𝑥 to another
variable 𝑦 contained in expression 𝐴.
(Contributed by NM,
14-Nov-2004.)
|
⊢ 𝐴 ∈ V & ⊢ ∃!𝑦 𝑥 = 𝐴
& ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (DECID
∃𝑦∃𝑥(𝑥 = 𝐴 ∧ 𝜓) → (∃!𝑥𝜑 ↔ ∃!𝑦𝜓)) |
|
Theorem | euind 2899* |
Existential uniqueness via an indirect equality. (Contributed by NM,
11-Oct-2010.)
|
⊢ 𝐵 ∈ V & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) ⇒ ⊢ ((∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝐴 = 𝐵) ∧ ∃𝑥𝜑) → ∃!𝑧∀𝑥(𝜑 → 𝑧 = 𝐴)) |
|
Theorem | reu2 2900* |
A way to express restricted uniqueness. (Contributed by NM,
22-Nov-1994.)
|
⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))) |