Theorem suppvalbr

Description: The value of the operation constructing the support of a function expressed by binary relations. (Contributed by AV, 7-Apr-2019) (Proof shortened by Sky Winter, 14-Oct-2026)

	Ref	Expression
Assertion	suppvalbr	|- ( ( R e. V /\ Z e. W ) -> ( R supp Z ) = { x | ( E. y x R y /\ E. y ( x R y <-> y =/= Z ) ) } )

Proof

Step	Hyp	Ref	Expression
1		suppval	|- ( ( R e. V /\ Z e. W ) -> ( R supp Z ) = { x e. dom R | ( R " { x } ) =/= { Z } } )
2		df-rab	|- { x e. dom R | ( R " { x } ) =/= { Z } } = { x | ( x e. dom R /\ ( R " { x } ) =/= { Z } ) }
3		vex	|- x e. _V
4	3	eldm	|- ( x e. dom R <-> E. y x R y )
5		nabbib	|- ( { y | x R y } =/= { y | y = Z } <-> E. y ( x R y <-> -. y = Z ) )
6		imasng	|- ( x e. _V -> ( R " { x } ) = { y | x R y } )
7	6	elv	|- ( R " { x } ) = { y | x R y }
8		df-sn	|- { Z } = { y | y = Z }
9	7 8	neeq12i	|- ( ( R " { x } ) =/= { Z } <-> { y | x R y } =/= { y | y = Z } )
10		df-ne	|- ( y =/= Z <-> -. y = Z )
11	10	bibi2i	|- ( ( x R y <-> y =/= Z ) <-> ( x R y <-> -. y = Z ) )
12	11	exbii	|- ( E. y ( x R y <-> y =/= Z ) <-> E. y ( x R y <-> -. y = Z ) )
13	5 9 12	3bitr4i	|- ( ( R " { x } ) =/= { Z } <-> E. y ( x R y <-> y =/= Z ) )
14	4 13	anbi12i	|- ( ( x e. dom R /\ ( R " { x } ) =/= { Z } ) <-> ( E. y x R y /\ E. y ( x R y <-> y =/= Z ) ) )
15	14	abbii	|- { x | ( x e. dom R /\ ( R " { x } ) =/= { Z } ) } = { x | ( E. y x R y /\ E. y ( x R y <-> y =/= Z ) ) }
16	2 15	eqtri	|- { x e. dom R | ( R " { x } ) =/= { Z } } = { x | ( E. y x R y /\ E. y ( x R y <-> y =/= Z ) ) }
17	1 16	eqtrdi	|- ( ( R e. V /\ Z e. W ) -> ( R supp Z ) = { x | ( E. y x R y /\ E. y ( x R y <-> y =/= Z ) ) } )