Metamath Proof Explorer


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 ) )