Theorem List for Intuitionistic Logic Explorer - 2801-2900 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | sbcor 2801 |
Distribution of class substitution over disjunction. (Contributed by
NM, 31-Dec-2016.)
|
⊢ ([A
/ x](φ ∨ ψ) ↔ ([A / x]φ
∨ [A / x]ψ)) |
|
Theorem | sbcorg 2802 |
Distribution of class substitution over disjunction. (Contributed by
NM, 21-May-2004.)
|
⊢ (A ∈ 𝑉 → ([A / x](φ
∨ ψ)
↔ ([A / x]φ
∨ [A / x]ψ))) |
|
Theorem | sbcbig 2803 |
Distribution of class substitution over biconditional. (Contributed by
Raph Levien, 10-Apr-2004.)
|
⊢ (A ∈ 𝑉 → ([A / x](φ
↔ ψ) ↔ ([A / x]φ
↔ [A / x]ψ))) |
|
Theorem | sbcal 2804* |
Move universal quantifier in and out of class substitution.
(Contributed by NM, 31-Dec-2016.)
|
⊢ ([A
/ y]∀xφ ↔ ∀x[A /
y]φ) |
|
Theorem | sbcalg 2805* |
Move universal quantifier in and out of class substitution.
(Contributed by NM, 16-Jan-2004.)
|
⊢ (A ∈ 𝑉 → ([A / y]∀xφ ↔ ∀x[A /
y]φ)) |
|
Theorem | sbcex2 2806* |
Move existential quantifier in and out of class substitution.
(Contributed by NM, 21-May-2004.)
|
⊢ ([A
/ y]∃xφ ↔ ∃x[A /
y]φ) |
|
Theorem | sbcexg 2807* |
Move existential quantifier in and out of class substitution.
(Contributed by NM, 21-May-2004.)
|
⊢ (A ∈ 𝑉 → ([A / y]∃xφ ↔ ∃x[A /
y]φ)) |
|
Theorem | sbceqal 2808* |
A variation of extensionality for classes. (Contributed by Andrew
Salmon, 28-Jun-2011.)
|
⊢ (A ∈ 𝑉 → (∀x(x = A →
x = B)
→ A = B)) |
|
Theorem | sbeqalb 2809* |
Theorem *14.121 in [WhiteheadRussell]
p. 185. (Contributed by Andrew
Salmon, 28-Jun-2011.) (Proof shortened by Wolf Lammen, 9-May-2013.)
|
⊢ (A ∈ 𝑉 → ((∀x(φ ↔ x = A) ∧ ∀x(φ ↔
x = B)) → A =
B)) |
|
Theorem | sbcbid 2810 |
Formula-building deduction rule for class substitution. (Contributed by
NM, 29-Dec-2014.)
|
⊢ Ⅎxφ
& ⊢ (φ
→ (ψ ↔ χ)) ⇒ ⊢ (φ → ([A / x]ψ
↔ [A / x]χ)) |
|
Theorem | sbcbidv 2811* |
Formula-building deduction rule for class substitution. (Contributed by
NM, 29-Dec-2014.)
|
⊢ (φ
→ (ψ ↔ χ)) ⇒ ⊢ (φ → ([A / x]ψ
↔ [A / x]χ)) |
|
Theorem | sbcbii 2812 |
Formula-building inference rule for class substitution. (Contributed by
NM, 11-Nov-2005.)
|
⊢ (φ
↔ ψ)
⇒ ⊢ ([A / x]φ
↔ [A / x]ψ) |
|
Theorem | eqsbc3r 2813* |
eqsbc3 2796 with setvar variable on right side of equals
sign.
(Contributed by Alan Sare, 24-Oct-2011.)
|
⊢ (A ∈ B →
([A / x]𝐶 = x
↔ 𝐶 = A)) |
|
Theorem | sbc3ang 2814 |
Distribution of class substitution over triple conjunction.
(Contributed by NM, 14-Dec-2006.) (Proof shortened by Andrew Salmon,
29-Jun-2011.)
|
⊢ (A ∈ 𝑉 → ([A / x](φ
∧ ψ
∧ χ)
↔ ([A / x]φ
∧ [A / x]ψ
∧ [A / x]χ))) |
|
Theorem | sbcel1gv 2815* |
Class substitution into a membership relation. (Contributed by NM,
17-Nov-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|
⊢ (A ∈ 𝑉 → ([A / x]x
∈ B
↔ A ∈ B)) |
|
Theorem | sbcel2gv 2816* |
Class substitution into a membership relation. (Contributed by NM,
17-Nov-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|
⊢ (B ∈ 𝑉 → ([B / x]A
∈ x
↔ A ∈ B)) |
|
Theorem | sbcimdv 2817* |
Substitution analog of Theorem 19.20 of [Margaris] p. 90. (Contributed
by NM, 11-Nov-2005.)
|
⊢ (φ
→ (ψ → χ)) ⇒ ⊢ ((φ ∧
A ∈
𝑉) →
([A / x]ψ
→ [A / x]χ)) |
|
Theorem | sbctt 2818 |
Substitution for a variable not free in a wff does not affect it.
(Contributed by Mario Carneiro, 14-Oct-2016.)
|
⊢ ((A ∈ 𝑉 ∧
Ⅎxφ) → ([A / x]φ
↔ φ)) |
|
Theorem | sbcgf 2819 |
Substitution for a variable not free in a wff does not affect it.
(Contributed by NM, 11-Oct-2004.) (Proof shortened by Andrew Salmon,
29-Jun-2011.)
|
⊢ Ⅎxφ ⇒ ⊢ (A ∈ 𝑉 → ([A / x]φ
↔ φ)) |
|
Theorem | sbc19.21g 2820 |
Substitution for a variable not free in antecedent affects only the
consequent. (Contributed by NM, 11-Oct-2004.)
|
⊢ Ⅎxφ ⇒ ⊢ (A ∈ 𝑉 → ([A / x](φ
→ ψ) ↔ (φ → [A / x]ψ))) |
|
Theorem | sbcg 2821* |
Substitution for a variable not occurring in a wff does not affect it.
Distinct variable form of sbcgf 2819. (Contributed by Alan Sare,
10-Nov-2012.)
|
⊢ (A ∈ 𝑉 → ([A / x]φ
↔ φ)) |
|
Theorem | sbc2iegf 2822* |
Conversion of implicit substitution to explicit class substitution.
(Contributed by Mario Carneiro, 19-Dec-2013.)
|
⊢ Ⅎxψ
& ⊢ Ⅎyψ
& ⊢ Ⅎx
B ∈
𝑊 & ⊢ ((x = A ∧ y = B) → (φ ↔ ψ)) ⇒ ⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊) → ([A / x][B / y]φ
↔ ψ)) |
|
Theorem | sbc2ie 2823* |
Conversion of implicit substitution to explicit class substitution.
(Contributed by NM, 16-Dec-2008.) (Revised by Mario Carneiro,
19-Dec-2013.)
|
⊢ A ∈ V
& ⊢ B ∈ V
& ⊢ ((x =
A ∧
y = B)
→ (φ ↔ ψ)) ⇒ ⊢ ([A / x][B / y]φ
↔ ψ) |
|
Theorem | sbc2iedv 2824* |
Conversion of implicit substitution to explicit class substitution.
(Contributed by NM, 16-Dec-2008.) (Proof shortened by Mario Carneiro,
18-Oct-2016.)
|
⊢ A ∈ V
& ⊢ B ∈ V
& ⊢ (φ
→ ((x = A ∧ y = B) →
(ψ ↔ χ))) ⇒ ⊢ (φ → ([A / x][B / y]ψ
↔ χ)) |
|
Theorem | sbc3ie 2825* |
Conversion of implicit substitution to explicit class substitution.
(Contributed by Mario Carneiro, 19-Jun-2014.) (Revised by Mario
Carneiro, 29-Dec-2014.)
|
⊢ A ∈ V
& ⊢ B ∈ V
& ⊢ 𝐶 ∈
V
& ⊢ ((x =
A ∧
y = B
∧ z =
𝐶) → (φ ↔ ψ)) ⇒ ⊢ ([A / x][B / y][𝐶 / z]φ
↔ ψ) |
|
Theorem | sbccomlem 2826* |
Lemma for sbccom 2827. (Contributed by NM, 14-Nov-2005.) (Revised
by
Mario Carneiro, 18-Oct-2016.)
|
⊢ ([A
/ x][B / y]φ
↔ [B / y][A / x]φ) |
|
Theorem | sbccom 2827* |
Commutative law for double class substitution. (Contributed by NM,
15-Nov-2005.) (Proof shortened by Mario Carneiro, 18-Oct-2016.)
|
⊢ ([A
/ x][B / y]φ
↔ [B / y][A / x]φ) |
|
Theorem | sbcralt 2828* |
Interchange class substitution and restricted quantifier. (Contributed
by NM, 1-Mar-2008.) (Revised by David Abernethy, 22-Feb-2010.)
|
⊢ ((A ∈ 𝑉 ∧
ℲyA) → ([A / x]∀y ∈ B φ ↔ ∀y ∈ B
[A / x]φ)) |
|
Theorem | sbcrext 2829* |
Interchange class substitution and restricted existential quantifier.
(Contributed by NM, 1-Mar-2008.) (Proof shortened by Mario Carneiro,
13-Oct-2016.)
|
⊢ ((A ∈ 𝑉 ∧
ℲyA) → ([A / x]∃y ∈ B φ ↔ ∃y ∈ B
[A / x]φ)) |
|
Theorem | sbcralg 2830* |
Interchange class substitution and restricted quantifier. (Contributed
by NM, 15-Nov-2005.) (Proof shortened by Andrew Salmon,
29-Jun-2011.)
|
⊢ (A ∈ 𝑉 → ([A / x]∀y ∈ B φ ↔ ∀y ∈ B
[A / x]φ)) |
|
Theorem | sbcrexg 2831* |
Interchange class substitution and restricted existential quantifier.
(Contributed by NM, 15-Nov-2005.) (Proof shortened by Andrew Salmon,
29-Jun-2011.)
|
⊢ (A ∈ 𝑉 → ([A / x]∃y ∈ B φ ↔ ∃y ∈ B
[A / x]φ)) |
|
Theorem | sbcreug 2832* |
Interchange class substitution and restricted uniqueness quantifier.
(Contributed by NM, 24-Feb-2013.)
|
⊢ (A ∈ 𝑉 → ([A / x]∃!y ∈ B φ ↔ ∃!y ∈ B
[A / x]φ)) |
|
Theorem | sbcabel 2833* |
Interchange class substitution and class abstraction. (Contributed by
NM, 5-Nov-2005.)
|
⊢ ℲxB ⇒ ⊢ (A ∈ 𝑉 → ([A / x]{y
∣ φ} ∈ B ↔
{y ∣ [A / x]φ}
∈ B)) |
|
Theorem | rspsbc 2834* |
Restricted quantifier version of Axiom 4 of [Mendelson] p. 69. This
provides an axiom for a predicate calculus for a restricted domain.
This theorem generalizes the unrestricted stdpc4 1655 and spsbc 2769. See
also rspsbca 2835 and rspcsbela . (Contributed by NM,
17-Nov-2006.)
(Proof shortened by Mario Carneiro, 13-Oct-2016.)
|
⊢ (A ∈ B →
(∀x
∈ B
φ → [A / x]φ)) |
|
Theorem | rspsbca 2835* |
Restricted quantifier version of Axiom 4 of [Mendelson] p. 69.
(Contributed by NM, 14-Dec-2005.)
|
⊢ ((A ∈ B ∧ ∀x ∈ B φ) →
[A / x]φ) |
|
Theorem | rspesbca 2836* |
Existence form of rspsbca 2835. (Contributed by NM, 29-Feb-2008.) (Proof
shortened by Mario Carneiro, 13-Oct-2016.)
|
⊢ ((A ∈ B ∧ [A /
x]φ) → ∃x ∈ B φ) |
|
Theorem | spesbc 2837 |
Existence form of spsbc 2769. (Contributed by Mario Carneiro,
18-Nov-2016.)
|
⊢ ([A
/ x]φ → ∃xφ) |
|
Theorem | spesbcd 2838 |
form of spsbc 2769. (Contributed by Mario Carneiro,
9-Feb-2017.)
|
⊢ (φ
→ [A / x]ψ) ⇒ ⊢ (φ → ∃xψ) |
|
Theorem | sbcth2 2839* |
A substitution into a theorem. (Contributed by NM, 1-Mar-2008.) (Proof
shortened by Mario Carneiro, 13-Oct-2016.)
|
⊢ (x ∈ B →
φ) ⇒ ⊢ (A ∈ B → [A / x]φ) |
|
Theorem | ra5 2840 |
Restricted quantifier version of Axiom 5 of [Mendelson] p. 69. This is
an axiom of a predicate calculus for a restricted domain. Compare the
unrestricted stdpc5 1473. (Contributed by NM, 16-Jan-2004.)
|
⊢ Ⅎxφ ⇒ ⊢ (∀x ∈ A (φ → ψ) → (φ → ∀x ∈ A ψ)) |
|
Theorem | rmo2ilem 2841* |
Condition implying restricted "at most one." (Contributed by Jim
Kingdon, 14-Jul-2018.)
|
⊢ Ⅎyφ ⇒ ⊢ (∃y∀x ∈ A (φ → x = y) →
∃*x
∈ A
φ) |
|
Theorem | rmo2i 2842* |
Condition implying restricted "at most one." (Contributed by NM,
17-Jun-2017.)
|
⊢ Ⅎyφ ⇒ ⊢ (∃y ∈ A ∀x ∈ A (φ → x = y) →
∃*x
∈ A
φ) |
|
Theorem | rmo3 2843* |
Restricted "at most one" using explicit substitution. (Contributed
by
NM, 4-Nov-2012.) (Revised by NM, 16-Jun-2017.)
|
⊢ Ⅎyφ ⇒ ⊢ (∃*x ∈ A φ ↔ ∀x ∈ A ∀y ∈ A ((φ ∧
[y / x]φ) →
x = y)) |
|
Theorem | rmob 2844* |
Consequence of "at most one", using implicit substitution.
(Contributed
by NM, 2-Jan-2015.) (Revised by NM, 16-Jun-2017.)
|
⊢ (x =
B → (φ ↔ ψ)) & ⊢ (x = 𝐶 → (φ ↔ χ)) ⇒ ⊢ ((∃*x ∈ A φ ∧
(B ∈
A ∧ ψ)) → (B = 𝐶 ↔ (𝐶 ∈
A ∧ χ))) |
|
Theorem | rmoi 2845* |
Consequence of "at most one", using implicit substitution.
(Contributed
by NM, 4-Nov-2012.) (Revised by NM, 16-Jun-2017.)
|
⊢ (x =
B → (φ ↔ ψ)) & ⊢ (x = 𝐶 → (φ ↔ χ)) ⇒ ⊢ ((∃*x ∈ A φ ∧
(B ∈
A ∧ ψ) ∧ (𝐶 ∈ A ∧ χ))
→ B = 𝐶) |
|
2.1.10 Proper substitution of classes for sets
into classes
|
|
Syntax | csb 2846 |
Extend class notation to include the proper substitution of a class for a
set into another class.
|
class ⦋A / x⦌B |
|
Definition | df-csb 2847* |
Define the proper substitution of a class for a set into another class.
The underlined brackets distinguish it from the substitution into a wff,
wsbc 2758, to prevent ambiguity. Theorem sbcel1g 2863 shows an example of
how ambiguity could arise if we didn't use distinguished brackets.
Theorem sbccsbg 2872 recreates substitution into a wff from this
definition. (Contributed by NM, 10-Nov-2005.)
|
⊢ ⦋A / x⦌B = {y ∣
[A / x]y
∈ B} |
|
Theorem | csb2 2848* |
Alternate expression for the proper substitution into a class, without
referencing substitution into a wff. Note that x can be free in
B but cannot
occur in A.
(Contributed by NM, 2-Dec-2013.)
|
⊢ ⦋A / x⦌B = {y ∣
∃x(x = A ∧ y ∈ B)} |
|
Theorem | csbeq1 2849 |
Analog of dfsbcq 2760 for proper substitution into a class.
(Contributed
by NM, 10-Nov-2005.)
|
⊢ (A =
B → ⦋A / x⦌𝐶 = ⦋B / x⦌𝐶) |
|
Theorem | cbvcsb 2850 |
Change bound variables in a class substitution. Interestingly, this
does not require any bound variable conditions on A. (Contributed
by Jeff Hankins, 13-Sep-2009.) (Revised by Mario Carneiro,
11-Dec-2016.)
|
⊢ Ⅎy𝐶
& ⊢ Ⅎx𝐷
& ⊢ (x =
y → 𝐶 = 𝐷) ⇒ ⊢ ⦋A / x⦌𝐶 = ⦋A / y⦌𝐷 |
|
Theorem | cbvcsbv 2851* |
Change the bound variable of a proper substitution into a class using
implicit substitution. (Contributed by NM, 30-Sep-2008.) (Revised by
Mario Carneiro, 13-Oct-2016.)
|
⊢ (x =
y → B = 𝐶) ⇒ ⊢ ⦋A / x⦌B = ⦋A / y⦌𝐶 |
|
Theorem | csbeq1d 2852 |
Equality deduction for proper substitution into a class. (Contributed
by NM, 3-Dec-2005.)
|
⊢ (φ
→ A = B) ⇒ ⊢ (φ → ⦋A / x⦌𝐶 = ⦋B / x⦌𝐶) |
|
Theorem | csbid 2853 |
Analog of sbid 1654 for proper substitution into a class.
(Contributed by
NM, 10-Nov-2005.)
|
⊢ ⦋x / x⦌A = A |
|
Theorem | csbeq1a 2854 |
Equality theorem for proper substitution into a class. (Contributed by
NM, 10-Nov-2005.)
|
⊢ (x =
A → B = ⦋A / x⦌B) |
|
Theorem | csbco 2855* |
Composition law for chained substitutions into a class. (Contributed by
NM, 10-Nov-2005.)
|
⊢ ⦋A / y⦌⦋y / x⦌B = ⦋A / x⦌B |
|
Theorem | csbtt 2856 |
Substitution doesn't affect a constant B (in which x is not
free). (Contributed by Mario Carneiro, 14-Oct-2016.)
|
⊢ ((A ∈ 𝑉 ∧
ℲxB) → ⦋A / x⦌B = B) |
|
Theorem | csbconstgf 2857 |
Substitution doesn't affect a constant B (in which x is not
free). (Contributed by NM, 10-Nov-2005.)
|
⊢ ℲxB ⇒ ⊢ (A ∈ 𝑉 → ⦋A / x⦌B = B) |
|
Theorem | csbconstg 2858* |
Substitution doesn't affect a constant B (in which x is not
free). csbconstgf 2857 with distinct variable requirement.
(Contributed by
Alan Sare, 22-Jul-2012.)
|
⊢ (A ∈ 𝑉 → ⦋A / x⦌B = B) |
|
Theorem | sbcel12g 2859 |
Distribute proper substitution through a membership relation.
(Contributed by NM, 10-Nov-2005.) (Proof shortened by Andrew Salmon,
29-Jun-2011.)
|
⊢ (A ∈ 𝑉 → ([A / x]B
∈ 𝐶 ↔ ⦋A / x⦌B ∈
⦋A / x⦌𝐶)) |
|
Theorem | sbceqg 2860 |
Distribute proper substitution through an equality relation.
(Contributed by NM, 10-Nov-2005.) (Proof shortened by Andrew Salmon,
29-Jun-2011.)
|
⊢ (A ∈ 𝑉 → ([A / x]B =
𝐶 ↔
⦋A / x⦌B = ⦋A / x⦌𝐶)) |
|
Theorem | sbcnel12g 2861 |
Distribute proper substitution through negated membership. (Contributed
by Andrew Salmon, 18-Jun-2011.)
|
⊢ (A ∈ 𝑉 → ([A / x]B
∉ 𝐶 ↔
⦋A / x⦌B ∉ ⦋A / x⦌𝐶)) |
|
Theorem | sbcne12g 2862 |
Distribute proper substitution through an inequality. (Contributed by
Andrew Salmon, 18-Jun-2011.)
|
⊢ (A ∈ 𝑉 → ([A / x]B ≠
𝐶 ↔
⦋A / x⦌B ≠ ⦋A / x⦌𝐶)) |
|
Theorem | sbcel1g 2863* |
Move proper substitution in and out of a membership relation. Note that
the scope of [A / x] is the wff B ∈ 𝐶, whereas the scope
of ⦋A
/ x⦌ is the class
B. (Contributed by
NM,
10-Nov-2005.)
|
⊢ (A ∈ 𝑉 → ([A / x]B
∈ 𝐶 ↔ ⦋A / x⦌B ∈ 𝐶)) |
|
Theorem | sbceq1g 2864* |
Move proper substitution to first argument of an equality. (Contributed
by NM, 30-Nov-2005.)
|
⊢ (A ∈ 𝑉 → ([A / x]B =
𝐶 ↔
⦋A / x⦌B = 𝐶)) |
|
Theorem | sbcel2g 2865* |
Move proper substitution in and out of a membership relation.
(Contributed by NM, 14-Nov-2005.)
|
⊢ (A ∈ 𝑉 → ([A / x]B
∈ 𝐶 ↔ B ∈
⦋A / x⦌𝐶)) |
|
Theorem | sbceq2g 2866* |
Move proper substitution to second argument of an equality.
(Contributed by NM, 30-Nov-2005.)
|
⊢ (A ∈ 𝑉 → ([A / x]B =
𝐶 ↔ B = ⦋A / x⦌𝐶)) |
|
Theorem | csbcomg 2867* |
Commutative law for double substitution into a class. (Contributed by
NM, 14-Nov-2005.)
|
⊢ ((A ∈ 𝑉 ∧
B ∈
𝑊) →
⦋A / x⦌⦋B / y⦌𝐶 = ⦋B / y⦌⦋A / x⦌𝐶) |
|
Theorem | csbeq2d 2868 |
Formula-building deduction rule for class substitution. (Contributed by
NM, 22-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
|
⊢ Ⅎxφ
& ⊢ (φ
→ B = 𝐶) ⇒ ⊢ (φ → ⦋A / x⦌B = ⦋A / x⦌𝐶) |
|
Theorem | csbeq2dv 2869* |
Formula-building deduction rule for class substitution. (Contributed by
NM, 10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
|
⊢ (φ
→ B = 𝐶) ⇒ ⊢ (φ → ⦋A / x⦌B = ⦋A / x⦌𝐶) |
|
Theorem | csbeq2i 2870 |
Formula-building inference rule for class substitution. (Contributed by
NM, 10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
|
⊢ B = 𝐶 ⇒ ⊢ ⦋A / x⦌B = ⦋A / x⦌𝐶 |
|
Theorem | csbvarg 2871 |
The proper substitution of a class for setvar variable results in the
class (if the class exists). (Contributed by NM, 10-Nov-2005.)
|
⊢ (A ∈ 𝑉 → ⦋A / x⦌x = A) |
|
Theorem | sbccsbg 2872* |
Substitution into a wff expressed in terms of substitution into a
class. (Contributed by NM, 15-Aug-2007.)
|
⊢ (A ∈ 𝑉 → ([A / x]φ
↔ y ∈ ⦋A / x⦌{y ∣ φ})) |
|
Theorem | sbccsb2g 2873 |
Substitution into a wff expressed in using substitution into a class.
(Contributed by NM, 27-Nov-2005.)
|
⊢ (A ∈ 𝑉 → ([A / x]φ
↔ A ∈ ⦋A / x⦌{x ∣ φ})) |
|
Theorem | nfcsb1d 2874 |
Bound-variable hypothesis builder for substitution into a class.
(Contributed by Mario Carneiro, 12-Oct-2016.)
|
⊢ (φ
→ ℲxA) ⇒ ⊢ (φ → Ⅎx⦋A / x⦌B) |
|
Theorem | nfcsb1 2875 |
Bound-variable hypothesis builder for substitution into a class.
(Contributed by Mario Carneiro, 12-Oct-2016.)
|
⊢ ℲxA ⇒ ⊢ Ⅎx⦋A / x⦌B |
|
Theorem | nfcsb1v 2876* |
Bound-variable hypothesis builder for substitution into a class.
(Contributed by NM, 17-Aug-2006.) (Revised by Mario Carneiro,
12-Oct-2016.)
|
⊢ Ⅎx⦋A / x⦌B |
|
Theorem | nfcsbd 2877 |
Deduction version of nfcsb 2878. (Contributed by NM, 21-Nov-2005.)
(Revised by Mario Carneiro, 12-Oct-2016.)
|
⊢ Ⅎyφ
& ⊢ (φ
→ ℲxA)
& ⊢ (φ
→ ℲxB) ⇒ ⊢ (φ → Ⅎx⦋A / y⦌B) |
|
Theorem | nfcsb 2878 |
Bound-variable hypothesis builder for substitution into a class.
(Contributed by Mario Carneiro, 12-Oct-2016.)
|
⊢ ℲxA & ⊢
ℲxB ⇒ ⊢ Ⅎx⦋A / y⦌B |
|
Theorem | csbhypf 2879* |
Introduce an explicit substitution into an implicit substitution
hypothesis. See sbhypf 2597 for class substitution version. (Contributed
by NM, 19-Dec-2008.)
|
⊢ ℲxA & ⊢
Ⅎx𝐶
& ⊢ (x =
A → B = 𝐶) ⇒ ⊢ (y = A →
⦋y / x⦌B = 𝐶) |
|
Theorem | csbiebt 2880* |
Conversion of implicit substitution to explicit substitution into a
class. (Closed theorem version of csbiegf 2884.) (Contributed by NM,
11-Nov-2005.)
|
⊢ ((A ∈ 𝑉 ∧
Ⅎx𝐶) → (∀x(x = A →
B = 𝐶) ↔ ⦋A / x⦌B = 𝐶)) |
|
Theorem | csbiedf 2881* |
Conversion of implicit substitution to explicit substitution into a
class. (Contributed by Mario Carneiro, 13-Oct-2016.)
|
⊢ Ⅎxφ
& ⊢ (φ
→ Ⅎx𝐶)
& ⊢ (φ
→ A ∈ 𝑉)
& ⊢ ((φ
∧ x =
A) → B = 𝐶) ⇒ ⊢ (φ → ⦋A / x⦌B = 𝐶) |
|
Theorem | csbieb 2882* |
Bidirectional conversion between an implicit class substitution
hypothesis x =
A → B = 𝐶 and its explicit substitution
equivalent.
(Contributed by NM, 2-Mar-2008.)
|
⊢ A ∈ V
& ⊢ Ⅎx𝐶 ⇒ ⊢ (∀x(x = A →
B = 𝐶) ↔ ⦋A / x⦌B = 𝐶) |
|
Theorem | csbiebg 2883* |
Bidirectional conversion between an implicit class substitution
hypothesis x =
A → B = 𝐶 and its explicit substitution
equivalent.
(Contributed by NM, 24-Mar-2013.) (Revised by Mario Carneiro,
11-Dec-2016.)
|
⊢ Ⅎx𝐶 ⇒ ⊢ (A ∈ 𝑉 → (∀x(x = A →
B = 𝐶) ↔ ⦋A / x⦌B = 𝐶)) |
|
Theorem | csbiegf 2884* |
Conversion of implicit substitution to explicit substitution into a
class. (Contributed by NM, 11-Nov-2005.) (Revised by Mario Carneiro,
13-Oct-2016.)
|
⊢ (A ∈ 𝑉 → Ⅎx𝐶)
& ⊢ (x =
A → B = 𝐶) ⇒ ⊢ (A ∈ 𝑉 → ⦋A / x⦌B = 𝐶) |
|
Theorem | csbief 2885* |
Conversion of implicit substitution to explicit substitution into a
class. (Contributed by NM, 26-Nov-2005.) (Revised by Mario Carneiro,
13-Oct-2016.)
|
⊢ A ∈ V
& ⊢ Ⅎx𝐶
& ⊢ (x =
A → B = 𝐶) ⇒ ⊢ ⦋A / x⦌B = 𝐶 |
|
Theorem | csbied 2886* |
Conversion of implicit substitution to explicit substitution into a
class. (Contributed by Mario Carneiro, 2-Dec-2014.) (Revised by Mario
Carneiro, 13-Oct-2016.)
|
⊢ (φ
→ A ∈ 𝑉)
& ⊢ ((φ
∧ x =
A) → B = 𝐶) ⇒ ⊢ (φ → ⦋A / x⦌B = 𝐶) |
|
Theorem | csbied2 2887* |
Conversion of implicit substitution to explicit class substitution,
deduction form. (Contributed by Mario Carneiro, 2-Jan-2017.)
|
⊢ (φ
→ A ∈ 𝑉)
& ⊢ (φ
→ A = B)
& ⊢ ((φ
∧ x =
B) → 𝐶 = 𝐷) ⇒ ⊢ (φ → ⦋A / x⦌𝐶 = 𝐷) |
|
Theorem | csbie2t 2888* |
Conversion of implicit substitution to explicit substitution into a
class (closed form of csbie2 2889). (Contributed by NM, 3-Sep-2007.)
(Revised by Mario Carneiro, 13-Oct-2016.)
|
⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (∀x∀y((x = A ∧ y = B) → 𝐶 = 𝐷) → ⦋A / x⦌⦋B / y⦌𝐶 = 𝐷) |
|
Theorem | csbie2 2889* |
Conversion of implicit substitution to explicit substitution into a
class. (Contributed by NM, 27-Aug-2007.)
|
⊢ A ∈ V
& ⊢ B ∈ V
& ⊢ ((x =
A ∧
y = B)
→ 𝐶 = 𝐷)
⇒ ⊢ ⦋A / x⦌⦋B / y⦌𝐶 = 𝐷 |
|
Theorem | csbie2g 2890* |
Conversion of implicit substitution to explicit class substitution.
This version of sbcie 2791 avoids a disjointness condition on x and
A by
substituting twice. (Contributed by Mario Carneiro,
11-Nov-2016.)
|
⊢ (x =
y → B = 𝐶)
& ⊢ (y =
A → 𝐶 = 𝐷) ⇒ ⊢ (A ∈ 𝑉 → ⦋A / x⦌B = 𝐷) |
|
Theorem | sbcnestgf 2891 |
Nest the composition of two substitutions. (Contributed by Mario
Carneiro, 11-Nov-2016.)
|
⊢ ((A ∈ 𝑉 ∧ ∀yℲxφ) → ([A / x][B / y]φ
↔ [⦋A / x⦌B / y]φ)) |
|
Theorem | csbnestgf 2892 |
Nest the composition of two substitutions. (Contributed by NM,
23-Nov-2005.) (Proof shortened by Mario Carneiro, 10-Nov-2016.)
|
⊢ ((A ∈ 𝑉 ∧ ∀yℲx𝐶) → ⦋A / x⦌⦋B / y⦌𝐶 = ⦋⦋A / x⦌B / y⦌𝐶) |
|
Theorem | sbcnestg 2893* |
Nest the composition of two substitutions. (Contributed by NM,
27-Nov-2005.) (Proof shortened by Mario Carneiro, 11-Nov-2016.)
|
⊢ (A ∈ 𝑉 → ([A / x][B / y]φ
↔ [⦋A / x⦌B / y]φ)) |
|
Theorem | csbnestg 2894* |
Nest the composition of two substitutions. (Contributed by NM,
23-Nov-2005.) (Proof shortened by Mario Carneiro, 10-Nov-2016.)
|
⊢ (A ∈ 𝑉 → ⦋A / x⦌⦋B / y⦌𝐶 = ⦋⦋A / x⦌B / y⦌𝐶) |
|
Theorem | csbnest1g 2895 |
Nest the composition of two substitutions. (Contributed by NM,
23-May-2006.) (Proof shortened by Mario Carneiro, 11-Nov-2016.)
|
⊢ (A ∈ 𝑉 → ⦋A / x⦌⦋B / x⦌𝐶 = ⦋⦋A / x⦌B / x⦌𝐶) |
|
Theorem | csbidmg 2896* |
Idempotent law for class substitutions. (Contributed by NM,
1-Mar-2008.)
|
⊢ (A ∈ 𝑉 → ⦋A / x⦌⦋A / x⦌B = ⦋A / x⦌B) |
|
Theorem | sbcco3g 2897* |
Composition of two substitutions. (Contributed by NM, 27-Nov-2005.)
(Revised by Mario Carneiro, 11-Nov-2016.)
|
⊢ (x =
A → B = 𝐶) ⇒ ⊢ (A ∈ 𝑉 → ([A / x][B / y]φ
↔ [𝐶 /
y]φ)) |
|
Theorem | csbco3g 2898* |
Composition of two class substitutions. (Contributed by NM,
27-Nov-2005.) (Revised by Mario Carneiro, 11-Nov-2016.)
|
⊢ (x =
A → B = 𝐶) ⇒ ⊢ (A ∈ 𝑉 → ⦋A / x⦌⦋B / y⦌𝐷 = ⦋𝐶 / y⦌𝐷) |
|
Theorem | rspcsbela 2899* |
Special case related to rspsbc 2834. (Contributed by NM, 10-Dec-2005.)
(Proof shortened by Eric Schmidt, 17-Jan-2007.)
|
⊢ ((A ∈ B ∧ ∀x ∈ B 𝐶 ∈ 𝐷) →
⦋A / x⦌𝐶 ∈ 𝐷) |
|
Theorem | sbnfc2 2900* |
Two ways of expressing "x is (effectively) not free in A."
(Contributed by Mario Carneiro, 14-Oct-2016.)
|
⊢ (ℲxA ↔ ∀y∀z⦋y / x⦌A = ⦋z / x⦌A) |