Metamath Proof Explorer

Definition df-mvrs

Description: Define the set of variables in an expression. (Contributed by Mario Carneiro, 14-Jul-2016)

Ref Expression
Assertion df-mvrs ⊢ mVars = t ∈ V ⟼ e ∈ mEx ⁡ t ⟼ ran ⁡ 2 nd ⁡ e ∩ mVR ⁡ t

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmvrs class mVars
1 vt setvar t
2 cvv class V
3 ve setvar e
4 cmex class mEx
5 1 cv setvar t
6 5 4 cfv class mEx ⁡ t
7 c2nd class 2 nd
8 3 cv setvar e
9 8 7 cfv class 2 nd ⁡ e
10 9 crn class ran ⁡ 2 nd ⁡ e
11 cmvar class mVR
12 5 11 cfv class mVR ⁡ t
13 10 12 cin class ran ⁡ 2 nd ⁡ e ∩ mVR ⁡ t
14 3 6 13 cmpt class e ∈ mEx ⁡ t ⟼ ran ⁡ 2 nd ⁡ e ∩ mVR ⁡ t
15 1 2 14 cmpt class t ∈ V ⟼ e ∈ mEx ⁡ t ⟼ ran ⁡ 2 nd ⁡ e ∩ mVR ⁡ t
16 0 15 wceq wff mVars = t ∈ V ⟼ e ∈ mEx ⁡ t ⟼ ran ⁡ 2 nd ⁡ e ∩ mVR ⁡ t