Description: Bound-variable hypothesis builder for set-like relations. (Contributed by Mario Carneiro, 24-Jun-2015) (Revised by Mario Carneiro, 14-Oct-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | nffr.r | |- F/_ x R |
|
nffr.a | |- F/_ x A |
||
Assertion | nfse | |- F/ x R Se A |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nffr.r | |- F/_ x R |
|
2 | nffr.a | |- F/_ x A |
|
3 | df-se | |- ( R Se A <-> A. b e. A { a e. A | a R b } e. _V ) |
|
4 | nfcv | |- F/_ x a |
|
5 | nfcv | |- F/_ x b |
|
6 | 4 1 5 | nfbr | |- F/ x a R b |
7 | 6 2 | nfrabw | |- F/_ x { a e. A | a R b } |
8 | 7 | nfel1 | |- F/ x { a e. A | a R b } e. _V |
9 | 2 8 | nfralw | |- F/ x A. b e. A { a e. A | a R b } e. _V |
10 | 3 9 | nfxfr | |- F/ x R Se A |