Theorem List for Intuitionistic Logic Explorer - 2901-3000 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | sbcim1 2901 |
Distribution of class substitution over implication. One direction of
sbcimg 2894 that holds for proper classes. (Contributed
by NM,
17-Aug-2018.)
|
⊢ ([𝐴 / 𝑥](𝜑 → 𝜓) → ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜓)) |
|
Theorem | sbcbi1 2902 |
Distribution of class substitution over biconditional. One direction of
sbcbig 2899 that holds for proper classes. (Contributed
by NM,
17-Aug-2018.)
|
⊢ ([𝐴 / 𝑥](𝜑 ↔ 𝜓) → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)) |
|
Theorem | sbcbi2 2903 |
Substituting into equivalent wff's gives equivalent results. (Contributed
by Giovanni Mascellani, 9-Apr-2018.)
|
⊢ (∀𝑥(𝜑 ↔ 𝜓) → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)) |
|
Theorem | sbcal 2904* |
Move universal quantifier in and out of class substitution.
(Contributed by NM, 31-Dec-2016.)
|
⊢ ([𝐴 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝐴 / 𝑦]𝜑) |
|
Theorem | sbcalg 2905* |
Move universal quantifier in and out of class substitution.
(Contributed by NM, 16-Jan-2004.)
|
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝐴 / 𝑦]𝜑)) |
|
Theorem | sbcex2 2906* |
Move existential quantifier in and out of class substitution.
(Contributed by NM, 21-May-2004.)
|
⊢ ([𝐴 / 𝑦]∃𝑥𝜑 ↔ ∃𝑥[𝐴 / 𝑦]𝜑) |
|
Theorem | sbcexg 2907* |
Move existential quantifier in and out of class substitution.
(Contributed by NM, 21-May-2004.)
|
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑦]∃𝑥𝜑 ↔ ∃𝑥[𝐴 / 𝑦]𝜑)) |
|
Theorem | sbceqal 2908* |
A variation of extensionality for classes. (Contributed by Andrew
Salmon, 28-Jun-2011.)
|
⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝑥 = 𝐵) → 𝐴 = 𝐵)) |
|
Theorem | sbeqalb 2909* |
Theorem *14.121 in [WhiteheadRussell]
p. 185. (Contributed by Andrew
Salmon, 28-Jun-2011.) (Proof shortened by Wolf Lammen, 9-May-2013.)
|
⊢ (𝐴 ∈ 𝑉 → ((∀𝑥(𝜑 ↔ 𝑥 = 𝐴) ∧ ∀𝑥(𝜑 ↔ 𝑥 = 𝐵)) → 𝐴 = 𝐵)) |
|
Theorem | sbcbid 2910 |
Formula-building deduction for class substitution. (Contributed by NM,
29-Dec-2014.)
|
⊢ Ⅎ𝑥𝜑
& ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐴 / 𝑥]𝜒)) |
|
Theorem | sbcbidv 2911* |
Formula-building deduction for class substitution. (Contributed by NM,
29-Dec-2014.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐴 / 𝑥]𝜒)) |
|
Theorem | sbcbii 2912 |
Formula-building inference for class substitution. (Contributed by NM,
11-Nov-2005.)
|
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓) |
|
Theorem | eqsbc3r 2913* |
eqsbc3 2892 with setvar variable on right side of equals
sign.
(Contributed by Alan Sare, 24-Oct-2011.) (Proof shortened by JJ,
7-Jul-2021.)
|
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝑥 ↔ 𝐵 = 𝐴)) |
|
Theorem | sbc3an 2914 |
Distribution of class substitution over triple conjunction. (Contributed
by NM, 14-Dec-2006.) (Revised by NM, 17-Aug-2018.)
|
⊢ ([𝐴 / 𝑥](𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓 ∧ [𝐴 / 𝑥]𝜒)) |
|
Theorem | sbcel1v 2915* |
Class substitution into a membership relation. (Contributed by NM,
17-Aug-2018.)
|
⊢ ([𝐴 / 𝑥]𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵) |
|
Theorem | sbcel2gv 2916* |
Class substitution into a membership relation. (Contributed by NM,
17-Nov-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|
⊢ (𝐵 ∈ 𝑉 → ([𝐵 / 𝑥]𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐵)) |
|
Theorem | sbcel21v 2917* |
Class substitution into a membership relation. One direction of
sbcel2gv 2916 that holds for proper classes. (Contributed
by NM,
17-Aug-2018.)
|
⊢ ([𝐵 / 𝑥]𝐴 ∈ 𝑥 → 𝐴 ∈ 𝐵) |
|
Theorem | sbcimdv 2918* |
Substitution analogue of Theorem 19.20 of [Margaris] p. 90 (alim 1398).
(Contributed by NM, 11-Nov-2005.) (Revised by NM, 17-Aug-2018.) (Proof
shortened by JJ, 7-Jul-2021.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)) |
|
Theorem | sbctt 2919 |
Substitution for a variable not free in a wff does not affect it.
(Contributed by Mario Carneiro, 14-Oct-2016.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ Ⅎ𝑥𝜑) → ([𝐴 / 𝑥]𝜑 ↔ 𝜑)) |
|
Theorem | sbcgf 2920 |
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 2921 |
Substitution for a variable not free in antecedent affects only the
consequent. (Contributed by NM, 11-Oct-2004.)
|
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → [𝐴 / 𝑥]𝜓))) |
|
Theorem | sbcg 2922* |
Substitution for a variable not occurring in a wff does not affect it.
Distinct variable form of sbcgf 2920. (Contributed by Alan Sare,
10-Nov-2012.)
|
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜑)) |
|
Theorem | sbc2iegf 2923* |
Conversion of implicit substitution to explicit class substitution.
(Contributed by Mario Carneiro, 19-Dec-2013.)
|
⊢ Ⅎ𝑥𝜓
& ⊢ Ⅎ𝑦𝜓
& ⊢ Ⅎ𝑥 𝐵 ∈ 𝑊
& ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ 𝜓)) |
|
Theorem | sbc2ie 2924* |
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 2925* |
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 2926* |
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 2927* |
Lemma for sbccom 2928. (Contributed by NM, 14-Nov-2005.) (Revised
by
Mario Carneiro, 18-Oct-2016.)
|
⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [𝐵 / 𝑦][𝐴 / 𝑥]𝜑) |
|
Theorem | sbccom 2928* |
Commutative law for double class substitution. (Contributed by NM,
15-Nov-2005.) (Proof shortened by Mario Carneiro, 18-Oct-2016.)
|
⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [𝐵 / 𝑦][𝐴 / 𝑥]𝜑) |
|
Theorem | sbcralt 2929* |
Interchange class substitution and restricted quantifier. (Contributed
by NM, 1-Mar-2008.) (Revised by David Abernethy, 22-Feb-2010.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ Ⅎ𝑦𝐴) → ([𝐴 / 𝑥]∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑)) |
|
Theorem | sbcrext 2930* |
Interchange class substitution and restricted existential quantifier.
(Contributed by NM, 1-Mar-2008.) (Proof shortened by Mario Carneiro,
13-Oct-2016.)
|
⊢ (Ⅎ𝑦𝐴 → ([𝐴 / 𝑥]∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑)) |
|
Theorem | sbcralg 2931* |
Interchange class substitution and restricted quantifier. (Contributed
by NM, 15-Nov-2005.) (Proof shortened by Andrew Salmon,
29-Jun-2011.)
|
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑)) |
|
Theorem | sbcrex 2932* |
Interchange class substitution and restricted existential quantifier.
(Contributed by NM, 15-Nov-2005.) (Revised by NM, 18-Aug-2018.)
|
⊢ ([𝐴 / 𝑥]∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑) |
|
Theorem | sbcreug 2933* |
Interchange class substitution and restricted unique existential
quantifier. (Contributed by NM, 24-Feb-2013.)
|
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]∃!𝑦 ∈ 𝐵 𝜑 ↔ ∃!𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑)) |
|
Theorem | sbcabel 2934* |
Interchange class substitution and class abstraction. (Contributed by
NM, 5-Nov-2005.)
|
⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]{𝑦 ∣ 𝜑} ∈ 𝐵 ↔ {𝑦 ∣ [𝐴 / 𝑥]𝜑} ∈ 𝐵)) |
|
Theorem | rspsbc 2935* |
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 1712 and spsbc 2865. See
also rspsbca 2936 and rspcsbela . (Contributed by NM,
17-Nov-2006.)
(Proof shortened by Mario Carneiro, 13-Oct-2016.)
|
⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → [𝐴 / 𝑥]𝜑)) |
|
Theorem | rspsbca 2936* |
Restricted quantifier version of Axiom 4 of [Mendelson] p. 69.
(Contributed by NM, 14-Dec-2005.)
|
⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝜑) → [𝐴 / 𝑥]𝜑) |
|
Theorem | rspesbca 2937* |
Existence form of rspsbca 2936. (Contributed by NM, 29-Feb-2008.) (Proof
shortened by Mario Carneiro, 13-Oct-2016.)
|
⊢ ((𝐴 ∈ 𝐵 ∧ [𝐴 / 𝑥]𝜑) → ∃𝑥 ∈ 𝐵 𝜑) |
|
Theorem | spesbc 2938 |
Existence form of spsbc 2865. (Contributed by Mario Carneiro,
18-Nov-2016.)
|
⊢ ([𝐴 / 𝑥]𝜑 → ∃𝑥𝜑) |
|
Theorem | spesbcd 2939 |
form of spsbc 2865. (Contributed by Mario Carneiro,
9-Feb-2017.)
|
⊢ (𝜑 → [𝐴 / 𝑥]𝜓) ⇒ ⊢ (𝜑 → ∃𝑥𝜓) |
|
Theorem | sbcth2 2940* |
A substitution into a theorem. (Contributed by NM, 1-Mar-2008.) (Proof
shortened by Mario Carneiro, 13-Oct-2016.)
|
⊢ (𝑥 ∈ 𝐵 → 𝜑) ⇒ ⊢ (𝐴 ∈ 𝐵 → [𝐴 / 𝑥]𝜑) |
|
Theorem | ra5 2941 |
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 1528. (Contributed by NM, 16-Jan-2004.)
|
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)) |
|
Theorem | rmo2ilem 2942* |
Condition implying restricted at-most-one quantifier. (Contributed by
Jim Kingdon, 14-Jul-2018.)
|
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃𝑦∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦) → ∃*𝑥 ∈ 𝐴 𝜑) |
|
Theorem | rmo2i 2943* |
Condition implying restricted at-most-one quantifier. (Contributed by
NM, 17-Jun-2017.)
|
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦) → ∃*𝑥 ∈ 𝐴 𝜑) |
|
Theorem | rmo3 2944* |
Restricted at-most-one quantifier using explicit substitution.
(Contributed by NM, 4-Nov-2012.) (Revised by NM, 16-Jun-2017.)
|
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) |
|
Theorem | rmob 2945* |
Consequence of "at most one", using implicit substitution.
(Contributed
by NM, 2-Jan-2015.) (Revised by NM, 16-Jun-2017.)
|
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜒)) ⇒ ⊢ ((∃*𝑥 ∈ 𝐴 𝜑 ∧ (𝐵 ∈ 𝐴 ∧ 𝜓)) → (𝐵 = 𝐶 ↔ (𝐶 ∈ 𝐴 ∧ 𝜒))) |
|
Theorem | rmoi 2946* |
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 2947 |
Extend class notation to include the proper substitution of a class for a
set into another class.
|
class ⦋𝐴 / 𝑥⦌𝐵 |
|
Definition | df-csb 2948* |
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 2854, to prevent ambiguity. Theorem sbcel1g 2964 shows an example of
how ambiguity could arise if we didn't use distinguished brackets.
Theorem sbccsbg 2973 recreates substitution into a wff from this
definition. (Contributed by NM, 10-Nov-2005.)
|
⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} |
|
Theorem | csb2 2949* |
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 2950 |
Analog of dfsbcq 2856 for proper substitution into a class.
(Contributed
by NM, 10-Nov-2005.)
|
⊢ (𝐴 = 𝐵 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶) |
|
Theorem | cbvcsb 2951 |
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 2952* |
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 2953 |
Equality deduction for proper substitution into a class. (Contributed
by NM, 3-Dec-2005.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶) |
|
Theorem | csbid 2954 |
Analog of sbid 1711 for proper substitution into a class.
(Contributed by
NM, 10-Nov-2005.)
|
⊢ ⦋𝑥 / 𝑥⦌𝐴 = 𝐴 |
|
Theorem | csbeq1a 2955 |
Equality theorem for proper substitution into a class. (Contributed by
NM, 10-Nov-2005.)
|
⊢ (𝑥 = 𝐴 → 𝐵 = ⦋𝐴 / 𝑥⦌𝐵) |
|
Theorem | csbco 2956* |
Composition law for chained substitutions into a class. (Contributed by
NM, 10-Nov-2005.)
|
⊢ ⦋𝐴 / 𝑦⦌⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵 |
|
Theorem | csbtt 2957 |
Substitution doesn't affect a constant 𝐵 (in which 𝑥 is not
free). (Contributed by Mario Carneiro, 14-Oct-2016.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ Ⅎ𝑥𝐵) → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵) |
|
Theorem | csbconstgf 2958 |
Substitution doesn't affect a constant 𝐵 (in which 𝑥 is not
free). (Contributed by NM, 10-Nov-2005.)
|
⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵) |
|
Theorem | csbconstg 2959* |
Substitution doesn't affect a constant 𝐵 (in which 𝑥 is not
free). csbconstgf 2958 with distinct variable requirement.
(Contributed by
Alan Sare, 22-Jul-2012.)
|
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵) |
|
Theorem | sbcel12g 2960 |
Distribute proper substitution through a membership relation.
(Contributed by NM, 10-Nov-2005.) (Proof shortened by Andrew Salmon,
29-Jun-2011.)
|
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 ∈ 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 ∈ ⦋𝐴 / 𝑥⦌𝐶)) |
|
Theorem | sbceqg 2961 |
Distribute proper substitution through an equality relation.
(Contributed by NM, 10-Nov-2005.) (Proof shortened by Andrew Salmon,
29-Jun-2011.)
|
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)) |
|
Theorem | sbcnel12g 2962 |
Distribute proper substitution through negated membership. (Contributed
by Andrew Salmon, 18-Jun-2011.)
|
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 ∉ 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 ∉ ⦋𝐴 / 𝑥⦌𝐶)) |
|
Theorem | sbcne12g 2963 |
Distribute proper substitution through an inequality. (Contributed by
Andrew Salmon, 18-Jun-2011.)
|
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 ≠ 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 ≠ ⦋𝐴 / 𝑥⦌𝐶)) |
|
Theorem | sbcel1g 2964* |
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 2965* |
Move proper substitution to first argument of an equality. (Contributed
by NM, 30-Nov-2005.)
|
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)) |
|
Theorem | sbcel2g 2966* |
Move proper substitution in and out of a membership relation.
(Contributed by NM, 14-Nov-2005.)
|
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 ∈ 𝐶 ↔ 𝐵 ∈ ⦋𝐴 / 𝑥⦌𝐶)) |
|
Theorem | sbceq2g 2967* |
Move proper substitution to second argument of an equality.
(Contributed by NM, 30-Nov-2005.)
|
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ 𝐵 = ⦋𝐴 / 𝑥⦌𝐶)) |
|
Theorem | csbcomg 2968* |
Commutative law for double substitution into a class. (Contributed by
NM, 14-Nov-2005.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = ⦋𝐵 / 𝑦⦌⦋𝐴 / 𝑥⦌𝐶) |
|
Theorem | csbeq2d 2969 |
Formula-building deduction for class substitution. (Contributed by NM,
22-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
|
⊢ Ⅎ𝑥𝜑
& ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶) |
|
Theorem | csbeq2dv 2970* |
Formula-building deduction for class substitution. (Contributed by NM,
10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
|
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶) |
|
Theorem | csbeq2i 2971 |
Formula-building inference for class substitution. (Contributed by NM,
10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
|
⊢ 𝐵 = 𝐶 ⇒ ⊢ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶 |
|
Theorem | csbvarg 2972 |
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 2973* |
Substitution into a wff expressed in terms of substitution into a class.
(Contributed by NM, 15-Aug-2007.)
|
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝜑})) |
|
Theorem | sbccsb2g 2974 |
Substitution into a wff expressed in using substitution into a class.
(Contributed by NM, 27-Nov-2005.)
|
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ ⦋𝐴 / 𝑥⦌{𝑥 ∣ 𝜑})) |
|
Theorem | nfcsb1d 2975 |
Bound-variable hypothesis builder for substitution into a class.
(Contributed by Mario Carneiro, 12-Oct-2016.)
|
⊢ (𝜑 → Ⅎ𝑥𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵) |
|
Theorem | nfcsb1 2976 |
Bound-variable hypothesis builder for substitution into a class.
(Contributed by Mario Carneiro, 12-Oct-2016.)
|
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵 |
|
Theorem | nfcsb1v 2977* |
Bound-variable hypothesis builder for substitution into a class.
(Contributed by NM, 17-Aug-2006.) (Revised by Mario Carneiro,
12-Oct-2016.)
|
⊢ Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵 |
|
Theorem | nfcsbd 2978 |
Deduction version of nfcsb 2979. (Contributed by NM, 21-Nov-2005.)
(Revised by Mario Carneiro, 12-Oct-2016.)
|
⊢ Ⅎ𝑦𝜑
& ⊢ (𝜑 → Ⅎ𝑥𝐴)
& ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵) |
|
Theorem | nfcsb 2979 |
Bound-variable hypothesis builder for substitution into a class.
(Contributed by Mario Carneiro, 12-Oct-2016.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵 |
|
Theorem | csbhypf 2980* |
Introduce an explicit substitution into an implicit substitution
hypothesis. See sbhypf 2682 for class substitution version. (Contributed
by NM, 19-Dec-2008.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝐶
& ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = 𝐶) |
|
Theorem | csbiebt 2981* |
Conversion of implicit substitution to explicit substitution into a
class. (Closed theorem version of csbiegf 2985.) (Contributed by NM,
11-Nov-2005.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ Ⅎ𝑥𝐶) → (∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)) |
|
Theorem | csbiedf 2982* |
Conversion of implicit substitution to explicit substitution into a
class. (Contributed by Mario Carneiro, 13-Oct-2016.)
|
⊢ Ⅎ𝑥𝜑
& ⊢ (𝜑 → Ⅎ𝑥𝐶)
& ⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶) |
|
Theorem | csbieb 2983* |
Bidirectional conversion between an implicit class substitution
hypothesis 𝑥 = 𝐴 → 𝐵 = 𝐶 and its explicit substitution
equivalent.
(Contributed by NM, 2-Mar-2008.)
|
⊢ 𝐴 ∈ V & ⊢
Ⅎ𝑥𝐶 ⇒ ⊢ (∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶) |
|
Theorem | csbiebg 2984* |
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 2985* |
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 2986* |
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 | csbie 2987* |
Conversion of implicit substitution to explicit substitution into a
class. (Contributed by AV, 2-Dec-2019.)
|
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶 |
|
Theorem | csbied 2988* |
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 2989* |
Conversion of implicit substitution to explicit class substitution,
deduction form. (Contributed by Mario Carneiro, 2-Jan-2017.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐶 = 𝐷) |
|
Theorem | csbie2t 2990* |
Conversion of implicit substitution to explicit substitution into a
class (closed form of csbie2 2991). (Contributed by NM, 3-Sep-2007.)
(Revised by Mario Carneiro, 13-Oct-2016.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝐶 = 𝐷) → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = 𝐷) |
|
Theorem | csbie2 2991* |
Conversion of implicit substitution to explicit substitution into a
class. (Contributed by NM, 27-Aug-2007.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝐶 = 𝐷) ⇒ ⊢ ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = 𝐷 |
|
Theorem | csbie2g 2992* |
Conversion of implicit substitution to explicit class substitution.
This version of sbcie 2887 avoids a disjointness condition on 𝑥 and
𝐴 by substituting twice. (Contributed
by Mario Carneiro,
11-Nov-2016.)
|
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
& ⊢ (𝑦 = 𝐴 → 𝐶 = 𝐷) ⇒ ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐷) |
|
Theorem | sbcnestgf 2993 |
Nest the composition of two substitutions. (Contributed by Mario
Carneiro, 11-Nov-2016.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑦Ⅎ𝑥𝜑) → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦]𝜑)) |
|
Theorem | csbnestgf 2994 |
Nest the composition of two substitutions. (Contributed by NM,
23-Nov-2005.) (Proof shortened by Mario Carneiro, 10-Nov-2016.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑦Ⅎ𝑥𝐶) → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = ⦋⦋𝐴 / 𝑥⦌𝐵 / 𝑦⦌𝐶) |
|
Theorem | sbcnestg 2995* |
Nest the composition of two substitutions. (Contributed by NM,
27-Nov-2005.) (Proof shortened by Mario Carneiro, 11-Nov-2016.)
|
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦]𝜑)) |
|
Theorem | csbnestg 2996* |
Nest the composition of two substitutions. (Contributed by NM,
23-Nov-2005.) (Proof shortened by Mario Carneiro, 10-Nov-2016.)
|
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = ⦋⦋𝐴 / 𝑥⦌𝐵 / 𝑦⦌𝐶) |
|
Theorem | csbnest1g 2997 |
Nest the composition of two substitutions. (Contributed by NM,
23-May-2006.) (Proof shortened by Mario Carneiro, 11-Nov-2016.)
|
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑥⦌𝐶 = ⦋⦋𝐴 / 𝑥⦌𝐵 / 𝑥⦌𝐶) |
|
Theorem | csbidmg 2998* |
Idempotent law for class substitutions. (Contributed by NM,
1-Mar-2008.)
|
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵) |
|
Theorem | sbcco3g 2999* |
Composition of two substitutions. (Contributed by NM, 27-Nov-2005.)
(Revised by Mario Carneiro, 11-Nov-2016.)
|
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [𝐶 / 𝑦]𝜑)) |
|
Theorem | csbco3g 3000* |
Composition of two class substitutions. (Contributed by NM,
27-Nov-2005.) (Revised by Mario Carneiro, 11-Nov-2016.)
|
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐷 = ⦋𝐶 / 𝑦⦌𝐷) |