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