Theorem dfse3

Description: Alternate definition of set-like relationships. (Contributed by Scott Fenton, 19-Aug-2024)

	Ref	Expression
Assertion	dfse3	|- ( R Se A <-> A. x e. A Pred ( R , A , x ) e. _V )

Proof

Step	Hyp	Ref	Expression
1		dfse2	|- ( R Se A <-> A. x e. A ( A i^i ( `' R " { x } ) ) e. _V )
2		df-pred	|- Pred ( R , A , x ) = ( A i^i ( `' R " { x } ) )
3	2	eleq1i	|- ( Pred ( R , A , x ) e. _V <-> ( A i^i ( `' R " { x } ) ) e. _V )
4	3	ralbii	|- ( A. x e. A Pred ( R , A , x ) e. _V <-> A. x e. A ( A i^i ( `' R " { x } ) ) e. _V )
5	1 4	bitr4i	|- ( R Se A <-> A. x e. A Pred ( R , A , x ) e. _V )