Theorem dfssr2

Description: Alternate definition of the subset relation. (Contributed by Peter Mazsa, 9-Aug-2021)

	Ref	Expression
Assertion	dfssr2	|- _S = ( ( _V X. _V ) \ ran ( _E |X. ( _V \ _E ) ) )

Proof

Step	Hyp	Ref	Expression
1		epel	|- ( z _E x <-> z e. x )
2		brvdif	|- ( z ( _V \ _E ) y <-> -. z _E y )
3		epel	|- ( z _E y <-> z e. y )
4	2 3	xchbinx	|- ( z ( _V \ _E ) y <-> -. z e. y )
5	1 4	anbi12i	|- ( ( z _E x /\ z ( _V \ _E ) y ) <-> ( z e. x /\ -. z e. y ) )
6	5	exbii	|- ( E. z ( z _E x /\ z ( _V \ _E ) y ) <-> E. z ( z e. x /\ -. z e. y ) )
7	6	notbii	|- ( -. E. z ( z _E x /\ z ( _V \ _E ) y ) <-> -. E. z ( z e. x /\ -. z e. y ) )
8		dfss6	|- ( x C_ y <-> -. E. z ( z e. x /\ -. z e. y ) )
9	7 8	bitr4i	|- ( -. E. z ( z _E x /\ z ( _V \ _E ) y ) <-> x C_ y )
10	9	opabbii	|- { <. x , y >. | -. E. z ( z _E x /\ z ( _V \ _E ) y ) } = { <. x , y >. | x C_ y }
11		rnxrn	|- ran ( _E |X. ( _V \ _E ) ) = { <. x , y >. | E. z ( z _E x /\ z ( _V \ _E ) y ) }
12	11	difeq2i	|- ( ( _V X. _V ) \ ran ( _E |X. ( _V \ _E ) ) ) = ( ( _V X. _V ) \ { <. x , y >. | E. z ( z _E x /\ z ( _V \ _E ) y ) } )
13		vvdifopab	|- ( ( _V X. _V ) \ { <. x , y >. | E. z ( z _E x /\ z ( _V \ _E ) y ) } ) = { <. x , y >. | -. E. z ( z _E x /\ z ( _V \ _E ) y ) }
14	12 13	eqtri	|- ( ( _V X. _V ) \ ran ( _E |X. ( _V \ _E ) ) ) = { <. x , y >. | -. E. z ( z _E x /\ z ( _V \ _E ) y ) }
15		df-ssr	|- _S = { <. x , y >. | x C_ y }
16	10 14 15	3eqtr4ri	|- _S = ( ( _V X. _V ) \ ran ( _E |X. ( _V \ _E ) ) )