Theorem List for Intuitionistic Logic Explorer - 2601-2700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | gencbvex2 2601* |
Restatement of gencbvex 2600 with weaker hypotheses. (Contributed by Jeff
Hankins, 6-Dec-2006.)
|
⊢ 𝐴 ∈ V & ⊢ (𝐴 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝐴 = 𝑦 → (𝜒 ↔ 𝜃)) & ⊢ (𝜃 → ∃𝑥(𝜒 ∧ 𝐴 = 𝑦)) ⇒ ⊢ (∃𝑥(𝜒 ∧ 𝜑) ↔ ∃𝑦(𝜃 ∧ 𝜓)) |
|
Theorem | gencbval 2602* |
Change of bound variable using implicit substitution. (Contributed by
NM, 17-May-1996.) (Proof rewritten by Jim Kingdon, 20-Jun-2018.)
|
⊢ 𝐴 ∈ V & ⊢ (𝐴 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝐴 = 𝑦 → (𝜒 ↔ 𝜃)) & ⊢ (𝜃 ↔ ∃𝑥(𝜒 ∧ 𝐴 = 𝑦)) ⇒ ⊢ (∀𝑥(𝜒 → 𝜑) ↔ ∀𝑦(𝜃 → 𝜓)) |
|
Theorem | sbhypf 2603* |
Introduce an explicit substitution into an implicit substitution
hypothesis. See also csbhypf . (Contributed by Raph Levien,
10-Apr-2004.)
|
⊢ Ⅎ𝑥𝜓
& ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ 𝜓)) |
|
Theorem | vtoclgft 2604 |
Closed theorem form of vtoclgf 2612. (Contributed by NM, 17-Feb-2013.)
(Revised by Mario Carneiro, 12-Oct-2016.)
|
⊢ (((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑) ∧ 𝐴 ∈ 𝑉) → 𝜓) |
|
Theorem | vtocldf 2605 |
Implicit substitution of a class for a setvar variable. (Contributed
by Mario Carneiro, 15-Oct-2016.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝜓)
& ⊢ Ⅎ𝑥𝜑
& ⊢ (𝜑 → Ⅎ𝑥𝐴)
& ⊢ (𝜑 → Ⅎ𝑥𝜒) ⇒ ⊢ (𝜑 → 𝜒) |
|
Theorem | vtocld 2606* |
Implicit substitution of a class for a setvar variable. (Contributed by
Mario Carneiro, 15-Oct-2016.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → 𝜒) |
|
Theorem | vtoclf 2607* |
Implicit substitution of a class for a setvar variable. This is a
generalization of chvar 1640. (Contributed by NM, 30-Aug-1993.)
|
⊢ Ⅎ𝑥𝜓
& ⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 |
|
Theorem | vtocl 2608* |
Implicit substitution of a class for a setvar variable. (Contributed by
NM, 30-Aug-1993.)
|
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 |
|
Theorem | vtocl2 2609* |
Implicit substitution of classes for setvar variables. (Contributed by
NM, 26-Jul-1995.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 |
|
Theorem | vtocl3 2610* |
Implicit substitution of classes for setvar variables. (Contributed by
NM, 3-Jun-1995.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 |
|
Theorem | vtoclb 2611* |
Implicit substitution of a class for a setvar variable. (Contributed by
NM, 23-Dec-1993.)
|
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃)) & ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (𝜒 ↔ 𝜃) |
|
Theorem | vtoclgf 2612 |
Implicit substitution of a class for a setvar variable, with
bound-variable hypotheses in place of distinct variable restrictions.
(Contributed by NM, 21-Sep-2003.) (Proof shortened by Mario Carneiro,
10-Oct-2016.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝜓
& ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝜓) |
|
Theorem | vtoclg 2613* |
Implicit substitution of a class expression for a setvar variable.
(Contributed by NM, 17-Apr-1995.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝜓) |
|
Theorem | vtoclbg 2614* |
Implicit substitution of a class for a setvar variable. (Contributed by
NM, 29-Apr-1994.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃)) & ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃)) |
|
Theorem | vtocl2gf 2615 |
Implicit substitution of a class for a setvar variable. (Contributed by
NM, 25-Apr-1995.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑦𝐴
& ⊢ Ⅎ𝑦𝐵
& ⊢ Ⅎ𝑥𝜓
& ⊢ Ⅎ𝑦𝜒
& ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ 𝜑 ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝜒) |
|
Theorem | vtocl3gf 2616 |
Implicit substitution of a class for a setvar variable. (Contributed by
NM, 10-Aug-2013.) (Revised by Mario Carneiro, 10-Oct-2016.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑦𝐴
& ⊢ Ⅎ𝑧𝐴
& ⊢ Ⅎ𝑦𝐵
& ⊢ Ⅎ𝑧𝐵
& ⊢ Ⅎ𝑧𝐶
& ⊢ Ⅎ𝑥𝜓
& ⊢ Ⅎ𝑦𝜒
& ⊢ Ⅎ𝑧𝜃
& ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ 𝜑 ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝜃) |
|
Theorem | vtocl2g 2617* |
Implicit substitution of 2 classes for 2 setvar variables. (Contributed
by NM, 25-Apr-1995.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ 𝜑 ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝜒) |
|
Theorem | vtoclgaf 2618* |
Implicit substitution of a class for a setvar variable. (Contributed by
NM, 17-Feb-2006.) (Revised by Mario Carneiro, 10-Oct-2016.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝜓
& ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 ∈ 𝐵 → 𝜑) ⇒ ⊢ (𝐴 ∈ 𝐵 → 𝜓) |
|
Theorem | vtoclga 2619* |
Implicit substitution of a class for a setvar variable. (Contributed by
NM, 20-Aug-1995.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 ∈ 𝐵 → 𝜑) ⇒ ⊢ (𝐴 ∈ 𝐵 → 𝜓) |
|
Theorem | vtocl2gaf 2620* |
Implicit substitution of 2 classes for 2 setvar variables. (Contributed
by NM, 10-Aug-2013.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑦𝐴
& ⊢ Ⅎ𝑦𝐵
& ⊢ Ⅎ𝑥𝜓
& ⊢ Ⅎ𝑦𝜒
& ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → 𝜑) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝜒) |
|
Theorem | vtocl2ga 2621* |
Implicit substitution of 2 classes for 2 setvar variables. (Contributed
by NM, 20-Aug-1995.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → 𝜑) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝜒) |
|
Theorem | vtocl3gaf 2622* |
Implicit substitution of 3 classes for 3 setvar variables. (Contributed
by NM, 10-Aug-2013.) (Revised by Mario Carneiro, 11-Oct-2016.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑦𝐴
& ⊢ Ⅎ𝑧𝐴
& ⊢ Ⅎ𝑦𝐵
& ⊢ Ⅎ𝑧𝐵
& ⊢ Ⅎ𝑧𝐶
& ⊢ Ⅎ𝑥𝜓
& ⊢ Ⅎ𝑦𝜒
& ⊢ Ⅎ𝑧𝜃
& ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇) → 𝜑) ⇒ ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → 𝜃) |
|
Theorem | vtocl3ga 2623* |
Implicit substitution of 3 classes for 3 setvar variables. (Contributed
by NM, 20-Aug-1995.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑆) → 𝜑) ⇒ ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝑅 ∧ 𝐶 ∈ 𝑆) → 𝜃) |
|
Theorem | vtocleg 2624* |
Implicit substitution of a class for a setvar variable. (Contributed by
NM, 10-Jan-2004.)
|
⊢ (𝑥 = 𝐴 → 𝜑) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝜑) |
|
Theorem | vtoclegft 2625* |
Implicit substitution of a class for a setvar variable. (Closed theorem
version of vtoclef 2626.) (Contributed by NM, 7-Nov-2005.) (Revised
by
Mario Carneiro, 11-Oct-2016.)
|
⊢ ((𝐴 ∈ 𝐵 ∧ Ⅎ𝑥𝜑 ∧ ∀𝑥(𝑥 = 𝐴 → 𝜑)) → 𝜑) |
|
Theorem | vtoclef 2626* |
Implicit substitution of a class for a setvar variable. (Contributed by
NM, 18-Aug-1993.)
|
⊢ Ⅎ𝑥𝜑
& ⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → 𝜑) ⇒ ⊢ 𝜑 |
|
Theorem | vtocle 2627* |
Implicit substitution of a class for a setvar variable. (Contributed by
NM, 9-Sep-1993.)
|
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → 𝜑) ⇒ ⊢ 𝜑 |
|
Theorem | vtoclri 2628* |
Implicit substitution of a class for a setvar variable. (Contributed by
NM, 21-Nov-1994.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ ∀𝑥 ∈ 𝐵 𝜑 ⇒ ⊢ (𝐴 ∈ 𝐵 → 𝜓) |
|
Theorem | spcimgft 2629 |
A closed version of spcimgf 2633. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
⊢ Ⅎ𝑥𝜓
& ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (∀𝑥(𝑥 = 𝐴 → (𝜑 → 𝜓)) → (𝐴 ∈ 𝐵 → (∀𝑥𝜑 → 𝜓))) |
|
Theorem | spcgft 2630 |
A closed version of spcgf 2635. (Contributed by Andrew Salmon,
6-Jun-2011.) (Revised by Mario Carneiro, 4-Jan-2017.)
|
⊢ Ⅎ𝑥𝜓
& ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝐴 ∈ 𝐵 → (∀𝑥𝜑 → 𝜓))) |
|
Theorem | spcimegft 2631 |
A closed version of spcimegf 2634. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
⊢ Ⅎ𝑥𝜓
& ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (∀𝑥(𝑥 = 𝐴 → (𝜓 → 𝜑)) → (𝐴 ∈ 𝐵 → (𝜓 → ∃𝑥𝜑))) |
|
Theorem | spcegft 2632 |
A closed version of spcegf 2636. (Contributed by Jim Kingdon,
22-Jun-2018.)
|
⊢ Ⅎ𝑥𝜓
& ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝐴 ∈ 𝐵 → (𝜓 → ∃𝑥𝜑))) |
|
Theorem | spcimgf 2633 |
Rule of specialization, using implicit substitution. Compare Theorem
7.3 of [Quine] p. 44. (Contributed by
Mario Carneiro, 4-Jan-2017.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝜓
& ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥𝜑 → 𝜓)) |
|
Theorem | spcimegf 2634 |
Existential specialization, using implicit substitution. (Contributed
by Mario Carneiro, 4-Jan-2017.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝜓
& ⊢ (𝑥 = 𝐴 → (𝜓 → 𝜑)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑)) |
|
Theorem | spcgf 2635 |
Rule of specialization, using implicit substitution. Compare Theorem
7.3 of [Quine] p. 44. (Contributed by NM,
2-Feb-1997.) (Revised by
Andrew Salmon, 12-Aug-2011.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝜓
& ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥𝜑 → 𝜓)) |
|
Theorem | spcegf 2636 |
Existential specialization, using implicit substitution. (Contributed
by NM, 2-Feb-1997.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝜓
& ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑)) |
|
Theorem | spcimdv 2637* |
Restricted specialization, using implicit substitution. (Contributed
by Mario Carneiro, 4-Jan-2017.)
|
⊢ (𝜑 → 𝐴 ∈ 𝐵)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 → 𝜒)) |
|
Theorem | spcdv 2638* |
Rule of specialization, using implicit substitution. Analogous to
rspcdv 2659. (Contributed by David Moews, 1-May-2017.)
|
⊢ (𝜑 → 𝐴 ∈ 𝐵)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 → 𝜒)) |
|
Theorem | spcimedv 2639* |
Restricted existential specialization, using implicit substitution.
(Contributed by Mario Carneiro, 4-Jan-2017.)
|
⊢ (𝜑 → 𝐴 ∈ 𝐵)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜒 → 𝜓)) ⇒ ⊢ (𝜑 → (𝜒 → ∃𝑥𝜓)) |
|
Theorem | spcgv 2640* |
Rule of specialization, using implicit substitution. Compare Theorem
7.3 of [Quine] p. 44. (Contributed by NM,
22-Jun-1994.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥𝜑 → 𝜓)) |
|
Theorem | spcegv 2641* |
Existential specialization, using implicit substitution. (Contributed
by NM, 14-Aug-1994.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑)) |
|
Theorem | spc2egv 2642* |
Existential specialization with 2 quantifiers, using implicit
substitution. (Contributed by NM, 3-Aug-1995.)
|
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝜓 → ∃𝑥∃𝑦𝜑)) |
|
Theorem | spc2gv 2643* |
Specialization with 2 quantifiers, using implicit substitution.
(Contributed by NM, 27-Apr-2004.)
|
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥∀𝑦𝜑 → 𝜓)) |
|
Theorem | spc3egv 2644* |
Existential specialization with 3 quantifiers, using implicit
substitution. (Contributed by NM, 12-May-2008.)
|
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝜓 → ∃𝑥∃𝑦∃𝑧𝜑)) |
|
Theorem | spc3gv 2645* |
Specialization with 3 quantifiers, using implicit substitution.
(Contributed by NM, 12-May-2008.)
|
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (∀𝑥∀𝑦∀𝑧𝜑 → 𝜓)) |
|
Theorem | spcv 2646* |
Rule of specialization, using implicit substitution. (Contributed by
NM, 22-Jun-1994.)
|
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) |
|
Theorem | spcev 2647* |
Existential specialization, using implicit substitution. (Contributed
by NM, 31-Dec-1993.) (Proof shortened by Eric Schmidt, 22-Dec-2006.)
|
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝜓 → ∃𝑥𝜑) |
|
Theorem | spc2ev 2648* |
Existential specialization, using implicit substitution. (Contributed
by NM, 3-Aug-1995.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝜓 → ∃𝑥∃𝑦𝜑) |
|
Theorem | rspct 2649* |
A closed version of rspc 2650. (Contributed by Andrew Salmon,
6-Jun-2011.)
|
⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))) |
|
Theorem | rspc 2650* |
Restricted specialization, using implicit substitution. (Contributed by
NM, 19-Apr-2005.) (Revised by Mario Carneiro, 11-Oct-2016.)
|
⊢ Ⅎ𝑥𝜓
& ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓)) |
|
Theorem | rspce 2651* |
Restricted existential specialization, using implicit substitution.
(Contributed by NM, 26-May-1998.) (Revised by Mario Carneiro,
11-Oct-2016.)
|
⊢ Ⅎ𝑥𝜓
& ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑) |
|
Theorem | rspcv 2652* |
Restricted specialization, using implicit substitution. (Contributed by
NM, 26-May-1998.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓)) |
|
Theorem | rspccv 2653* |
Restricted specialization, using implicit substitution. (Contributed by
NM, 2-Feb-2006.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐵 𝜑 → (𝐴 ∈ 𝐵 → 𝜓)) |
|
Theorem | rspcva 2654* |
Restricted specialization, using implicit substitution. (Contributed by
NM, 13-Sep-2005.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝜑) → 𝜓) |
|
Theorem | rspccva 2655* |
Restricted specialization, using implicit substitution. (Contributed by
NM, 26-Jul-2006.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((∀𝑥 ∈ 𝐵 𝜑 ∧ 𝐴 ∈ 𝐵) → 𝜓) |
|
Theorem | rspcev 2656* |
Restricted existential specialization, using implicit substitution.
(Contributed by NM, 26-May-1998.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑) |
|
Theorem | rspcimdv 2657* |
Restricted specialization, using implicit substitution. (Contributed
by Mario Carneiro, 4-Jan-2017.)
|
⊢ (𝜑 → 𝐴 ∈ 𝐵)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 → 𝜒)) |
|
Theorem | rspcimedv 2658* |
Restricted existential specialization, using implicit substitution.
(Contributed by Mario Carneiro, 4-Jan-2017.)
|
⊢ (𝜑 → 𝐴 ∈ 𝐵)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜒 → 𝜓)) ⇒ ⊢ (𝜑 → (𝜒 → ∃𝑥 ∈ 𝐵 𝜓)) |
|
Theorem | rspcdv 2659* |
Restricted specialization, using implicit substitution. (Contributed by
NM, 17-Feb-2007.) (Revised by Mario Carneiro, 4-Jan-2017.)
|
⊢ (𝜑 → 𝐴 ∈ 𝐵)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 → 𝜒)) |
|
Theorem | rspcedv 2660* |
Restricted existential specialization, using implicit substitution.
(Contributed by FL, 17-Apr-2007.) (Revised by Mario Carneiro,
4-Jan-2017.)
|
⊢ (𝜑 → 𝐴 ∈ 𝐵)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝜒 → ∃𝑥 ∈ 𝐵 𝜓)) |
|
Theorem | rspc2 2661* |
2-variable restricted specialization, using implicit substitution.
(Contributed by NM, 9-Nov-2012.)
|
⊢ Ⅎ𝑥𝜒
& ⊢ Ⅎ𝑦𝜓
& ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓)) |
|
Theorem | rspc2v 2662* |
2-variable restricted specialization, using implicit substitution.
(Contributed by NM, 13-Sep-1999.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓)) |
|
Theorem | rspc2va 2663* |
2-variable restricted specialization, using implicit substitution.
(Contributed by NM, 18-Jun-2014.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓)) ⇒ ⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑) → 𝜓) |
|
Theorem | rspc2ev 2664* |
2-variable restricted existential specialization, using implicit
substitution. (Contributed by NM, 16-Oct-1999.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 𝜑) |
|
Theorem | rspc3v 2665* |
3-variable restricted specialization, using implicit substitution.
(Contributed by NM, 10-May-2005.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜃)) & ⊢ (𝑧 = 𝐶 → (𝜃 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑇 𝜑 → 𝜓)) |
|
Theorem | rspc3ev 2666* |
3-variable restricted existentional specialization, using implicit
substitution. (Contributed by NM, 25-Jul-2012.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜃)) & ⊢ (𝑧 = 𝐶 → (𝜃 ↔ 𝜓)) ⇒ ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ 𝜓) → ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑆 ∃𝑧 ∈ 𝑇 𝜑) |
|
Theorem | eqvinc 2667* |
A variable introduction law for class equality. (Contributed by NM,
14-Apr-1995.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 = 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 = 𝐵)) |
|
Theorem | eqvincg 2668* |
A variable introduction law for class equality, deduction version.
(Contributed by Thierry Arnoux, 2-Mar-2017.)
|
⊢ (𝐴 ∈ 𝑉 → (𝐴 = 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 = 𝐵))) |
|
Theorem | eqvincf 2669 |
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 2670* |
Two ways to express substitution of 𝐴 for 𝑥 in 𝜑.
(Contributed by NM, 2-Mar-1995.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) |
|
Theorem | ceqex 2671* |
Equality implies equivalence with substitution. (Contributed by NM,
2-Mar-1995.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑))) |
|
Theorem | ceqsexg 2672* |
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 2673* |
Elimination of an existential quantifier, using implicit substitution.
(Contributed by NM, 29-Dec-1996.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓)) |
|
Theorem | ceqsrexv 2674* |
Elimination of a restricted existential quantifier, using implicit
substitution. (Contributed by NM, 30-Apr-2004.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝐵 → (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓)) |
|
Theorem | ceqsrexbv 2675* |
Elimination of a restricted existential quantifier, using implicit
substitution. (Contributed by Mario Carneiro, 14-Mar-2014.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜑) ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)) |
|
Theorem | ceqsrex2v 2676* |
Elimination of a restricted existential quantifier, using implicit
substitution. (Contributed by NM, 29-Oct-2005.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ 𝜑) ↔ 𝜒)) |
|
Theorem | clel2 2677* |
An alternate definition of class membership when the class is a set.
(Contributed by NM, 18-Aug-1993.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ 𝐵 ↔ ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵)) |
|
Theorem | clel3g 2678* |
An alternate definition of class membership when the class is a set.
(Contributed by NM, 13-Aug-2005.)
|
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝐴 ∈ 𝑥))) |
|
Theorem | clel3 2679* |
An alternate definition of class membership when the class is a set.
(Contributed by NM, 18-Aug-1993.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝐴 ∈ 𝑥)) |
|
Theorem | clel4 2680* |
An alternate definition of class membership when the class is a set.
(Contributed by NM, 18-Aug-1993.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∈ 𝐵 ↔ ∀𝑥(𝑥 = 𝐵 → 𝐴 ∈ 𝑥)) |
|
Theorem | pm13.183 2681* |
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 2682* |
Restricted quantifier version of Theorem 19.3 of [Margaris] p. 89.
(Contributed by NM, 25-Oct-2012.)
|
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑) |
|
Theorem | rr19.28v 2683* |
Restricted quantifier version of Theorem 19.28 of [Margaris] p. 90.
(Contributed by NM, 29-Oct-2012.)
|
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∀𝑥 ∈ 𝐴 (𝜑 ∧ ∀𝑦 ∈ 𝐴 𝜓)) |
|
Theorem | elabgt 2684* |
Membership in a class abstraction, using implicit substitution. (Closed
theorem version of elabg 2688.) (Contributed by NM, 7-Nov-2005.) (Proof
shortened by Andrew Salmon, 8-Jun-2011.)
|
⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) |
|
Theorem | elabgf 2685 |
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 2686* |
Membership in a class abstraction, using implicit substitution.
(Contributed by NM, 1-Aug-1994.) (Revised by Mario Carneiro,
12-Oct-2016.)
|
⊢ Ⅎ𝑥𝜓
& ⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓) |
|
Theorem | elab 2687* |
Membership in a class abstraction, using implicit substitution. Compare
Theorem 6.13 of [Quine] p. 44.
(Contributed by NM, 1-Aug-1994.)
|
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓) |
|
Theorem | elabg 2688* |
Membership in a class abstraction, using implicit substitution. Compare
Theorem 6.13 of [Quine] p. 44.
(Contributed by NM, 14-Apr-1995.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) |
|
Theorem | elab2g 2689* |
Membership in a class abstraction, using implicit substitution.
(Contributed by NM, 13-Sep-1995.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝐵 = {𝑥 ∣ 𝜑} ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ 𝜓)) |
|
Theorem | elab2 2690* |
Membership in a class abstraction, using implicit substitution.
(Contributed by NM, 13-Sep-1995.)
|
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝐵 = {𝑥 ∣ 𝜑} ⇒ ⊢ (𝐴 ∈ 𝐵 ↔ 𝜓) |
|
Theorem | elab4g 2691* |
Membership in a class abstraction, using implicit substitution.
(Contributed by NM, 17-Oct-2012.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝐵 = {𝑥 ∣ 𝜑} ⇒ ⊢ (𝐴 ∈ 𝐵 ↔ (𝐴 ∈ V ∧ 𝜓)) |
|
Theorem | elab3gf 2692 |
Membership in a class abstraction, with a weaker antecedent than
elabgf 2685. (Contributed by NM, 6-Sep-2011.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝜓
& ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝜓 → 𝐴 ∈ 𝐵) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) |
|
Theorem | elab3g 2693* |
Membership in a class abstraction, with a weaker antecedent than
elabg 2688. (Contributed by NM, 29-Aug-2006.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝜓 → 𝐴 ∈ 𝐵) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) |
|
Theorem | elab3 2694* |
Membership in a class abstraction using implicit substitution.
(Contributed by NM, 10-Nov-2000.)
|
⊢ (𝜓 → 𝐴 ∈ V) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓) |
|
Theorem | elrabi 2695* |
Implication for the membership in a restricted class abstraction.
(Contributed by Alexander van der Vekens, 31-Dec-2017.)
|
⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉) |
|
Theorem | elrabf 2696 |
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 2697* |
Membership in a restricted class abstraction, using implicit
substitution. (Closed theorem version of elrab3 2699.) (Contributed by
Thierry Arnoux, 31-Aug-2017.)
|
⊢ ((∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝐵) → (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ 𝜓)) |
|
Theorem | elrab 2698* |
Membership in a restricted class abstraction, using implicit
substitution. (Contributed by NM, 21-May-1999.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)) |
|
Theorem | elrab3 2699* |
Membership in a restricted class abstraction, using implicit
substitution. (Contributed by NM, 5-Oct-2006.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ 𝜓)) |
|
Theorem | elrab2 2700* |
Membership in a class abstraction, using implicit substitution.
(Contributed by NM, 2-Nov-2006.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝐶 = {𝑥 ∈ 𝐵 ∣ 𝜑} ⇒ ⊢ (𝐴 ∈ 𝐶 ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)) |