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