P. 365 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36401-36500   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	cmvrs 36401	The variables in an expression.
class mVars
Syntax	cmrsub 36402	The set of raw substitutions.
class mRSubst
Syntax	cmsub 36403	The set of substitutions.
class mSubst
Syntax	cmvh 36404	The set of variable hypotheses.
class mVH
Syntax	cmpst 36405	The set of pre-statements.
class mPreSt
Syntax	cmsr 36406	The reduct of a pre-statement.
class mStRed
Syntax	cmsta 36407	The set of statements.
class mStat
Syntax	cmfs 36408	The set of formal systems.
class mFS
Syntax	cmcls 36409	The closure of a set of statements.
class mCls
Syntax	cmpps 36410	The set of provable pre-statements.
class mPPSt
Syntax	cmthm 36411	The set of theorems.
class mThm
Definition	df-mcn 36412	Define the set of constants in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mCN = Slot 1
Definition	df-mvar 36413	Define the set of variables in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mVR = Slot 2
Definition	df-mty 36414	Define the type function in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mType = Slot 3
Definition	df-mtc 36415	Define the set of typecodes in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mTC = Slot 4
Definition	df-mmax 36416	Define the set of axioms in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mAx = Slot 5
Definition	df-mvt 36417	Define the set of variable typecodes in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mVT = (𝑡 ∈ V ↦ ran (mType‘𝑡))
Definition	df-mrex 36418	Define the set of "raw expressions", which are expressions without a typecode attached. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mREx = (𝑡 ∈ V ↦ Word ((mCN‘𝑡) ∪ (mVR‘𝑡)))
Definition	df-mex 36419	Define the set of expressions, which are strings of constants and variables headed by a typecode constant. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mEx = (𝑡 ∈ V ↦ ((mTC‘𝑡) × (mREx‘𝑡)))
Definition	df-mdv 36420	Define the set of distinct variable conditions, which are pairs of distinct variables. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mDV = (𝑡 ∈ V ↦ (((mVR‘𝑡) × (mVR‘𝑡)) ∖ I ))
Definition	df-mvrs 36421*	Define the set of variables in an expression. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mVars = (𝑡 ∈ V ↦ (𝑒 ∈ (mEx‘𝑡) ↦ (ran (2nd ‘𝑒) ∩ (mVR‘𝑡))))
Definition	df-mrsub 36422*	Define a substitution of raw expressions given a mapping from variables to expressions. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mRSubst = (𝑡 ∈ V ↦ (𝑓 ∈ ((mREx‘𝑡) ↑pm (mVR‘𝑡)) ↦ (𝑒 ∈ (mREx‘𝑡) ↦ ((freeMnd‘((mCN‘𝑡) ∪ (mVR‘𝑡))) Σg ((𝑣 ∈ ((mCN‘𝑡) ∪ (mVR‘𝑡)) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), ⟨“𝑣”⟩)) ∘ 𝑒)))))
Definition	df-msub 36423*	Define a substitution of expressions given a mapping from variables to expressions. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mSubst = (𝑡 ∈ V ↦ (𝑓 ∈ ((mREx‘𝑡) ↑pm (mVR‘𝑡)) ↦ (𝑒 ∈ (mEx‘𝑡) ↦ ⟨(1st ‘𝑒), (((mRSubst‘𝑡)‘𝑓)‘(2nd ‘𝑒))⟩)))
Definition	df-mvh 36424*	Define the mapping from variables to their variable hypothesis. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mVH = (𝑡 ∈ V ↦ (𝑣 ∈ (mVR‘𝑡) ↦ ⟨((mType‘𝑡)‘𝑣), ⟨“𝑣”⟩⟩))
Definition	df-mpst 36425*	Define the set of all pre-statements. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mPreSt = (𝑡 ∈ V ↦ (({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ ◡𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin)) × (mEx‘𝑡)))
Definition	df-msr 36426*	Define the reduct of a pre-statement. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mStRed = (𝑡 ∈ V ↦ (𝑠 ∈ (mPreSt‘𝑡) ↦ ⦋(2nd ‘(1st ‘𝑠)) / ℎ⦌⦋(2nd ‘𝑠) / 𝑎⦌⟨((1st ‘(1st ‘𝑠)) ∩ ⦋∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎⟩))
Definition	df-msta 36427	Define the set of all statements. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mStat = (𝑡 ∈ V ↦ ran (mStRed‘𝑡))
Definition	df-mfs 36428*	Define the set of all formal systems. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mFS = {𝑡 ∣ ((((mCN‘𝑡) ∩ (mVR‘𝑡)) = ∅ ∧ (mType‘𝑡):(mVR‘𝑡)⟶(mTC‘𝑡)) ∧ ((mAx‘𝑡) ⊆ (mStat‘𝑡) ∧ ∀𝑣 ∈ (mVT‘𝑡) ¬ (◡(mType‘𝑡) “ {𝑣}) ∈ Fin))}
Definition	df-mcls 36429*	Define the closure of a set of statements relative to a set of disjointness constraints. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mCls = (𝑡 ∈ V ↦ (𝑑 ∈ 𝒫 (mDV‘𝑡), ℎ ∈ 𝒫 (mEx‘𝑡) ↦ ∩ {𝑐 ∣ ((ℎ ∪ ran (mVH‘𝑡)) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐)))}))
Definition	df-mpps 36430*	Define the set of provable pre-statements. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mPPSt = (𝑡 ∈ V ↦ {⟨⟨𝑑, ℎ⟩, 𝑎⟩ ∣ (⟨𝑑, ℎ, 𝑎⟩ ∈ (mPreSt‘𝑡) ∧ 𝑎 ∈ (𝑑(mCls‘𝑡)ℎ))})
Definition	df-mthm 36431	Define the set of theorems. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mThm = (𝑡 ∈ V ↦ (◡(mStRed‘𝑡) “ ((mStRed‘𝑡) “ (mPPSt‘𝑡))))
Theorem	mvtval 36432	The set of variable typecodes. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVT‘𝑇)    &   ⊢ 𝑌 = (mType‘𝑇)    ⇒   ⊢ 𝑉 = ran 𝑌
Theorem	mrexval 36433	The set of "raw expressions", which are expressions without a typecode, that is, just sequences of constants and variables. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐶 = (mCN‘𝑇)    &   ⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    ⇒   ⊢ (𝑇 ∈ 𝑊 → 𝑅 = Word (𝐶 ∪ 𝑉))
Theorem	mexval 36434	The set of expressions, which are pairs whose first element is a typecode, and whose second element is a raw expression. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐾 = (mTC‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    ⇒   ⊢ 𝐸 = (𝐾 × 𝑅)
Theorem	mexval2 36435	The set of expressions, which are pairs whose first element is a typecode, and whose second element is a list of constants and variables. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐾 = (mTC‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝐶 = (mCN‘𝑇)    &   ⊢ 𝑉 = (mVR‘𝑇)    ⇒   ⊢ 𝐸 = (𝐾 × Word (𝐶 ∪ 𝑉))
Theorem	mdvval 36436	The set of disjoint variable conditions, which are pairs of distinct variables. (This definition differs from appendix C, which uses unordered pairs instead. We use ordered pairs, but all sets of disjoint variable conditions of interest will be symmetric, so it does not matter.) (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝐷 = (mDV‘𝑇)    ⇒   ⊢ 𝐷 = ((𝑉 × 𝑉) ∖ I )
Theorem	mvrsval 36437	The set of variables in an expression. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝑊 = (mVars‘𝑇)    ⇒   ⊢ (𝑋 ∈ 𝐸 → (𝑊‘𝑋) = (ran (2nd ‘𝑋) ∩ 𝑉))
Theorem	mvrsfpw 36438	The set of variables in an expression is a finite subset of 𝑉. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝑊 = (mVars‘𝑇)    ⇒   ⊢ (𝑋 ∈ 𝐸 → (𝑊‘𝑋) ∈ (𝒫 𝑉 ∩ Fin))
Theorem	mrsubffval 36439*	The substitution of some variables for expressions in a raw expression. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐶 = (mCN‘𝑇)    &   ⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mRSubst‘𝑇)    &   ⊢ 𝐺 = (freeMnd‘(𝐶 ∪ 𝑉))    ⇒   ⊢ (𝑇 ∈ 𝑊 → 𝑆 = (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ 𝑅 ↦ (𝐺 Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), ⟨“𝑣”⟩)) ∘ 𝑒)))))
Theorem	mrsubfval 36440*	The substitution of some variables for expressions in a raw expression. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐶 = (mCN‘𝑇)    &   ⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mRSubst‘𝑇)    &   ⊢ 𝐺 = (freeMnd‘(𝐶 ∪ 𝑉))    ⇒   ⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉) → (𝑆‘𝐹) = (𝑒 ∈ 𝑅 ↦ (𝐺 Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝐴, (𝐹‘𝑣), ⟨“𝑣”⟩)) ∘ 𝑒))))
Theorem	mrsubval 36441*	The substitution of some variables for expressions in a raw expression. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐶 = (mCN‘𝑇)    &   ⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mRSubst‘𝑇)    &   ⊢ 𝐺 = (freeMnd‘(𝐶 ∪ 𝑉))    ⇒   ⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝑅) → ((𝑆‘𝐹)‘𝑋) = (𝐺 Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝐴, (𝐹‘𝑣), ⟨“𝑣”⟩)) ∘ 𝑋)))
Theorem	mrsubcv 36442	The value of a substituted singleton. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐶 = (mCN‘𝑇)    &   ⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mRSubst‘𝑇)    ⇒   ⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ (𝐶 ∪ 𝑉)) → ((𝑆‘𝐹)‘⟨“𝑋”⟩) = if(𝑋 ∈ 𝐴, (𝐹‘𝑋), ⟨“𝑋”⟩))
Theorem	mrsubvr 36443	The value of a substituted variable. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mRSubst‘𝑇)    ⇒   ⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐴) → ((𝑆‘𝐹)‘⟨“𝑋”⟩) = (𝐹‘𝑋))
Theorem	mrsubff 36444	A substitution is a function from 𝑅 to 𝑅. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mRSubst‘𝑇)    ⇒   ⊢ (𝑇 ∈ 𝑊 → 𝑆:(𝑅 ↑pm 𝑉)⟶(𝑅 ↑m 𝑅))
Theorem	mrsubrn 36445	Although it is defined for partial mappings of variables, every partial substitution is a substitution on some complete mapping of the variables. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mRSubst‘𝑇)    ⇒   ⊢ ran 𝑆 = (𝑆 “ (𝑅 ↑m 𝑉))
Theorem	mrsubff1 36446	When restricted to complete mappings, the substitution-producing function is one-to-one. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mRSubst‘𝑇)    ⇒   ⊢ (𝑇 ∈ 𝑊 → (𝑆 ↾ (𝑅 ↑m 𝑉)):(𝑅 ↑m 𝑉)⟶1-1(𝑅 ↑m 𝑅))
Theorem	mrsubff1o 36447	When restricted to complete mappings, the substitution-producing function is bijective to the set of all substitutions. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mRSubst‘𝑇)    ⇒   ⊢ (𝑇 ∈ 𝑊 → (𝑆 ↾ (𝑅 ↑m 𝑉)):(𝑅 ↑m 𝑉)⟶1-1ontoran 𝑆)
Theorem	mrsub0 36448	The value of the substituted empty string. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑆 = (mRSubst‘𝑇)    ⇒   ⊢ (𝐹 ∈ ran 𝑆 → (𝐹‘∅) = ∅)
Theorem	mrsubf 36449	A substitution is a function. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑆 = (mRSubst‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    ⇒   ⊢ (𝐹 ∈ ran 𝑆 → 𝐹:𝑅⟶𝑅)
Theorem	mrsubccat 36450	Substitution distributes over concatenation. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑆 = (mRSubst‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    ⇒   ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅) → (𝐹‘(𝑋 ++ 𝑌)) = ((𝐹‘𝑋) ++ (𝐹‘𝑌)))
Theorem	mrsubcn 36451	A substitution does not change the value of constant substrings. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑆 = (mRSubst‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝐶 = (mCN‘𝑇)    ⇒   ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑋 ∈ (𝐶 ∖ 𝑉)) → (𝐹‘⟨“𝑋”⟩) = ⟨“𝑋”⟩)
Theorem	elmrsubrn 36452*	Characterization of the substitutions as functions from expressions to expressions that distribute under concatenation and map constants to themselves. (The constant part uses (𝐶 ∖ 𝑉) because we don't know that 𝐶 and 𝑉 are disjoint until we get to ismfs 36481.) (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑆 = (mRSubst‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝐶 = (mCN‘𝑇)    ⇒   ⊢ (𝑇 ∈ 𝑊 → (𝐹 ∈ ran 𝑆 ↔ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))))
Theorem	mrsubco 36453	The composition of two substitutions is a substitution. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑆 = (mRSubst‘𝑇)    ⇒   ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) → (𝐹 ∘ 𝐺) ∈ ran 𝑆)
Theorem	mrsubvrs 36454*	The set of variables in a substitution is the union, indexed by the variables in the original expression, of the variables in the substitution to that variable. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑆 = (mRSubst‘𝑇)    &   ⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    ⇒   ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑋 ∈ 𝑅) → (ran (𝐹‘𝑋) ∩ 𝑉) = ∪ 𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘⟨“𝑥”⟩) ∩ 𝑉))
Theorem	msubffval 36455*	A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mSubst‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝑂 = (mRSubst‘𝑇)    ⇒   ⊢ (𝑇 ∈ 𝑊 → 𝑆 = (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1st ‘𝑒), ((𝑂‘𝑓)‘(2nd ‘𝑒))⟩)))
Theorem	msubfval 36456*	A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mSubst‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝑂 = (mRSubst‘𝑇)    ⇒   ⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉) → (𝑆‘𝐹) = (𝑒 ∈ 𝐸 ↦ ⟨(1st ‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))⟩))
Theorem	msubval 36457	A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mSubst‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝑂 = (mRSubst‘𝑇)    ⇒   ⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐸) → ((𝑆‘𝐹)‘𝑋) = ⟨(1st ‘𝑋), ((𝑂‘𝐹)‘(2nd ‘𝑋))⟩)
Theorem	msubrsub 36458	A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mSubst‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝑂 = (mRSubst‘𝑇)    ⇒   ⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐸) → (2nd ‘((𝑆‘𝐹)‘𝑋)) = ((𝑂‘𝐹)‘(2nd ‘𝑋)))
Theorem	msubty 36459	The type of a substituted expression is the same as the original type. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mSubst‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    ⇒   ⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐸) → (1st ‘((𝑆‘𝐹)‘𝑋)) = (1st ‘𝑋))
Theorem	elmsubrn 36460*	Characterization of substitution in terms of raw substitution, without reference to the generating functions. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝑂 = (mRSubst‘𝑇)    &   ⊢ 𝑆 = (mSubst‘𝑇)    ⇒   ⊢ ran 𝑆 = ran (𝑓 ∈ ran 𝑂 ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))⟩))
Theorem	msubrn 36461	Although it is defined for partial mappings of variables, every partial substitution is a substitution on some complete mapping of the variables. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mSubst‘𝑇)    ⇒   ⊢ ran 𝑆 = (𝑆 “ (𝑅 ↑m 𝑉))
Theorem	msubff 36462	A substitution is a function from 𝐸 to 𝐸. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mSubst‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    ⇒   ⊢ (𝑇 ∈ 𝑊 → 𝑆:(𝑅 ↑pm 𝑉)⟶(𝐸 ↑m 𝐸))
Theorem	msubco 36463	The composition of two substitutions is a substitution. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑆 = (mSubst‘𝑇)    ⇒   ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) → (𝐹 ∘ 𝐺) ∈ ran 𝑆)
Theorem	msubf 36464	A substitution is a function. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑆 = (mSubst‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    ⇒   ⊢ (𝐹 ∈ ran 𝑆 → 𝐹:𝐸⟶𝐸)
Theorem	mvhfval 36465*	Value of the function mapping variables to their corresponding variable expressions. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑌 = (mType‘𝑇)    &   ⊢ 𝐻 = (mVH‘𝑇)    ⇒   ⊢ 𝐻 = (𝑣 ∈ 𝑉 ↦ ⟨(𝑌‘𝑣), ⟨“𝑣”⟩⟩)
Theorem	mvhval 36466	Value of the function mapping variables to their corresponding variable expressions. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑌 = (mType‘𝑇)    &   ⊢ 𝐻 = (mVH‘𝑇)    ⇒   ⊢ (𝑋 ∈ 𝑉 → (𝐻‘𝑋) = ⟨(𝑌‘𝑋), ⟨“𝑋”⟩⟩)
Theorem	mpstval 36467*	A pre-statement is an ordered triple, whose first member is a symmetric set of disjoint variable conditions, whose second member is a finite set of expressions, and whose third member is an expression. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mDV‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝑃 = (mPreSt‘𝑇)    ⇒   ⊢ 𝑃 = (({𝑑 ∈ 𝒫 𝑉 ∣ ◡𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)) × 𝐸)
Theorem	elmpst 36468	Property of being a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mDV‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝑃 = (mPreSt‘𝑇)    ⇒   ⊢ (⟨𝐷, 𝐻, 𝐴⟩ ∈ 𝑃 ↔ ((𝐷 ⊆ 𝑉 ∧ ◡𝐷 = 𝐷) ∧ (𝐻 ⊆ 𝐸 ∧ 𝐻 ∈ Fin) ∧ 𝐴 ∈ 𝐸))
Theorem	msrfval 36469*	Value of the reduct of a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVars‘𝑇)    &   ⊢ 𝑃 = (mPreSt‘𝑇)    &   ⊢ 𝑅 = (mStRed‘𝑇)    ⇒   ⊢ 𝑅 = (𝑠 ∈ 𝑃 ↦ ⦋(2nd ‘(1st ‘𝑠)) / ℎ⦌⦋(2nd ‘𝑠) / 𝑎⦌⟨((1st ‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉 “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎⟩)
Theorem	msrval 36470	Value of the reduct of a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVars‘𝑇)    &   ⊢ 𝑃 = (mPreSt‘𝑇)    &   ⊢ 𝑅 = (mStRed‘𝑇)    &   ⊢ 𝑍 = ∪ (𝑉 “ (𝐻 ∪ {𝐴}))    ⇒   ⊢ (⟨𝐷, 𝐻, 𝐴⟩ ∈ 𝑃 → (𝑅‘⟨𝐷, 𝐻, 𝐴⟩) = ⟨(𝐷 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩)
Theorem	mpstssv 36471	A pre-statement is an ordered triple. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑃 = (mPreSt‘𝑇)    ⇒   ⊢ 𝑃 ⊆ ((V × V) × V)
Theorem	mpst123 36472	Decompose a pre-statement into a triple of values. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑃 = (mPreSt‘𝑇)    ⇒   ⊢ (𝑋 ∈ 𝑃 → 𝑋 = ⟨(1st ‘(1st ‘𝑋)), (2nd ‘(1st ‘𝑋)), (2nd ‘𝑋)⟩)
Theorem	mpstrcl 36473	The elements of a pre-statement are sets. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑃 = (mPreSt‘𝑇)    ⇒   ⊢ (⟨𝐷, 𝐻, 𝐴⟩ ∈ 𝑃 → (𝐷 ∈ V ∧ 𝐻 ∈ V ∧ 𝐴 ∈ V))
Theorem	msrf 36474	The reduct of a pre-statement is a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑃 = (mPreSt‘𝑇)    &   ⊢ 𝑅 = (mStRed‘𝑇)    ⇒   ⊢ 𝑅:𝑃⟶𝑃
Theorem	msrrcl 36475	If 𝑋 and 𝑌 have the same reduct, then one is a pre-statement iff the other is. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑃 = (mPreSt‘𝑇)    &   ⊢ 𝑅 = (mStRed‘𝑇)    ⇒   ⊢ ((𝑅‘𝑋) = (𝑅‘𝑌) → (𝑋 ∈ 𝑃 ↔ 𝑌 ∈ 𝑃))
Theorem	mstaval 36476	Value of the set of statements. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑅 = (mStRed‘𝑇)    &   ⊢ 𝑆 = (mStat‘𝑇)    ⇒   ⊢ 𝑆 = ran 𝑅
Theorem	msrid 36477	The reduct of a statement is itself. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑅 = (mStRed‘𝑇)    &   ⊢ 𝑆 = (mStat‘𝑇)    ⇒   ⊢ (𝑋 ∈ 𝑆 → (𝑅‘𝑋) = 𝑋)
Theorem	msrfo 36478	The reduct of a pre-statement is a statement. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑅 = (mStRed‘𝑇)    &   ⊢ 𝑆 = (mStat‘𝑇)    &   ⊢ 𝑃 = (mPreSt‘𝑇)    ⇒   ⊢ 𝑅:𝑃⟶onto𝑆
Theorem	mstapst 36479	A statement is a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑃 = (mPreSt‘𝑇)    &   ⊢ 𝑆 = (mStat‘𝑇)    ⇒   ⊢ 𝑆 ⊆ 𝑃
Theorem	elmsta 36480	Property of being a statement. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑃 = (mPreSt‘𝑇)    &   ⊢ 𝑆 = (mStat‘𝑇)    &   ⊢ 𝑉 = (mVars‘𝑇)    &   ⊢ 𝑍 = ∪ (𝑉 “ (𝐻 ∪ {𝐴}))    ⇒   ⊢ (⟨𝐷, 𝐻, 𝐴⟩ ∈ 𝑆 ↔ (⟨𝐷, 𝐻, 𝐴⟩ ∈ 𝑃 ∧ 𝐷 ⊆ (𝑍 × 𝑍)))
Theorem	ismfs 36481*	A formal system is a tuple ⟨mCN, mVR, mType, mVT, mTC, mAx⟩ such that: mCN and mVR are disjoint; mType is a function from mVR to mVT; mVT is a subset of mTC; mAx is a set of statements; and for each variable typecode, there are infinitely many variables of that type. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐶 = (mCN‘𝑇)    &   ⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑌 = (mType‘𝑇)    &   ⊢ 𝐹 = (mVT‘𝑇)    &   ⊢ 𝐾 = (mTC‘𝑇)    &   ⊢ 𝐴 = (mAx‘𝑇)    &   ⊢ 𝑆 = (mStat‘𝑇)    ⇒   ⊢ (𝑇 ∈ 𝑊 → (𝑇 ∈ mFS ↔ (((𝐶 ∩ 𝑉) = ∅ ∧ 𝑌:𝑉⟶𝐾) ∧ (𝐴 ⊆ 𝑆 ∧ ∀𝑣 ∈ 𝐹 ¬ (◡𝑌 “ {𝑣}) ∈ Fin))))
Theorem	mfsdisj 36482	The constants and variables of a formal system are disjoint. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐶 = (mCN‘𝑇)    &   ⊢ 𝑉 = (mVR‘𝑇)    ⇒   ⊢ (𝑇 ∈ mFS → (𝐶 ∩ 𝑉) = ∅)
Theorem	mtyf2 36483	The type function maps variables to typecodes. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝐾 = (mTC‘𝑇)    &   ⊢ 𝑌 = (mType‘𝑇)    ⇒   ⊢ (𝑇 ∈ mFS → 𝑌:𝑉⟶𝐾)
Theorem	mtyf 36484	The type function maps variables to variable typecodes. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝐹 = (mVT‘𝑇)    &   ⊢ 𝑌 = (mType‘𝑇)    ⇒   ⊢ (𝑇 ∈ mFS → 𝑌:𝑉⟶𝐹)
Theorem	mvtss 36485	The set of variable typecodes is a subset of all typecodes. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐹 = (mVT‘𝑇)    &   ⊢ 𝐾 = (mTC‘𝑇)    ⇒   ⊢ (𝑇 ∈ mFS → 𝐹 ⊆ 𝐾)
Theorem	maxsta 36486	An axiom is a statement. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐴 = (mAx‘𝑇)    &   ⊢ 𝑆 = (mStat‘𝑇)    ⇒   ⊢ (𝑇 ∈ mFS → 𝐴 ⊆ 𝑆)
Theorem	mvtinf 36487	Each variable typecode has infinitely many variables. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐹 = (mVT‘𝑇)    &   ⊢ 𝑌 = (mType‘𝑇)    ⇒   ⊢ ((𝑇 ∈ mFS ∧ 𝑋 ∈ 𝐹) → ¬ (◡𝑌 “ {𝑋}) ∈ Fin)
Theorem	msubff1 36488	When restricted to complete mappings, the substitution-producing function is one-to-one. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mSubst‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    ⇒   ⊢ (𝑇 ∈ mFS → (𝑆 ↾ (𝑅 ↑m 𝑉)):(𝑅 ↑m 𝑉)⟶1-1(𝐸 ↑m 𝐸))
Theorem	msubff1o 36489	When restricted to complete mappings, the substitution-producing function is bijective to the set of all substitutions. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝑅 = (mREx‘𝑇)    &   ⊢ 𝑆 = (mSubst‘𝑇)    ⇒   ⊢ (𝑇 ∈ mFS → (𝑆 ↾ (𝑅 ↑m 𝑉)):(𝑅 ↑m 𝑉)⟶1-1ontoran 𝑆)
Theorem	mvhf 36490	The function mapping variables to variable expressions is a function. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝐻 = (mVH‘𝑇)    ⇒   ⊢ (𝑇 ∈ mFS → 𝐻:𝑉⟶𝐸)
Theorem	mvhf1 36491	The function mapping variables to variable expressions is one-to-one. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝐻 = (mVH‘𝑇)    ⇒   ⊢ (𝑇 ∈ mFS → 𝐻:𝑉⟶1-1𝐸)
Theorem	msubvrs 36492*	The set of variables in a substitution is the union, indexed by the variables in the original expression, of the variables in the substitution to that variable. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑆 = (mSubst‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝑉 = (mVars‘𝑇)    &   ⊢ 𝐻 = (mVH‘𝑇)    ⇒   ⊢ ((𝑇 ∈ mFS ∧ 𝐹 ∈ ran 𝑆 ∧ 𝑋 ∈ 𝐸) → (𝑉‘(𝐹‘𝑋)) = ∪ 𝑥 ∈ (𝑉‘𝑋)(𝑉‘(𝐹‘(𝐻‘𝑥))))
Theorem	mclsrcl 36493	Reverse closure for the closure function. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐷 = (mDV‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝐶 = (mCls‘𝑇)    ⇒   ⊢ (𝐴 ∈ (𝐾𝐶𝐵) → (𝑇 ∈ V ∧ 𝐾 ⊆ 𝐷 ∧ 𝐵 ⊆ 𝐸))
Theorem	mclsssvlem 36494*	Lemma for mclsssv 36496. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐷 = (mDV‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝐶 = (mCls‘𝑇)    &   ⊢ (𝜑 → 𝑇 ∈ mFS)    &   ⊢ (𝜑 → 𝐾 ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐸)    &   ⊢ 𝐻 = (mVH‘𝑇)    &   ⊢ 𝐴 = (mAx‘𝑇)    &   ⊢ 𝑆 = (mSubst‘𝑇)    &   ⊢ 𝑉 = (mVars‘𝑇)    ⇒   ⊢ (𝜑 → ∩ {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))} ⊆ 𝐸)
Theorem	mclsval 36495*	The function mapping variables to variable expressions is one-to-one. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐷 = (mDV‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝐶 = (mCls‘𝑇)    &   ⊢ (𝜑 → 𝑇 ∈ mFS)    &   ⊢ (𝜑 → 𝐾 ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐸)    &   ⊢ 𝐻 = (mVH‘𝑇)    &   ⊢ 𝐴 = (mAx‘𝑇)    &   ⊢ 𝑆 = (mSubst‘𝑇)    &   ⊢ 𝑉 = (mVars‘𝑇)    ⇒   ⊢ (𝜑 → (𝐾𝐶𝐵) = ∩ {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))})
Theorem	mclsssv 36496	The closure of a set of expressions is a set of expressions. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐷 = (mDV‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝐶 = (mCls‘𝑇)    &   ⊢ (𝜑 → 𝑇 ∈ mFS)    &   ⊢ (𝜑 → 𝐾 ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐸)    ⇒   ⊢ (𝜑 → (𝐾𝐶𝐵) ⊆ 𝐸)
Theorem	ssmclslem 36497	Lemma for ssmcls 36499. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐷 = (mDV‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝐶 = (mCls‘𝑇)    &   ⊢ (𝜑 → 𝑇 ∈ mFS)    &   ⊢ (𝜑 → 𝐾 ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐸)    &   ⊢ 𝐻 = (mVH‘𝑇)    ⇒   ⊢ (𝜑 → (𝐵 ∪ ran 𝐻) ⊆ (𝐾𝐶𝐵))
Theorem	vhmcls 36498	All variable hypotheses are in the closure. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐷 = (mDV‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝐶 = (mCls‘𝑇)    &   ⊢ (𝜑 → 𝑇 ∈ mFS)    &   ⊢ (𝜑 → 𝐾 ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐸)    &   ⊢ 𝐻 = (mVH‘𝑇)    &   ⊢ 𝑉 = (mVR‘𝑇)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐻‘𝑋) ∈ (𝐾𝐶𝐵))
Theorem	ssmcls 36499	The original expressions are also in the closure. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐷 = (mDV‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝐶 = (mCls‘𝑇)    &   ⊢ (𝜑 → 𝑇 ∈ mFS)    &   ⊢ (𝜑 → 𝐾 ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐸)    ⇒   ⊢ (𝜑 → 𝐵 ⊆ (𝐾𝐶𝐵))
Theorem	ss2mcls 36500	The closure is monotonic under subsets of the original set of expressions and the set of disjoint variable conditions. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝐷 = (mDV‘𝑇)    &   ⊢ 𝐸 = (mEx‘𝑇)    &   ⊢ 𝐶 = (mCls‘𝑇)    &   ⊢ (𝜑 → 𝑇 ∈ mFS)    &   ⊢ (𝜑 → 𝐾 ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐸)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝐾)    &   ⊢ (𝜑 → 𝑌 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝐶𝑌) ⊆ (𝐾𝐶𝐵))