Theorem releldmb

Description: Membership in a domain. (Contributed by Mario Carneiro, 5-Nov-2015)

	Ref	Expression
Assertion	releldmb	|- ( Rel R -> ( A e. dom R <-> E. x A R x ) )

Proof

Step	Hyp	Ref	Expression
1		eldmg	|- ( A e. dom R -> ( A e. dom R <-> E. x A R x ) )
2	1	ibi	|- ( A e. dom R -> E. x A R x )
3		releldm	|- ( ( Rel R /\ A R x ) -> A e. dom R )
4	3	ex	|- ( Rel R -> ( A R x -> A e. dom R ) )
5	4	exlimdv	|- ( Rel R -> ( E. x A R x -> A e. dom R ) )
6	2 5	impbid2	|- ( Rel R -> ( A e. dom R <-> E. x A R x ) )