Theorem List for New Foundations Explorer - 3101-3200 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | sbcbii 3101 |
Formula-building inference rule for class substitution. (Contributed by
NM, 11-Nov-2005.)
|
⊢ (φ
↔ ψ)
⇒ ⊢ ([̣A / x]̣φ
↔ [̣A / x]̣ψ) |
|
Theorem | sbcbiiOLD 3102 |
Formula-building inference rule for class substitution. (Contributed by
NM, 11-Nov-2005.) (New usage is discouraged.)
|
⊢ (φ
↔ ψ)
⇒ ⊢ (A ∈ V → ([̣A / x]̣φ
↔ [̣A / x]̣ψ)) |
|
Theorem | eqsbc3r 3103* |
eqsbc3 3085 with setvar variable on right side of equals
sign. This proof
was automatically generated from the virtual deduction proof eqsbc3rVD
in set.mm using a translation program. (Contributed by Alan Sare,
24-Oct-2011.)
|
⊢ (A ∈ B →
([̣A / x]̣C =
x ↔ C = A)) |
|
Theorem | sbc3ang 3104 |
Distribution of class substitution over triple conjunction.
(Contributed by NM, 14-Dec-2006.) (Proof shortened by Andrew Salmon,
29-Jun-2011.)
|
⊢ (A ∈ V →
([̣A / x]̣(φ
∧ ψ
∧ χ)
↔ ([̣A / x]̣φ
∧ [̣A / x]̣ψ
∧ [̣A / x]̣χ))) |
|
Theorem | sbcel1gv 3105* |
Class substitution into a membership relation. (Contributed by NM,
17-Nov-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|
⊢ (A ∈ V →
([̣A / x]̣x ∈ B ↔
A ∈
B)) |
|
Theorem | sbcel2gv 3106* |
Class substitution into a membership relation. (Contributed by NM,
17-Nov-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|
⊢ (B ∈ V →
([̣B / x]̣A ∈ x ↔
A ∈
B)) |
|
Theorem | sbcimdv 3107* |
Substitution analog of Theorem 19.20 of [Margaris] p. 90. (Contributed
by NM, 11-Nov-2005.)
|
⊢ (φ
→ (ψ → χ)) ⇒ ⊢ ((φ
∧ A ∈ V) →
([̣A / x]̣ψ
→ [̣A / x]̣χ)) |
|
Theorem | sbctt 3108 |
Substitution for a variable not free in a wff does not affect it.
(Contributed by Mario Carneiro, 14-Oct-2016.)
|
⊢ ((A ∈ V ∧ Ⅎxφ) → ([̣A / x]̣φ
↔ φ)) |
|
Theorem | sbcgf 3109 |
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 ∈ V →
([̣A / x]̣φ
↔ φ)) |
|
Theorem | sbc19.21g 3110 |
Substitution for a variable not free in antecedent affects only the
consequent. (Contributed by NM, 11-Oct-2004.)
|
⊢ Ⅎxφ ⇒ ⊢ (A ∈ V →
([̣A / x]̣(φ
→ ψ) ↔ (φ → [̣A / x]̣ψ))) |
|
Theorem | sbcg 3111* |
Substitution for a variable not occurring in a wff does not affect it.
Distinct variable form of sbcgf 3109. (Contributed by Alan Sare,
10-Nov-2012.)
|
⊢ (A ∈ V →
([̣A / x]̣φ
↔ φ)) |
|
Theorem | sbc2iegf 3112* |
Conversion of implicit substitution to explicit class substitution.
(Contributed by Mario Carneiro, 19-Dec-2013.)
|
⊢ Ⅎxψ
& ⊢ Ⅎyψ
& ⊢ Ⅎx
B ∈
W
& ⊢ ((x =
A ∧
y = B)
→ (φ ↔ ψ)) ⇒ ⊢ ((A ∈ V ∧ B ∈ W) →
([̣A / x]̣[̣B / y]̣φ
↔ ψ)) |
|
Theorem | sbc2ie 3113* |
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 3114* |
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 3115* |
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
& ⊢ C ∈ V
& ⊢ ((x =
A ∧
y = B
∧ z =
C) → (φ ↔ ψ)) ⇒ ⊢ ([̣A /
x]̣[̣B / y]̣[̣C / z]̣φ
↔ ψ) |
|
Theorem | sbccomlem 3116* |
Lemma for sbccom 3117. (Contributed by NM, 14-Nov-2005.) (Revised
by
Mario Carneiro, 18-Oct-2016.)
|
⊢ ([̣A /
x]̣[̣B / y]̣φ
↔ [̣B / y]̣[̣A / x]̣φ) |
|
Theorem | sbccom 3117* |
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 3118* |
Interchange class substitution and restricted quantifier. (Contributed
by NM, 1-Mar-2008.) (Revised by David Abernethy, 22-Feb-2010.)
|
⊢ ((A ∈ V ∧ ℲyA) →
([̣A / x]̣∀y ∈ B φ ↔ ∀y ∈ B
[̣A / x]̣φ)) |
|
Theorem | sbcrext 3119* |
Interchange class substitution and restricted existential quantifier.
(Contributed by NM, 1-Mar-2008.) (Proof shortened by Mario Carneiro,
13-Oct-2016.)
|
⊢ ((A ∈ V ∧ ℲyA) →
([̣A / x]̣∃y ∈ B φ ↔ ∃y ∈ B
[̣A / x]̣φ)) |
|
Theorem | sbcralg 3120* |
Interchange class substitution and restricted quantifier. (Contributed
by NM, 15-Nov-2005.) (Proof shortened by Andrew Salmon,
29-Jun-2011.)
|
⊢ (A ∈ V →
([̣A / x]̣∀y ∈ B φ ↔ ∀y ∈ B
[̣A / x]̣φ)) |
|
Theorem | sbcrexg 3121* |
Interchange class substitution and restricted existential quantifier.
(Contributed by NM, 15-Nov-2005.) (Proof shortened by Andrew Salmon,
29-Jun-2011.)
|
⊢ (A ∈ V →
([̣A / x]̣∃y ∈ B φ ↔ ∃y ∈ B
[̣A / x]̣φ)) |
|
Theorem | sbcreug 3122* |
Interchange class substitution and restricted uniqueness quantifier.
(Contributed by NM, 24-Feb-2013.)
|
⊢ (A ∈ V →
([̣A / x]̣∃!y ∈ B φ ↔ ∃!y ∈ B
[̣A / x]̣φ)) |
|
Theorem | sbcabel 3123* |
Interchange class substitution and class abstraction. (Contributed by
NM, 5-Nov-2005.)
|
⊢ ℲxB ⇒ ⊢ (A ∈ V →
([̣A / x]̣{y
∣ φ} ∈
B ↔ {y ∣
[̣A / x]̣φ}
∈ B)) |
|
Theorem | rspsbc 3124* |
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 2024 and spsbc 3058. See
also rspsbca 3125 and rspcsbela 3195. (Contributed by NM, 17-Nov-2006.)
(Proof shortened by Mario Carneiro, 13-Oct-2016.)
|
⊢ (A ∈ B →
(∀x
∈ B
φ → [̣A / x]̣φ)) |
|
Theorem | rspsbca 3125* |
Restricted quantifier version of Axiom 4 of [Mendelson] p. 69.
(Contributed by NM, 14-Dec-2005.)
|
⊢ ((A ∈ B ∧ ∀x ∈ B φ) →
[̣A / x]̣φ) |
|
Theorem | rspesbca 3126* |
Existence form of rspsbca 3125. (Contributed by NM, 29-Feb-2008.) (Proof
shortened by Mario Carneiro, 13-Oct-2016.)
|
⊢ ((A ∈ B ∧ [̣A /
x]̣φ) → ∃x ∈ B φ) |
|
Theorem | spesbc 3127 |
Existence form of spsbc 3058. (Contributed by Mario Carneiro,
18-Nov-2016.)
|
⊢ ([̣A /
x]̣φ → ∃xφ) |
|
Theorem | spesbcd 3128 |
form of spsbc 3058. (Contributed by Mario Carneiro,
9-Feb-2017.)
|
⊢ (φ
→ [̣A / x]̣ψ) ⇒ ⊢ (φ
→ ∃xψ) |
|
Theorem | sbcth2 3129* |
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 3130 |
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 1798. (Contributed by NM, 16-Jan-2004.)
|
⊢ Ⅎxφ ⇒ ⊢ (∀x ∈ A (φ →
ψ) → (φ → ∀x ∈ A ψ)) |
|
Theorem | rmo2 3131* |
Alternate definition of restricted "at most one." Note that
∃*x ∈ Aφ is
not equivalent to
∃y ∈ A∀x ∈ A(φ →
x = y) (in analogy to reu6 3025); to see
this, let A be the
empty set. However, one direction of this
pattern holds; see rmo2i 3132. (Contributed by NM, 17-Jun-2017.)
|
⊢ Ⅎyφ ⇒ ⊢ (∃*x ∈ A φ ↔
∃y∀x ∈ A (φ → x = y)) |
|
Theorem | rmo2i 3132* |
Condition implying restricted "at most one." (Contributed by NM,
17-Jun-2017.)
|
⊢ Ⅎyφ ⇒ ⊢ (∃y ∈ A ∀x ∈ A (φ →
x = y)
→ ∃*x ∈ A φ) |
|
Theorem | rmo3 3133* |
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 3134* |
Consequence of "at most one", using implicit substitution.
(Contributed
by NM, 2-Jan-2015.) (Revised by NM, 16-Jun-2017.)
|
⊢ (x =
B → (φ ↔ ψ))
& ⊢ (x =
C → (φ ↔ χ)) ⇒ ⊢ ((∃*x ∈ A φ ∧ (B ∈ A ∧ ψ))
→ (B = C ↔ (C
∈ A
∧ χ))) |
|
Theorem | rmoi 3135* |
Consequence of "at most one", using implicit substitution.
(Contributed
by NM, 4-Nov-2012.) (Revised by NM, 16-Jun-2017.)
|
⊢ (x =
B → (φ ↔ ψ))
& ⊢ (x =
C → (φ ↔ χ)) ⇒ ⊢ ((∃*x ∈ A φ ∧ (B ∈ A ∧ ψ) ∧ (C ∈ A ∧ χ))
→ B = C) |
|
2.1.9 Proper substitution of classes for sets
into classes
|
|
Syntax | csb 3136 |
Extend class notation to include the proper substitution of a class for a
set into another class.
|
class
[A / x]B |
|
Definition | df-csb 3137* |
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 3046, to prevent ambiguity. Theorem sbcel1g 3155 shows an example of
how ambiguity could arise if we didn't use distinguished brackets.
Theorem sbccsbg 3164 recreates substitution into a wff from this
definition. (Contributed by NM, 10-Nov-2005.)
|
⊢ [A /
x]B = {y ∣ [̣A /
x]̣y ∈ B} |
|
Theorem | csb2 3138* |
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 3139 |
Analog of dfsbcq 3048 for proper substitution into a class.
(Contributed
by NM, 10-Nov-2005.)
|
⊢ (A =
B → [A / x]C =
[B / x]C) |
|
Theorem | cbvcsb 3140 |
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.)
|
⊢ ℲyC & ⊢ ℲxD & ⊢ (x =
y → C = D) ⇒ ⊢ [A /
x]C = [A /
y]D |
|
Theorem | cbvcsbv 3141* |
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 = C) ⇒ ⊢ [A /
x]B = [A /
y]C |
|
Theorem | csbeq1d 3142 |
Equality deduction for proper substitution into a class. (Contributed
by NM, 3-Dec-2005.)
|
⊢ (φ
→ A = B) ⇒ ⊢ (φ
→ [A / x]C =
[B / x]C) |
|
Theorem | csbid 3143 |
Analog of sbid 1922 for proper substitution into a class.
(Contributed by
NM, 10-Nov-2005.)
|
⊢ [x /
x]A = A |
|
Theorem | csbeq1a 3144 |
Equality theorem for proper substitution into a class. (Contributed by
NM, 10-Nov-2005.)
|
⊢ (x =
A → B = [A /
x]B) |
|
Theorem | csbco 3145* |
Composition law for chained substitutions into a class. (Contributed by
NM, 10-Nov-2005.)
|
⊢ [A /
y][y / x]B =
[A / x]B |
|
Theorem | csbexg 3146 |
The existence of proper substitution into a class. (Contributed by NM,
10-Nov-2005.)
|
⊢ ((A ∈ V ∧ ∀x B ∈ W) →
[A / x]B
∈ V) |
|
Theorem | csbex 3147 |
The existence of proper substitution into a class. (Contributed by NM,
7-Aug-2007.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|
⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ [A /
x]B ∈
V |
|
Theorem | csbtt 3148 |
Substitution doesn't affect a constant B (in which x is not
free). (Contributed by Mario Carneiro, 14-Oct-2016.)
|
⊢ ((A ∈ V ∧ ℲxB) →
[A / x]B =
B) |
|
Theorem | csbconstgf 3149 |
Substitution doesn't affect a constant B (in which x is not
free). (Contributed by NM, 10-Nov-2005.)
|
⊢ ℲxB ⇒ ⊢ (A ∈ V →
[A / x]B =
B) |
|
Theorem | csbconstg 3150* |
Substitution doesn't affect a constant B (in which x is not
free). csbconstgf 3149 with distinct variable requirement.
(Contributed by
Alan Sare, 22-Jul-2012.)
|
⊢ (A ∈ V →
[A / x]B =
B) |
|
Theorem | sbcel12g 3151 |
Distribute proper substitution through a membership relation.
(Contributed by NM, 10-Nov-2005.) (Proof shortened by Andrew Salmon,
29-Jun-2011.)
|
⊢ (A ∈ V →
([̣A / x]̣B ∈ C ↔
[A / x]B
∈ [A / x]C)) |
|
Theorem | sbceqg 3152 |
Distribute proper substitution through an equality relation.
(Contributed by NM, 10-Nov-2005.) (Proof shortened by Andrew Salmon,
29-Jun-2011.)
|
⊢ (A ∈ V →
([̣A / x]̣B =
C ↔ [A / x]B =
[A / x]C)) |
|
Theorem | sbcnel12g 3153 |
Distribute proper substitution through negated membership. (Contributed
by Andrew Salmon, 18-Jun-2011.)
|
⊢ (A ∈ V →
([̣A / x]̣B ∉ C ↔
[A / x]B
∉ [A / x]C)) |
|
Theorem | sbcne12g 3154 |
Distribute proper substitution through an inequality. (Contributed by
Andrew Salmon, 18-Jun-2011.)
|
⊢ (A ∈ V →
([̣A / x]̣B ≠
C ↔ [A / x]B ≠
[A / x]C)) |
|
Theorem | sbcel1g 3155* |
Move proper substitution in and out of a membership relation. Note that
the scope of [̣A /
x]̣ is the wff B ∈ C, whereas the scope
of [A / x] is the class B. (Contributed by NM,
10-Nov-2005.)
|
⊢ (A ∈ V →
([̣A / x]̣B ∈ C ↔
[A / x]B
∈ C)) |
|
Theorem | sbceq1g 3156* |
Move proper substitution to first argument of an equality. (Contributed
by NM, 30-Nov-2005.)
|
⊢ (A ∈ V →
([̣A / x]̣B =
C ↔ [A / x]B =
C)) |
|
Theorem | sbcel2g 3157* |
Move proper substitution in and out of a membership relation.
(Contributed by NM, 14-Nov-2005.)
|
⊢ (A ∈ V →
([̣A / x]̣B ∈ C ↔
B ∈
[A / x]C)) |
|
Theorem | sbceq2g 3158* |
Move proper substitution to second argument of an equality.
(Contributed by NM, 30-Nov-2005.)
|
⊢ (A ∈ V →
([̣A / x]̣B =
C ↔ B = [A /
x]C)) |
|
Theorem | csbcomg 3159* |
Commutative law for double substitution into a class. (Contributed by
NM, 14-Nov-2005.)
|
⊢ ((A ∈ V ∧ B ∈ W) →
[A / x][B / y]C =
[B / y][A / x]C) |
|
Theorem | csbeq2d 3160 |
Formula-building deduction rule for class substitution. (Contributed by
NM, 22-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
|
⊢ Ⅎxφ
& ⊢ (φ
→ B = C) ⇒ ⊢ (φ
→ [A / x]B =
[A / x]C) |
|
Theorem | csbeq2dv 3161* |
Formula-building deduction rule for class substitution. (Contributed by
NM, 10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
|
⊢ (φ
→ B = C) ⇒ ⊢ (φ
→ [A / x]B =
[A / x]C) |
|
Theorem | csbeq2i 3162 |
Formula-building inference rule for class substitution. (Contributed by
NM, 10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
|
⊢ B =
C ⇒ ⊢ [A /
x]B = [A /
x]C |
|
Theorem | csbvarg 3163 |
The proper substitution of a class for setvar variable results in the
class (if the class exists). (Contributed by NM, 10-Nov-2005.)
|
⊢ (A ∈ V →
[A / x]x =
A) |
|
Theorem | sbccsbg 3164* |
Substitution into a wff expressed in terms of substitution into a
class. (Contributed by NM, 15-Aug-2007.)
|
⊢ (A ∈ V →
([̣A / x]̣φ
↔ y ∈ [A /
x]{y ∣ φ})) |
|
Theorem | sbccsb2g 3165 |
Substitution into a wff expressed in using substitution into a class.
(Contributed by NM, 27-Nov-2005.)
|
⊢ (A ∈ V →
([̣A / x]̣φ
↔ A ∈ [A /
x]{x ∣ φ})) |
|
Theorem | nfcsb1d 3166 |
Bound-variable hypothesis builder for substitution into a class.
(Contributed by Mario Carneiro, 12-Oct-2016.)
|
⊢ (φ
→ ℲxA) ⇒ ⊢ (φ
→ Ⅎx[A / x]B) |
|
Theorem | nfcsb1 3167 |
Bound-variable hypothesis builder for substitution into a class.
(Contributed by Mario Carneiro, 12-Oct-2016.)
|
⊢ ℲxA ⇒ ⊢ Ⅎx[A /
x]B |
|
Theorem | nfcsb1v 3168* |
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 3169 |
Deduction version of nfcsb 3170. (Contributed by NM, 21-Nov-2005.)
(Revised by Mario Carneiro, 12-Oct-2016.)
|
⊢ Ⅎyφ
& ⊢ (φ
→ ℲxA)
& ⊢ (φ
→ ℲxB) ⇒ ⊢ (φ
→ Ⅎx[A / y]B) |
|
Theorem | nfcsb 3170 |
Bound-variable hypothesis builder for substitution into a class.
(Contributed by Mario Carneiro, 12-Oct-2016.)
|
⊢ ℲxA & ⊢ ℲxB ⇒ ⊢ Ⅎx[A /
y]B |
|
Theorem | csbhypf 3171* |
Introduce an explicit substitution into an implicit substitution
hypothesis. See sbhypf 2904 for class substitution version. (Contributed
by NM, 19-Dec-2008.)
|
⊢ ℲxA & ⊢ ℲxC & ⊢ (x =
A → B = C) ⇒ ⊢ (y =
A → [y / x]B =
C) |
|
Theorem | csbiebt 3172* |
Conversion of implicit substitution to explicit substitution into a
class. (Closed theorem version of csbiegf 3176.) (Contributed by NM,
11-Nov-2005.)
|
⊢ ((A ∈ V ∧ ℲxC) →
(∀x(x = A → B =
C) ↔ [A / x]B =
C)) |
|
Theorem | csbiedf 3173* |
Conversion of implicit substitution to explicit substitution into a
class. (Contributed by Mario Carneiro, 13-Oct-2016.)
|
⊢ Ⅎxφ
& ⊢ (φ
→ ℲxC)
& ⊢ (φ
→ A ∈ V)
& ⊢ ((φ
∧ x =
A) → B = C) ⇒ ⊢ (φ
→ [A / x]B =
C) |
|
Theorem | csbieb 3174* |
Bidirectional conversion between an implicit class substitution
hypothesis x = A → B =
C and its explicit substitution
equivalent.
(Contributed by NM, 2-Mar-2008.)
|
⊢ A ∈ V
& ⊢ ℲxC ⇒ ⊢ (∀x(x = A → B =
C) ↔ [A / x]B =
C) |
|
Theorem | csbiebg 3175* |
Bidirectional conversion between an implicit class substitution
hypothesis x = A → B =
C and its explicit substitution
equivalent.
(Contributed by NM, 24-Mar-2013.) (Revised by Mario Carneiro,
11-Dec-2016.)
|
⊢ ℲxC ⇒ ⊢ (A ∈ V →
(∀x(x = A → B =
C) ↔ [A / x]B =
C)) |
|
Theorem | csbiegf 3176* |
Conversion of implicit substitution to explicit substitution into a
class. (Contributed by NM, 11-Nov-2005.) (Revised by Mario Carneiro,
13-Oct-2016.)
|
⊢ (A ∈ V →
ℲxC)
& ⊢ (x =
A → B = C) ⇒ ⊢ (A ∈ V →
[A / x]B =
C) |
|
Theorem | csbief 3177* |
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
& ⊢ ℲxC & ⊢ (x =
A → B = C) ⇒ ⊢ [A /
x]B = C |
|
Theorem | csbied 3178* |
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 ∈ V)
& ⊢ ((φ
∧ x =
A) → B = C) ⇒ ⊢ (φ
→ [A / x]B =
C) |
|
Theorem | csbied2 3179* |
Conversion of implicit substitution to explicit class substitution,
deduction form. (Contributed by Mario Carneiro, 2-Jan-2017.)
|
⊢ (φ
→ A ∈ V)
& ⊢ (φ
→ A = B)
& ⊢ ((φ
∧ x =
B) → C = D) ⇒ ⊢ (φ
→ [A / x]C =
D) |
|
Theorem | csbie2t 3180* |
Conversion of implicit substitution to explicit substitution into a
class (closed form of csbie2 3181). (Contributed by NM, 3-Sep-2007.)
(Revised by Mario Carneiro, 13-Oct-2016.)
|
⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (∀x∀y((x = A ∧ y = B) →
C = D)
→ [A / x][B / y]C =
D) |
|
Theorem | csbie2 3181* |
Conversion of implicit substitution to explicit substitution into a
class. (Contributed by NM, 27-Aug-2007.)
|
⊢ A ∈ V
& ⊢ B ∈ V
& ⊢ ((x =
A ∧
y = B)
→ C = D) ⇒ ⊢ [A /
x][B / y]C =
D |
|
Theorem | csbie2g 3182* |
Conversion of implicit substitution to explicit class substitution.
This version of sbcie 3080 avoids a disjointness condition on x, A by
substituting twice. (Contributed by Mario Carneiro, 11-Nov-2016.)
|
⊢ (x =
y → B = C)
& ⊢ (y =
A → C = D) ⇒ ⊢ (A ∈ V →
[A / x]B =
D) |
|
Theorem | sbcnestgf 3183 |
Nest the composition of two substitutions. (Contributed by Mario
Carneiro, 11-Nov-2016.)
|
⊢ ((A ∈ V ∧ ∀yℲxφ) → ([̣A / x]̣[̣B / y]̣φ
↔ [̣[A / x]B /
y]̣φ)) |
|
Theorem | csbnestgf 3184 |
Nest the composition of two substitutions. (Contributed by NM,
23-Nov-2005.) (Proof shortened by Mario Carneiro, 10-Nov-2016.)
|
⊢ ((A ∈ V ∧ ∀yℲxC) →
[A / x][B / y]C =
[[A / x]B /
y]C) |
|
Theorem | sbcnestg 3185* |
Nest the composition of two substitutions. (Contributed by NM,
27-Nov-2005.) (Proof shortened by Mario Carneiro, 11-Nov-2016.)
|
⊢ (A ∈ V →
([̣A / x]̣[̣B / y]̣φ
↔ [̣[A / x]B /
y]̣φ)) |
|
Theorem | csbnestg 3186* |
Nest the composition of two substitutions. (Contributed by NM,
23-Nov-2005.) (Proof shortened by Mario Carneiro, 10-Nov-2016.)
|
⊢ (A ∈ V →
[A / x][B / y]C =
[[A / x]B /
y]C) |
|
Theorem | csbnestgOLD 3187* |
Nest the composition of two substitutions. (New usage is discouraged.)
(Contributed by NM, 23-Nov-2005.)
|
⊢ ((A ∈ V ∧ ∀x B ∈ W) →
[A / x][B / y]C =
[[A / x]B /
y]C) |
|
Theorem | csbnest1g 3188 |
Nest the composition of two substitutions. (Contributed by NM,
23-May-2006.) (Proof shortened by Mario Carneiro, 11-Nov-2016.)
|
⊢ (A ∈ V →
[A / x][B / x]C =
[[A / x]B /
x]C) |
|
Theorem | csbnest1gOLD 3189* |
Nest the composition of two substitutions. Obsolete as of 11-Nov-2016.
(Contributed by NM, 23-May-2006.) (New usage is discouraged.)
|
⊢ ((A ∈ V ∧ ∀x B ∈ W) →
[A / x][B / x]C =
[[A / x]B /
x]C) |
|
Theorem | csbidmg 3190* |
Idempotent law for class substitutions. (Contributed by NM,
1-Mar-2008.)
|
⊢ (A ∈ V →
[A / x][A / x]B =
[A / x]B) |
|
Theorem | sbcco3g 3191* |
Composition of two substitutions. (Contributed by NM, 27-Nov-2005.)
(Revised by Mario Carneiro, 11-Nov-2016.)
|
⊢ (x =
A → B = C) ⇒ ⊢ (A ∈ V →
([̣A / x]̣[̣B / y]̣φ
↔ [̣C / y]̣φ)) |
|
Theorem | sbcco3gOLD 3192* |
Composition of two substitutions. (Contributed by NM, 27-Nov-2005.)
(New usage is discouraged.)
|
⊢ (x =
A → B = C) ⇒ ⊢ ((A ∈ V ∧ ∀x B ∈ W) →
([̣A / x]̣[̣B / y]̣φ
↔ [̣C / y]̣φ)) |
|
Theorem | csbco3g 3193* |
Composition of two class substitutions. (Contributed by NM,
27-Nov-2005.) (Revised by Mario Carneiro, 11-Nov-2016.)
|
⊢ (x =
A → B = C) ⇒ ⊢ (A ∈ V →
[A / x][B / y]D =
[C / y]D) |
|
Theorem | csbco3gOLD 3194* |
Composition of two class substitutions. Obsolete as of 11-Nov-2016.
(Contributed by NM, 27-Nov-2005.) (New usage is discouraged.)
|
⊢ (x =
A → B = D) ⇒ ⊢ ((A ∈ V ∧ ∀x B ∈ W) →
[A / x][B / y]C =
[D / y]C) |
|
Theorem | rspcsbela 3195* |
Special case related to rspsbc 3124. (Contributed by NM, 10-Dec-2005.)
(Proof shortened by Eric Schmidt, 17-Jan-2007.)
|
⊢ ((A ∈ B ∧ ∀x ∈ B C ∈ D) →
[A / x]C
∈ D) |
|
Theorem | sbnfc2 3196* |
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) |
|
Theorem | csbabg 3197* |
Move substitution into a class abstraction. (Contributed by NM,
13-Dec-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|
⊢ (A ∈ V →
[A / x]{y
∣ φ} = {y
∣ [̣A / x]̣φ}) |
|
Theorem | cbvralcsf 3198 |
A more general version of cbvralf 2829 that doesn't require A and B
to be distinct from x
or y. Changes bound
variables using
implicit substitution. (Contributed by Andrew Salmon, 13-Jul-2011.)
|
⊢ ℲyA & ⊢ ℲxB & ⊢ Ⅎyφ
& ⊢ Ⅎxψ
& ⊢ (x =
y → A = B)
& ⊢ (x =
y → (φ ↔ ψ)) ⇒ ⊢ (∀x ∈ A φ ↔
∀y
∈ B
ψ) |
|
Theorem | cbvrexcsf 3199 |
A more general version of cbvrexf 2830 that has no distinct variable
restrictions. Changes bound variables using implicit substitution.
(Contributed by Andrew Salmon, 13-Jul-2011.) (Proof shortened by Mario
Carneiro, 7-Dec-2014.)
|
⊢ ℲyA & ⊢ ℲxB & ⊢ Ⅎyφ
& ⊢ Ⅎxψ
& ⊢ (x =
y → A = B)
& ⊢ (x =
y → (φ ↔ ψ)) ⇒ ⊢ (∃x ∈ A φ ↔
∃y
∈ B
ψ) |
|
Theorem | cbvreucsf 3200 |
A more general version of cbvreuv 2837 that has no distinct variable
rextrictions. Changes bound variables using implicit substitution.
(Contributed by Andrew Salmon, 13-Jul-2011.)
|
⊢ ℲyA & ⊢ ℲxB & ⊢ Ⅎyφ
& ⊢ Ⅎxψ
& ⊢ (x =
y → A = B)
& ⊢ (x =
y → (φ ↔ ψ)) ⇒ ⊢ (∃!x ∈ A φ ↔
∃!y
∈ B
ψ) |