Theorem elqsg

Description: Closed form of elqs . (Contributed by Rodolfo Medina, 12-Oct-2010)

	Ref	Expression
Assertion	elqsg	|- ( B e. V -> ( B e. ( A /. R ) <-> E. x e. A B = [ x ] R ) )

Proof

Step	Hyp	Ref	Expression
1		eqeq1	|- ( y = B -> ( y = [ x ] R <-> B = [ x ] R ) )
2	1	rexbidv	|- ( y = B -> ( E. x e. A y = [ x ] R <-> E. x e. A B = [ x ] R ) )
3		df-qs	|- ( A /. R ) = { y | E. x e. A y = [ x ] R }
4	2 3	elab2g	|- ( B e. V -> ( B e. ( A /. R ) <-> E. x e. A B = [ x ] R ) )