Theorem ecdmn0

Description: A representative of a nonempty equivalence class belongs to the domain of the equivalence relation. (Contributed by NM, 15-Feb-1996) (Revised by Mario Carneiro, 9-Jul-2014)

	Ref	Expression
Assertion	ecdmn0	|- ( A e. dom R <-> [ A ] R =/= (/) )

Proof

Step	Hyp	Ref	Expression
1		elex	|- ( A e. dom R -> A e. _V )
2		n0	|- ( [ A ] R =/= (/) <-> E. x x e. [ A ] R )
3		ecexr	|- ( x e. [ A ] R -> A e. _V )
4	3	exlimiv	|- ( E. x x e. [ A ] R -> A e. _V )
5	2 4	sylbi	|- ( [ A ] R =/= (/) -> A e. _V )
6		vex	|- x e. _V
7		elecg	|- ( ( x e. _V /\ A e. _V ) -> ( x e. [ A ] R <-> A R x ) )
8	6 7	mpan	|- ( A e. _V -> ( x e. [ A ] R <-> A R x ) )
9	8	exbidv	|- ( A e. _V -> ( E. x x e. [ A ] R <-> E. x A R x ) )
10	2	a1i	|- ( A e. _V -> ( [ A ] R =/= (/) <-> E. x x e. [ A ] R ) )
11		eldmg	|- ( A e. _V -> ( A e. dom R <-> E. x A R x ) )
12	9 10 11	3bitr4rd	|- ( A e. _V -> ( A e. dom R <-> [ A ] R =/= (/) ) )
13	1 5 12	pm5.21nii	|- ( A e. dom R <-> [ A ] R =/= (/) )