Theorem eldmres3

Description: Elementhood in the domain of a restriction. (Contributed by Peter Mazsa, 23-Nov-2025)

	Ref	Expression
Assertion	eldmres3	|- ( B e. V -> ( B e. dom ( R |` A ) <-> ( B e. A /\ [ B ] R =/= (/) ) ) )

Proof

Step	Hyp	Ref	Expression
1		eldmres2	|- ( B e. V -> ( B e. dom ( R |` A ) <-> ( B e. A /\ E. y y e. [ B ] R ) ) )
2		n0	|- ( [ B ] R =/= (/) <-> E. y y e. [ B ] R )
3	2	anbi2i	|- ( ( B e. A /\ [ B ] R =/= (/) ) <-> ( B e. A /\ E. y y e. [ B ] R ) )
4	1 3	bitr4di	|- ( B e. V -> ( B e. dom ( R |` A ) <-> ( B e. A /\ [ B ] R =/= (/) ) ) )