Metamath Proof Explorer


Theorem nfse

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

Proof

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