df-msub

Description: Define a substitution of expressions given a mapping from variables to expressions. (Contributed by Mario Carneiro, 14-Jul-2016)

		Ref	Expression
	Assertion	df-msub	$⊢ mSubst = (t \in V ⟼ (f \in (mREx (t) ↑_{𝑝𝑚} mVR (t)) ⟼ (e \in mEx (t) ⟼ ⟨1^{st} (e), mRSubst (t) (f) (2^{nd} (e))⟩)))$

Step	Hyp	Ref	Expression
0		cmsub	$class mSubst$
1		vt	$setvar t$
2		cvv	$class V$
3		vf	$setvar f$
4		cmrex	$class mREx$
5	1	cv	$setvar t$
6	5 4	cfv	$class mREx (t)$
7		cpm	$class ↑_{𝑝𝑚}$
8		cmvar	$class mVR$
9	5 8	cfv	$class mVR (t)$
10	6 9 7	co	$class (mREx (t) ↑_{𝑝𝑚} mVR (t))$
11		ve	$setvar e$
12		cmex	$class mEx$
13	5 12	cfv	$class mEx (t)$
14		c1st	$class 1^{st}$
15	11	cv	$setvar e$
16	15 14	cfv	$class 1^{st} (e)$
17		cmrsub	$class mRSubst$
18	5 17	cfv	$class mRSubst (t)$
19	3	cv	$setvar f$
20	19 18	cfv	$class mRSubst (t) (f)$
21		c2nd	$class 2^{nd}$
22	15 21	cfv	$class 2^{nd} (e)$
23	22 20	cfv	$class mRSubst (t) (f) (2^{nd} (e))$
24	16 23	cop	$class ⟨1^{st} (e), mRSubst (t) (f) (2^{nd} (e))⟩$
25	11 13 24	cmpt	$class (e \in mEx (t) ⟼ ⟨1^{st} (e), mRSubst (t) (f) (2^{nd} (e))⟩)$
26	3 10 25	cmpt	$class (f \in (mREx (t) ↑_{𝑝𝑚} mVR (t)) ⟼ (e \in mEx (t) ⟼ ⟨1^{st} (e), mRSubst (t) (f) (2^{nd} (e))⟩))$
27	1 2 26	cmpt	$class (t \in V ⟼ (f \in (mREx (t) ↑_{𝑝𝑚} mVR (t)) ⟼ (e \in mEx (t) ⟼ ⟨1^{st} (e), mRSubst (t) (f) (2^{nd} (e))⟩)))$
28	0 27	wceq	$wff mSubst = (t \in V ⟼ (f \in (mREx (t) ↑_{𝑝𝑚} mVR (t)) ⟼ (e \in mEx (t) ⟼ ⟨1^{st} (e), mRSubst (t) (f) (2^{nd} (e))⟩)))$

Metamath Proof Explorer