Definition df-sate

Description: A simplified version of the satisfaction predicate, using the standard membership relation and eliminating the extra variable n . (Contributed by Mario Carneiro, 14-Jul-2013)

	Ref	Expression
Assertion	df-sate	$$⊢{\mathrm{Sat}}_{\in }=\left(m\in \mathrm{V},u\in \mathrm{V}⟼\left(m\mathrm{Sat}\left(\mathrm{E}\cap \left(m\times m\right)\right)\right)\left(\mathrm{\omega }\right)\left(u\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csate	$$class{\mathrm{Sat}}_{\in }$$
1		vm	$$setvarm$$
2		cvv	$$class\mathrm{V}$$
3		vu	$$setvaru$$
4	1	cv	$$setvarm$$
5		csat	$$class\mathrm{Sat}$$
6		cep	$$class\mathrm{E}$$
7	4 4	cxp	$$class\left(m\times m\right)$$
8	6 7	cin	$$class\left(\mathrm{E}\cap \left(m\times m\right)\right)$$
9	4 8 5	co	$$class\left(m\mathrm{Sat}\left(\mathrm{E}\cap \left(m\times m\right)\right)\right)$$
10		com	$$class\mathrm{\omega }$$
11	10 9	cfv	$$class\left(m\mathrm{Sat}\left(\mathrm{E}\cap \left(m\times m\right)\right)\right)\left(\mathrm{\omega }\right)$$
12	3	cv	$$setvaru$$
13	12 11	cfv	$$class\left(m\mathrm{Sat}\left(\mathrm{E}\cap \left(m\times m\right)\right)\right)\left(\mathrm{\omega }\right)\left(u\right)$$
14	1 3 2 2 13	cmpo	$$class\left(m\in \mathrm{V},u\in \mathrm{V}⟼\left(m\mathrm{Sat}\left(\mathrm{E}\cap \left(m\times m\right)\right)\right)\left(\mathrm{\omega }\right)\left(u\right)\right)$$
15	0 14	wceq	$$wff{\mathrm{Sat}}_{\in }=\left(m\in \mathrm{V},u\in \mathrm{V}⟼\left(m\mathrm{Sat}\left(\mathrm{E}\cap \left(m\times m\right)\right)\right)\left(\mathrm{\omega }\right)\left(u\right)\right)$$