P. 29 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 2801-2900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sbctt 2801	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 2802	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 2803	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 2804*	Substitution for a variable not occurring in a wff does not affect it. Distinct variable form of sbcgf 2802. (Contributed by Alan Sare, 10-Nov-2012.)
⊢ (A ∈ 𝑉 → ([A / x]φ ↔ φ))
Theorem	sbc2iegf 2805*	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 2806*	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 2807*	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 2808*	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 2809*	Lemma for sbccom 2810. (Contributed by NM, 14-Nov-2005.) (Revised by Mario Carneiro, 18-Oct-2016.)
⊢ ([A / x][B / y]φ ↔ [B / y][A / x]φ)
Theorem	sbccom 2810*	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 2811*	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 2812*	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 2813*	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 2814*	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 2815*	Interchange class substitution and restricted uniqueness quantifier. (Contributed by NM, 24-Feb-2013.)
⊢ (A ∈ 𝑉 → ([A / x]∃!y ∈ B φ ↔ ∃!y ∈ B [A / x]φ))
Theorem	sbcabel 2816*	Interchange class substitution and class abstraction. (Contributed by NM, 5-Nov-2005.)
⊢ ℲxB    ⇒   ⊢ (A ∈ 𝑉 → ([A / x]{y ∣ φ} ∈ B ↔ {y ∣ [A / x]φ} ∈ B))
Theorem	rspsbc 2817*	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 1640 and spsbc 2752. See also rspsbca 2818 and rspcsbela . (Contributed by NM, 17-Nov-2006.) (Proof shortened by Mario Carneiro, 13-Oct-2016.)
⊢ (A ∈ B → (∀x ∈ B φ → [A / x]φ))
Theorem	rspsbca 2818*	Restricted quantifier version of Axiom 4 of [Mendelson] p. 69. (Contributed by NM, 14-Dec-2005.)
⊢ ((A ∈ B ∧ ∀x ∈ B φ) → [A / x]φ)
Theorem	rspesbca 2819*	Existence form of rspsbca 2818. (Contributed by NM, 29-Feb-2008.) (Proof shortened by Mario Carneiro, 13-Oct-2016.)
⊢ ((A ∈ B ∧ [A / x]φ) → ∃x ∈ B φ)
Theorem	spesbc 2820	Existence form of spsbc 2752. (Contributed by Mario Carneiro, 18-Nov-2016.)
⊢ ([A / x]φ → ∃xφ)
Theorem	spesbcd 2821	form of spsbc 2752. (Contributed by Mario Carneiro, 9-Feb-2017.)
⊢ (φ → [A / x]ψ)    ⇒   ⊢ (φ → ∃xψ)
Theorem	sbcth2 2822*	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 2823	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 1458. (Contributed by NM, 16-Jan-2004.)
⊢ Ⅎxφ    ⇒   ⊢ (∀x ∈ A (φ → ψ) → (φ → ∀x ∈ A ψ))
Theorem	rmo2ilem 2824*	Condition implying restricted "at most one." (Contributed by Jim Kingdon, 14-Jul-2018.)
⊢ Ⅎyφ    ⇒   ⊢ (∃y∀x ∈ A (φ → x = y) → ∃*x ∈ A φ)
Theorem	rmo2i 2825*	Condition implying restricted "at most one." (Contributed by NM, 17-Jun-2017.)
⊢ Ⅎyφ    ⇒   ⊢ (∃y ∈ A ∀x ∈ A (φ → x = y) → ∃*x ∈ A φ)
Theorem	rmo3 2826*	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 2827*	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 2828*	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 2829	Extend class notation to include the proper substitution of a class for a set into another class.
class ⦋A / x⦌B
Definition	df-csb 2830*	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 2741, to prevent ambiguity. Theorem sbcel1g 2846 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 2855 recreates substitution into a wff from this definition. (Contributed by NM, 10-Nov-2005.)
⊢ ⦋A / x⦌B = {y ∣ [A / x]y ∈ B}
Theorem	csb2 2831*	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 2832	Analog of dfsbcq 2743 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
⊢ (A = B → ⦋A / x⦌𝐶 = ⦋B / x⦌𝐶)
Theorem	cbvcsb 2833	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 2834*	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 2835	Equality deduction for proper substitution into a class. (Contributed by NM, 3-Dec-2005.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → ⦋A / x⦌𝐶 = ⦋B / x⦌𝐶)
Theorem	csbid 2836	Analog of sbid 1639 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
⊢ ⦋x / x⦌A = A
Theorem	csbeq1a 2837	Equality theorem for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
⊢ (x = A → B = ⦋A / x⦌B)
Theorem	csbco 2838*	Composition law for chained substitutions into a class. (Contributed by NM, 10-Nov-2005.)
⊢ ⦋A / y⦌⦋y / x⦌B = ⦋A / x⦌B
Theorem	csbtt 2839	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 2840	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 2841*	Substitution doesn't affect a constant B (in which x is not free). csbconstgf 2840 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.)
⊢ (A ∈ 𝑉 → ⦋A / x⦌B = B)
Theorem	sbcel12g 2842	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 2843	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 2844	Distribute proper substitution through negated membership. (Contributed by Andrew Salmon, 18-Jun-2011.)
⊢ (A ∈ 𝑉 → ([A / x]B ∉ 𝐶 ↔ ⦋A / x⦌B ∉ ⦋A / x⦌𝐶))
Theorem	sbcne12g 2845	Distribute proper substitution through an inequality. (Contributed by Andrew Salmon, 18-Jun-2011.)
⊢ (A ∈ 𝑉 → ([A / x]B ≠ 𝐶 ↔ ⦋A / x⦌B ≠ ⦋A / x⦌𝐶))
Theorem	sbcel1g 2846*	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 2847*	Move proper substitution to first argument of an equality. (Contributed by NM, 30-Nov-2005.)
⊢ (A ∈ 𝑉 → ([A / x]B = 𝐶 ↔ ⦋A / x⦌B = 𝐶))
Theorem	sbcel2g 2848*	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 2849*	Move proper substitution to second argument of an equality. (Contributed by NM, 30-Nov-2005.)
⊢ (A ∈ 𝑉 → ([A / x]B = 𝐶 ↔ B = ⦋A / x⦌𝐶))
Theorem	csbcomg 2850*	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 2851	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 2852*	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 2853	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 2854	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 2855*	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 2856	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 2857	Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.)
⊢ (φ → ℲxA)    ⇒   ⊢ (φ → Ⅎx⦋A / x⦌B)
Theorem	nfcsb1 2858	Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.)
⊢ ℲxA    ⇒   ⊢ Ⅎx⦋A / x⦌B
Theorem	nfcsb1v 2859*	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 2860	Deduction version of nfcsb 2861. (Contributed by NM, 21-Nov-2005.) (Revised by Mario Carneiro, 12-Oct-2016.)
⊢ Ⅎyφ    &   ⊢ (φ → ℲxA)    &   ⊢ (φ → ℲxB)    ⇒   ⊢ (φ → Ⅎx⦋A / y⦌B)
Theorem	nfcsb 2861	Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.)
⊢ ℲxA    &   ⊢ ℲxB    ⇒   ⊢ Ⅎx⦋A / y⦌B
Theorem	csbhypf 2862*	Introduce an explicit substitution into an implicit substitution hypothesis. See sbhypf 2580 for class substitution version. (Contributed by NM, 19-Dec-2008.)
⊢ ℲxA    &   ⊢ Ⅎx𝐶    &   ⊢ (x = A → B = 𝐶)    ⇒   ⊢ (y = A → ⦋y / x⦌B = 𝐶)
Theorem	csbiebt 2863*	Conversion of implicit substitution to explicit substitution into a class. (Closed theorem version of csbiegf 2867.) (Contributed by NM, 11-Nov-2005.)
⊢ ((A ∈ 𝑉 ∧ Ⅎx𝐶) → (∀x(x = A → B = 𝐶) ↔ ⦋A / x⦌B = 𝐶))
Theorem	csbiedf 2864*	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 2865*	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 2866*	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 2867*	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 2868*	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 2869*	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 2870*	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 2871*	Conversion of implicit substitution to explicit substitution into a class (closed form of csbie2 2872). (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 2872*	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 2873*	Conversion of implicit substitution to explicit class substitution. This version of sbcie 2774 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 2874	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 2875	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 2876*	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 2877*	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 2878	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 2879*	Idempotent law for class substitutions. (Contributed by NM, 1-Mar-2008.)
⊢ (A ∈ 𝑉 → ⦋A / x⦌⦋A / x⦌B = ⦋A / x⦌B)
Theorem	sbcco3g 2880*	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 2881*	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 2882*	Special case related to rspsbc 2817. (Contributed by NM, 10-Dec-2005.) (Proof shortened by Eric Schmidt, 17-Jan-2007.)
⊢ ((A ∈ B ∧ ∀x ∈ B 𝐶 ∈ 𝐷) → ⦋A / x⦌𝐶 ∈ 𝐷)
Theorem	sbnfc2 2883*	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 2884*	Move substitution into a class abstraction. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ (A ∈ 𝑉 → ⦋A / x⦌{y ∣ φ} = {y ∣ [A / x]φ})
Theorem	cbvralcsf 2885	A more general version of cbvralf 2505 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 2886	A more general version of cbvrexf 2506 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 2887	A more general version of cbvreuv 2513 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 ψ)
Theorem	cbvrabcsf 2888	A more general version of cbvrab 2533 with no distinct variable restrictions. (Contributed by Andrew Salmon, 13-Jul-2011.)
⊢ ℲyA    &   ⊢ ℲxB    &   ⊢ Ⅎyφ    &   ⊢ Ⅎxψ    &   ⊢ (x = y → A = B)    &   ⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ {x ∈ A ∣ φ} = {y ∈ B ∣ ψ}
Theorem	cbvralv2 2889*	Rule used to change the bound variable in a restricted universal quantifier with implicit substitution which also changes the quantifier domain. (Contributed by David Moews, 1-May-2017.)
⊢ (x = y → (ψ ↔ χ))    &   ⊢ (x = y → A = B)    ⇒   ⊢ (∀x ∈ A ψ ↔ ∀y ∈ B χ)
Theorem	cbvrexv2 2890*	Rule used to change the bound variable in a restricted existential quantifier with implicit substitution which also changes the quantifier domain. (Contributed by David Moews, 1-May-2017.)
⊢ (x = y → (ψ ↔ χ))    &   ⊢ (x = y → A = B)    ⇒   ⊢ (∃x ∈ A ψ ↔ ∃y ∈ B χ)
2.1.11  Define basic set operations and relations
Syntax	cdif 2891	Extend class notation to include class difference (read: "A minus B").
class (A ∖ B)
Syntax	cun 2892	Extend class notation to include union of two classes (read: "A union B").
class (A ∪ B)
Syntax	cin 2893	Extend class notation to include the intersection of two classes (read: "A intersect B").
class (A ∩ B)
Syntax	wss 2894	Extend wff notation to include the subclass relation. This is read "A is a subclass of B " or "B includes A." When A exists as a set, it is also read "A is a subset of B."
wff A ⊆ B
Syntax	wpss 2895	Extend wff notation with proper subclass relation.
wff A ⊊ B
Theorem	difjust 2896*	Soundness justification theorem for df-dif 2897. (Contributed by Rodolfo Medina, 27-Apr-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ {x ∣ (x ∈ A ∧ ¬ x ∈ B)} = {y ∣ (y ∈ A ∧ ¬ y ∈ B)}
Definition	df-dif 2897*	Define class difference, also called relative complement. Definition 5.12 of [TakeutiZaring] p. 20. Contrast this operation with union (A ∪ B) (df-un 2899) and intersection (A ∩ B) (df-in 2901). Several notations are used in the literature; we chose the ∖ convention used in Definition 5.3 of [Eisenberg] p. 67 instead of the more common minus sign to reserve the latter for later use in, e.g., arithmetic. We will use the terminology "A excludes B " to mean A ∖ B. We will use "B is removed from A " to mean A ∖ {B} i.e. the removal of an element or equivalently the exclusion of a singleton. (Contributed by NM, 29-Apr-1994.)
⊢ (A ∖ B) = {x ∣ (x ∈ A ∧ ¬ x ∈ B)}
Theorem	unjust 2898*	Soundness justification theorem for df-un 2899. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ {x ∣ (x ∈ A ∨ x ∈ B)} = {y ∣ (y ∈ A ∨ y ∈ B)}
Definition	df-un 2899*	Define the union of two classes. Definition 5.6 of [TakeutiZaring] p. 16. Contrast this operation with difference (A ∖ B) (df-dif 2897) and intersection (A ∩ B) (df-in 2901). (Contributed by NM, 23-Aug-1993.)
⊢ (A ∪ B) = {x ∣ (x ∈ A ∨ x ∈ B)}
Theorem	injust 2900*	Soundness justification theorem for df-in 2901. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ {x ∣ (x ∈ A ∧ x ∈ B)} = {y ∣ (y ∈ A ∧ y ∈ B)}