Theorem List for Intuitionistic Logic Explorer - 2701-2800 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | rmov 2701 |
An at-most-one quantifier restricted to the universe is unrestricted.
(Contributed by Alexander van der Vekens, 17-Jun-2017.)
|
⊢ (∃*𝑥 ∈ V 𝜑 ↔ ∃*𝑥𝜑) |
|
Theorem | rabab 2702 |
A class abstraction restricted to the universe is unrestricted.
(Contributed by NM, 27-Dec-2004.) (Proof shortened by Andrew Salmon,
8-Jun-2011.)
|
⊢ {𝑥 ∈ V ∣ 𝜑} = {𝑥 ∣ 𝜑} |
|
Theorem | ralcom4 2703* |
Commutation of restricted and unrestricted universal quantifiers.
(Contributed by NM, 26-Mar-2004.) (Proof shortened by Andrew Salmon,
8-Jun-2011.)
|
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑦∀𝑥 ∈ 𝐴 𝜑) |
|
Theorem | rexcom4 2704* |
Commutation of restricted and unrestricted existential quantifiers.
(Contributed by NM, 12-Apr-2004.) (Proof shortened by Andrew Salmon,
8-Jun-2011.)
|
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑) |
|
Theorem | rexcom4a 2705* |
Specialized existential commutation lemma. (Contributed by Jeff Madsen,
1-Jun-2011.)
|
⊢ (∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑦 ∈ 𝐴 (𝜑 ∧ ∃𝑥𝜓)) |
|
Theorem | rexcom4b 2706* |
Specialized existential commutation lemma. (Contributed by Jeff Madsen,
1-Jun-2011.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ (∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ↔ ∃𝑦 ∈ 𝐴 𝜑) |
|
Theorem | ceqsalt 2707* |
Closed theorem version of ceqsalg 2709. (Contributed by NM, 28-Feb-2013.)
(Revised by Mario Carneiro, 10-Oct-2016.)
|
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) |
|
Theorem | ceqsralt 2708* |
Restricted quantifier version of ceqsalt 2707. (Contributed by NM,
28-Feb-2013.) (Revised by Mario Carneiro, 10-Oct-2016.)
|
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝐵) → (∀𝑥 ∈ 𝐵 (𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) |
|
Theorem | ceqsalg 2709* |
A representation of explicit substitution of a class for a variable,
inferred from an implicit substitution hypothesis. (Contributed by NM,
29-Oct-2003.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
|
⊢ Ⅎ𝑥𝜓
& ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) |
|
Theorem | ceqsal 2710* |
A representation of explicit substitution of a class for a variable,
inferred from an implicit substitution hypothesis. (Contributed by NM,
18-Aug-1993.)
|
⊢ Ⅎ𝑥𝜓
& ⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓) |
|
Theorem | ceqsalv 2711* |
A representation of explicit substitution of a class for a variable,
inferred from an implicit substitution hypothesis. (Contributed by NM,
18-Aug-1993.)
|
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓) |
|
Theorem | ceqsralv 2712* |
Restricted quantifier version of ceqsalv 2711. (Contributed by NM,
21-Jun-2013.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 (𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) |
|
Theorem | gencl 2713* |
Implicit substitution for class with embedded variable. (Contributed by
NM, 17-May-1996.)
|
⊢ (𝜃 ↔ ∃𝑥(𝜒 ∧ 𝐴 = 𝐵)) & ⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) & ⊢ (𝜒 → 𝜑) ⇒ ⊢ (𝜃 → 𝜓) |
|
Theorem | 2gencl 2714* |
Implicit substitution for class with embedded variable. (Contributed by
NM, 17-May-1996.)
|
⊢ (𝐶 ∈ 𝑆 ↔ ∃𝑥 ∈ 𝑅 𝐴 = 𝐶)
& ⊢ (𝐷 ∈ 𝑆 ↔ ∃𝑦 ∈ 𝑅 𝐵 = 𝐷)
& ⊢ (𝐴 = 𝐶 → (𝜑 ↔ 𝜓)) & ⊢ (𝐵 = 𝐷 → (𝜓 ↔ 𝜒)) & ⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) → 𝜑) ⇒ ⊢ ((𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆) → 𝜒) |
|
Theorem | 3gencl 2715* |
Implicit substitution for class with embedded variable. (Contributed by
NM, 17-May-1996.)
|
⊢ (𝐷 ∈ 𝑆 ↔ ∃𝑥 ∈ 𝑅 𝐴 = 𝐷)
& ⊢ (𝐹 ∈ 𝑆 ↔ ∃𝑦 ∈ 𝑅 𝐵 = 𝐹)
& ⊢ (𝐺 ∈ 𝑆 ↔ ∃𝑧 ∈ 𝑅 𝐶 = 𝐺)
& ⊢ (𝐴 = 𝐷 → (𝜑 ↔ 𝜓)) & ⊢ (𝐵 = 𝐹 → (𝜓 ↔ 𝜒)) & ⊢ (𝐶 = 𝐺 → (𝜒 ↔ 𝜃)) & ⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅) → 𝜑) ⇒ ⊢ ((𝐷 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆) → 𝜃) |
|
Theorem | cgsexg 2716* |
Implicit substitution inference for general classes. (Contributed by
NM, 26-Aug-2007.)
|
⊢ (𝑥 = 𝐴 → 𝜒)
& ⊢ (𝜒 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∃𝑥(𝜒 ∧ 𝜑) ↔ 𝜓)) |
|
Theorem | cgsex2g 2717* |
Implicit substitution inference for general classes. (Contributed by
NM, 26-Jul-1995.)
|
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝜒)
& ⊢ (𝜒 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑥∃𝑦(𝜒 ∧ 𝜑) ↔ 𝜓)) |
|
Theorem | cgsex4g 2718* |
An implicit substitution inference for 4 general classes. (Contributed
by NM, 5-Aug-1995.)
|
⊢ (((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) → 𝜒)
& ⊢ (𝜒 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆)) → (∃𝑥∃𝑦∃𝑧∃𝑤(𝜒 ∧ 𝜑) ↔ 𝜓)) |
|
Theorem | ceqsex 2719* |
Elimination of an existential quantifier, using implicit substitution.
(Contributed by NM, 2-Mar-1995.) (Revised by Mario Carneiro,
10-Oct-2016.)
|
⊢ Ⅎ𝑥𝜓
& ⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓) |
|
Theorem | ceqsexv 2720* |
Elimination of an existential quantifier, using implicit substitution.
(Contributed by NM, 2-Mar-1995.)
|
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓) |
|
Theorem | ceqsex2 2721* |
Elimination of two existential quantifiers, using implicit substitution.
(Contributed by Scott Fenton, 7-Jun-2006.)
|
⊢ Ⅎ𝑥𝜓
& ⊢ Ⅎ𝑦𝜒
& ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝜑) ↔ 𝜒) |
|
Theorem | ceqsex2v 2722* |
Elimination of two existential quantifiers, using implicit substitution.
(Contributed by Scott Fenton, 7-Jun-2006.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝜑) ↔ 𝜒) |
|
Theorem | ceqsex3v 2723* |
Elimination of three existential quantifiers, using implicit
substitution. (Contributed by NM, 16-Aug-2011.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃)) ⇒ ⊢ (∃𝑥∃𝑦∃𝑧((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ 𝜑) ↔ 𝜃) |
|
Theorem | ceqsex4v 2724* |
Elimination of four existential quantifiers, using implicit
substitution. (Contributed by NM, 23-Sep-2011.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ (𝑤 = 𝐷 → (𝜃 ↔ 𝜏)) ⇒ ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷) ∧ 𝜑) ↔ 𝜏) |
|
Theorem | ceqsex6v 2725* |
Elimination of six existential quantifiers, using implicit substitution.
(Contributed by NM, 21-Sep-2011.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V & ⊢ 𝐸 ∈ V & ⊢ 𝐹 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ (𝑤 = 𝐷 → (𝜃 ↔ 𝜏)) & ⊢ (𝑣 = 𝐸 → (𝜏 ↔ 𝜂)) & ⊢ (𝑢 = 𝐹 → (𝜂 ↔ 𝜁)) ⇒ ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ (𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹) ∧ 𝜑) ↔ 𝜁) |
|
Theorem | ceqsex8v 2726* |
Elimination of eight existential quantifiers, using implicit
substitution. (Contributed by NM, 23-Sep-2011.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V & ⊢ 𝐸 ∈ V & ⊢ 𝐹 ∈ V & ⊢ 𝐺 ∈ V & ⊢ 𝐻 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ (𝑤 = 𝐷 → (𝜃 ↔ 𝜏)) & ⊢ (𝑣 = 𝐸 → (𝜏 ↔ 𝜂)) & ⊢ (𝑢 = 𝐹 → (𝜂 ↔ 𝜁)) & ⊢ (𝑡 = 𝐺 → (𝜁 ↔ 𝜎)) & ⊢ (𝑠 = 𝐻 → (𝜎 ↔ 𝜌)) ⇒ ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤∃𝑣∃𝑢∃𝑡∃𝑠(((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) ∧ ((𝑣 = 𝐸 ∧ 𝑢 = 𝐹) ∧ (𝑡 = 𝐺 ∧ 𝑠 = 𝐻)) ∧ 𝜑) ↔ 𝜌) |
|
Theorem | gencbvex 2727* |
Change of bound variable using implicit substitution. (Contributed by
NM, 17-May-1996.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
|
⊢ 𝐴 ∈ V & ⊢ (𝐴 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝐴 = 𝑦 → (𝜒 ↔ 𝜃)) & ⊢ (𝜃 ↔ ∃𝑥(𝜒 ∧ 𝐴 = 𝑦)) ⇒ ⊢ (∃𝑥(𝜒 ∧ 𝜑) ↔ ∃𝑦(𝜃 ∧ 𝜓)) |
|
Theorem | gencbvex2 2728* |
Restatement of gencbvex 2727 with weaker hypotheses. (Contributed by Jeff
Hankins, 6-Dec-2006.)
|
⊢ 𝐴 ∈ V & ⊢ (𝐴 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝐴 = 𝑦 → (𝜒 ↔ 𝜃)) & ⊢ (𝜃 → ∃𝑥(𝜒 ∧ 𝐴 = 𝑦)) ⇒ ⊢ (∃𝑥(𝜒 ∧ 𝜑) ↔ ∃𝑦(𝜃 ∧ 𝜓)) |
|
Theorem | gencbval 2729* |
Change of bound variable using implicit substitution. (Contributed by
NM, 17-May-1996.) (Proof rewritten by Jim Kingdon, 20-Jun-2018.)
|
⊢ 𝐴 ∈ V & ⊢ (𝐴 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝐴 = 𝑦 → (𝜒 ↔ 𝜃)) & ⊢ (𝜃 ↔ ∃𝑥(𝜒 ∧ 𝐴 = 𝑦)) ⇒ ⊢ (∀𝑥(𝜒 → 𝜑) ↔ ∀𝑦(𝜃 → 𝜓)) |
|
Theorem | sbhypf 2730* |
Introduce an explicit substitution into an implicit substitution
hypothesis. See also csbhypf . (Contributed by Raph Levien,
10-Apr-2004.)
|
⊢ Ⅎ𝑥𝜓
& ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ 𝜓)) |
|
Theorem | vtoclgft 2731 |
Closed theorem form of vtoclgf 2739. (Contributed by NM, 17-Feb-2013.)
(Revised by Mario Carneiro, 12-Oct-2016.)
|
⊢ (((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑) ∧ 𝐴 ∈ 𝑉) → 𝜓) |
|
Theorem | vtocldf 2732 |
Implicit substitution of a class for a setvar variable. (Contributed
by Mario Carneiro, 15-Oct-2016.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝜓)
& ⊢ Ⅎ𝑥𝜑
& ⊢ (𝜑 → Ⅎ𝑥𝐴)
& ⊢ (𝜑 → Ⅎ𝑥𝜒) ⇒ ⊢ (𝜑 → 𝜒) |
|
Theorem | vtocld 2733* |
Implicit substitution of a class for a setvar variable. (Contributed by
Mario Carneiro, 15-Oct-2016.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → 𝜒) |
|
Theorem | vtoclf 2734* |
Implicit substitution of a class for a setvar variable. This is a
generalization of chvar 1730. (Contributed by NM, 30-Aug-1993.)
|
⊢ Ⅎ𝑥𝜓
& ⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 |
|
Theorem | vtocl 2735* |
Implicit substitution of a class for a setvar variable. (Contributed by
NM, 30-Aug-1993.)
|
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 |
|
Theorem | vtocl2 2736* |
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 2737* |
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 2738* |
Implicit substitution of a class for a setvar variable. (Contributed by
NM, 23-Dec-1993.)
|
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃)) & ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (𝜒 ↔ 𝜃) |
|
Theorem | vtoclgf 2739 |
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 | vtoclg1f 2740* |
Version of vtoclgf 2739 with one non-freeness hypothesis replaced
with a
disjoint variable condition, thus avoiding dependency on ax-11 1484 and
ax-13 1491. (Contributed by BJ, 1-May-2019.)
|
⊢ Ⅎ𝑥𝜓
& ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝜓) |
|
Theorem | vtoclg 2741* |
Implicit substitution of a class expression for a setvar variable.
(Contributed by NM, 17-Apr-1995.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝜓) |
|
Theorem | vtoclbg 2742* |
Implicit substitution of a class for a setvar variable. (Contributed by
NM, 29-Apr-1994.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃)) & ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃)) |
|
Theorem | vtocl2gf 2743 |
Implicit substitution of a class for a setvar variable. (Contributed by
NM, 25-Apr-1995.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑦𝐴
& ⊢ Ⅎ𝑦𝐵
& ⊢ Ⅎ𝑥𝜓
& ⊢ Ⅎ𝑦𝜒
& ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ 𝜑 ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝜒) |
|
Theorem | vtocl3gf 2744 |
Implicit substitution of a class for a setvar variable. (Contributed by
NM, 10-Aug-2013.) (Revised by Mario Carneiro, 10-Oct-2016.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑦𝐴
& ⊢ Ⅎ𝑧𝐴
& ⊢ Ⅎ𝑦𝐵
& ⊢ Ⅎ𝑧𝐵
& ⊢ Ⅎ𝑧𝐶
& ⊢ Ⅎ𝑥𝜓
& ⊢ Ⅎ𝑦𝜒
& ⊢ Ⅎ𝑧𝜃
& ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ 𝜑 ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝜃) |
|
Theorem | vtocl2g 2745* |
Implicit substitution of 2 classes for 2 setvar variables. (Contributed
by NM, 25-Apr-1995.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ 𝜑 ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝜒) |
|
Theorem | vtoclgaf 2746* |
Implicit substitution of a class for a setvar variable. (Contributed by
NM, 17-Feb-2006.) (Revised by Mario Carneiro, 10-Oct-2016.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝜓
& ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 ∈ 𝐵 → 𝜑) ⇒ ⊢ (𝐴 ∈ 𝐵 → 𝜓) |
|
Theorem | vtoclga 2747* |
Implicit substitution of a class for a setvar variable. (Contributed by
NM, 20-Aug-1995.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 ∈ 𝐵 → 𝜑) ⇒ ⊢ (𝐴 ∈ 𝐵 → 𝜓) |
|
Theorem | vtocl2gaf 2748* |
Implicit substitution of 2 classes for 2 setvar variables. (Contributed
by NM, 10-Aug-2013.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑦𝐴
& ⊢ Ⅎ𝑦𝐵
& ⊢ Ⅎ𝑥𝜓
& ⊢ Ⅎ𝑦𝜒
& ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → 𝜑) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝜒) |
|
Theorem | vtocl2ga 2749* |
Implicit substitution of 2 classes for 2 setvar variables. (Contributed
by NM, 20-Aug-1995.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → 𝜑) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝜒) |
|
Theorem | vtocl3gaf 2750* |
Implicit substitution of 3 classes for 3 setvar variables. (Contributed
by NM, 10-Aug-2013.) (Revised by Mario Carneiro, 11-Oct-2016.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑦𝐴
& ⊢ Ⅎ𝑧𝐴
& ⊢ Ⅎ𝑦𝐵
& ⊢ Ⅎ𝑧𝐵
& ⊢ Ⅎ𝑧𝐶
& ⊢ Ⅎ𝑥𝜓
& ⊢ Ⅎ𝑦𝜒
& ⊢ Ⅎ𝑧𝜃
& ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇) → 𝜑) ⇒ ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → 𝜃) |
|
Theorem | vtocl3ga 2751* |
Implicit substitution of 3 classes for 3 setvar variables. (Contributed
by NM, 20-Aug-1995.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑆) → 𝜑) ⇒ ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝑅 ∧ 𝐶 ∈ 𝑆) → 𝜃) |
|
Theorem | vtocleg 2752* |
Implicit substitution of a class for a setvar variable. (Contributed by
NM, 10-Jan-2004.)
|
⊢ (𝑥 = 𝐴 → 𝜑) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝜑) |
|
Theorem | vtoclegft 2753* |
Implicit substitution of a class for a setvar variable. (Closed theorem
version of vtoclef 2754.) (Contributed by NM, 7-Nov-2005.) (Revised
by
Mario Carneiro, 11-Oct-2016.)
|
⊢ ((𝐴 ∈ 𝐵 ∧ Ⅎ𝑥𝜑 ∧ ∀𝑥(𝑥 = 𝐴 → 𝜑)) → 𝜑) |
|
Theorem | vtoclef 2754* |
Implicit substitution of a class for a setvar variable. (Contributed by
NM, 18-Aug-1993.)
|
⊢ Ⅎ𝑥𝜑
& ⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → 𝜑) ⇒ ⊢ 𝜑 |
|
Theorem | vtocle 2755* |
Implicit substitution of a class for a setvar variable. (Contributed by
NM, 9-Sep-1993.)
|
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → 𝜑) ⇒ ⊢ 𝜑 |
|
Theorem | vtoclri 2756* |
Implicit substitution of a class for a setvar variable. (Contributed by
NM, 21-Nov-1994.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ ∀𝑥 ∈ 𝐵 𝜑 ⇒ ⊢ (𝐴 ∈ 𝐵 → 𝜓) |
|
Theorem | spcimgft 2757 |
A closed version of spcimgf 2761. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
⊢ Ⅎ𝑥𝜓
& ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (∀𝑥(𝑥 = 𝐴 → (𝜑 → 𝜓)) → (𝐴 ∈ 𝐵 → (∀𝑥𝜑 → 𝜓))) |
|
Theorem | spcgft 2758 |
A closed version of spcgf 2763. (Contributed by Andrew Salmon,
6-Jun-2011.) (Revised by Mario Carneiro, 4-Jan-2017.)
|
⊢ Ⅎ𝑥𝜓
& ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝐴 ∈ 𝐵 → (∀𝑥𝜑 → 𝜓))) |
|
Theorem | spcimegft 2759 |
A closed version of spcimegf 2762. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
⊢ Ⅎ𝑥𝜓
& ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (∀𝑥(𝑥 = 𝐴 → (𝜓 → 𝜑)) → (𝐴 ∈ 𝐵 → (𝜓 → ∃𝑥𝜑))) |
|
Theorem | spcegft 2760 |
A closed version of spcegf 2764. (Contributed by Jim Kingdon,
22-Jun-2018.)
|
⊢ Ⅎ𝑥𝜓
& ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝐴 ∈ 𝐵 → (𝜓 → ∃𝑥𝜑))) |
|
Theorem | spcimgf 2761 |
Rule of specialization, using implicit substitution. Compare Theorem
7.3 of [Quine] p. 44. (Contributed by
Mario Carneiro, 4-Jan-2017.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝜓
& ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥𝜑 → 𝜓)) |
|
Theorem | spcimegf 2762 |
Existential specialization, using implicit substitution. (Contributed
by Mario Carneiro, 4-Jan-2017.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝜓
& ⊢ (𝑥 = 𝐴 → (𝜓 → 𝜑)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑)) |
|
Theorem | spcgf 2763 |
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 2764 |
Existential specialization, using implicit substitution. (Contributed
by NM, 2-Feb-1997.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝜓
& ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑)) |
|
Theorem | spcimdv 2765* |
Restricted specialization, using implicit substitution. (Contributed
by Mario Carneiro, 4-Jan-2017.)
|
⊢ (𝜑 → 𝐴 ∈ 𝐵)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 → 𝜒)) |
|
Theorem | spcdv 2766* |
Rule of specialization, using implicit substitution. Analogous to
rspcdv 2787. (Contributed by David Moews, 1-May-2017.)
|
⊢ (𝜑 → 𝐴 ∈ 𝐵)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 → 𝜒)) |
|
Theorem | spcimedv 2767* |
Restricted existential specialization, using implicit substitution.
(Contributed by Mario Carneiro, 4-Jan-2017.)
|
⊢ (𝜑 → 𝐴 ∈ 𝐵)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜒 → 𝜓)) ⇒ ⊢ (𝜑 → (𝜒 → ∃𝑥𝜓)) |
|
Theorem | spcgv 2768* |
Rule of specialization, using implicit substitution. Compare Theorem
7.3 of [Quine] p. 44. (Contributed by NM,
22-Jun-1994.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥𝜑 → 𝜓)) |
|
Theorem | spcegv 2769* |
Existential specialization, using implicit substitution. (Contributed
by NM, 14-Aug-1994.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑)) |
|
Theorem | spc2egv 2770* |
Existential specialization with 2 quantifiers, using implicit
substitution. (Contributed by NM, 3-Aug-1995.)
|
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝜓 → ∃𝑥∃𝑦𝜑)) |
|
Theorem | spc2gv 2771* |
Specialization with 2 quantifiers, using implicit substitution.
(Contributed by NM, 27-Apr-2004.)
|
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥∀𝑦𝜑 → 𝜓)) |
|
Theorem | spc3egv 2772* |
Existential specialization with 3 quantifiers, using implicit
substitution. (Contributed by NM, 12-May-2008.)
|
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝜓 → ∃𝑥∃𝑦∃𝑧𝜑)) |
|
Theorem | spc3gv 2773* |
Specialization with 3 quantifiers, using implicit substitution.
(Contributed by NM, 12-May-2008.)
|
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (∀𝑥∀𝑦∀𝑧𝜑 → 𝜓)) |
|
Theorem | spcv 2774* |
Rule of specialization, using implicit substitution. (Contributed by
NM, 22-Jun-1994.)
|
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) |
|
Theorem | spcev 2775* |
Existential specialization, using implicit substitution. (Contributed
by NM, 31-Dec-1993.) (Proof shortened by Eric Schmidt, 22-Dec-2006.)
|
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝜓 → ∃𝑥𝜑) |
|
Theorem | spc2ev 2776* |
Existential specialization, using implicit substitution. (Contributed
by NM, 3-Aug-1995.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝜓 → ∃𝑥∃𝑦𝜑) |
|
Theorem | rspct 2777* |
A closed version of rspc 2778. (Contributed by Andrew Salmon,
6-Jun-2011.)
|
⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))) |
|
Theorem | rspc 2778* |
Restricted specialization, using implicit substitution. (Contributed by
NM, 19-Apr-2005.) (Revised by Mario Carneiro, 11-Oct-2016.)
|
⊢ Ⅎ𝑥𝜓
& ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓)) |
|
Theorem | rspce 2779* |
Restricted existential specialization, using implicit substitution.
(Contributed by NM, 26-May-1998.) (Revised by Mario Carneiro,
11-Oct-2016.)
|
⊢ Ⅎ𝑥𝜓
& ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑) |
|
Theorem | rspcv 2780* |
Restricted specialization, using implicit substitution. (Contributed by
NM, 26-May-1998.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓)) |
|
Theorem | rspccv 2781* |
Restricted specialization, using implicit substitution. (Contributed by
NM, 2-Feb-2006.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐵 𝜑 → (𝐴 ∈ 𝐵 → 𝜓)) |
|
Theorem | rspcva 2782* |
Restricted specialization, using implicit substitution. (Contributed by
NM, 13-Sep-2005.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝜑) → 𝜓) |
|
Theorem | rspccva 2783* |
Restricted specialization, using implicit substitution. (Contributed by
NM, 26-Jul-2006.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((∀𝑥 ∈ 𝐵 𝜑 ∧ 𝐴 ∈ 𝐵) → 𝜓) |
|
Theorem | rspcev 2784* |
Restricted existential specialization, using implicit substitution.
(Contributed by NM, 26-May-1998.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑) |
|
Theorem | rspcimdv 2785* |
Restricted specialization, using implicit substitution. (Contributed
by Mario Carneiro, 4-Jan-2017.)
|
⊢ (𝜑 → 𝐴 ∈ 𝐵)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 → 𝜒)) |
|
Theorem | rspcimedv 2786* |
Restricted existential specialization, using implicit substitution.
(Contributed by Mario Carneiro, 4-Jan-2017.)
|
⊢ (𝜑 → 𝐴 ∈ 𝐵)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜒 → 𝜓)) ⇒ ⊢ (𝜑 → (𝜒 → ∃𝑥 ∈ 𝐵 𝜓)) |
|
Theorem | rspcdv 2787* |
Restricted specialization, using implicit substitution. (Contributed by
NM, 17-Feb-2007.) (Revised by Mario Carneiro, 4-Jan-2017.)
|
⊢ (𝜑 → 𝐴 ∈ 𝐵)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 → 𝜒)) |
|
Theorem | rspcedv 2788* |
Restricted existential specialization, using implicit substitution.
(Contributed by FL, 17-Apr-2007.) (Revised by Mario Carneiro,
4-Jan-2017.)
|
⊢ (𝜑 → 𝐴 ∈ 𝐵)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝜒 → ∃𝑥 ∈ 𝐵 𝜓)) |
|
Theorem | rspcdva 2789* |
Restricted specialization, using implicit substitution. (Contributed by
Thierry Arnoux, 21-Jun-2020.)
|
⊢ (𝑥 = 𝐶 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)
& ⊢ (𝜑 → 𝐶 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝜒) |
|
Theorem | rspcedvd 2790* |
Restricted existential specialization, using implicit substitution.
Variant of rspcedv 2788. (Contributed by AV, 27-Nov-2019.)
|
⊢ (𝜑 → 𝐴 ∈ 𝐵)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝜒) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓) |
|
Theorem | rspcime 2791* |
Prove a restricted existential. (Contributed by Rohan Ridenour,
3-Aug-2023.)
|
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝜓)
& ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓) |
|
Theorem | rspceaimv 2792* |
Restricted existential specialization of a universally quantified
implication. (Contributed by BJ, 24-Aug-2022.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐶 (𝜓 → 𝜒)) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 (𝜑 → 𝜒)) |
|
Theorem | rspcedeq1vd 2793* |
Restricted existential specialization, using implicit substitution.
Variant of rspcedvd 2790 for equations, in which the left hand side
depends on the quantified variable. (Contributed by AV,
24-Dec-2019.)
|
⊢ (𝜑 → 𝐴 ∈ 𝐵)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝐶 = 𝐷) |
|
Theorem | rspcedeq2vd 2794* |
Restricted existential specialization, using implicit substitution.
Variant of rspcedvd 2790 for equations, in which the right hand side
depends on the quantified variable. (Contributed by AV,
24-Dec-2019.)
|
⊢ (𝜑 → 𝐴 ∈ 𝐵)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝐶 = 𝐷) |
|
Theorem | rspc2 2795* |
2-variable restricted specialization, using implicit substitution.
(Contributed by NM, 9-Nov-2012.)
|
⊢ Ⅎ𝑥𝜒
& ⊢ Ⅎ𝑦𝜓
& ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓)) |
|
Theorem | rspc2gv 2796* |
Restricted specialization with two quantifiers, using implicit
substitution. (Contributed by BJ, 2-Dec-2021.)
|
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑊 𝜑 → 𝜓)) |
|
Theorem | rspc2v 2797* |
2-variable restricted specialization, using implicit substitution.
(Contributed by NM, 13-Sep-1999.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓)) |
|
Theorem | rspc2va 2798* |
2-variable restricted specialization, using implicit substitution.
(Contributed by NM, 18-Jun-2014.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓)) ⇒ ⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑) → 𝜓) |
|
Theorem | rspc2ev 2799* |
2-variable restricted existential specialization, using implicit
substitution. (Contributed by NM, 16-Oct-1999.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 𝜑) |
|
Theorem | rspc3v 2800* |
3-variable restricted specialization, using implicit substitution.
(Contributed by NM, 10-May-2005.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜃)) & ⊢ (𝑧 = 𝐶 → (𝜃 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑇 𝜑 → 𝜓)) |