Description: Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011) (Revised by Mario Carneiro, 7-Oct-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | nfnel.1 | |
|
nfnel.2 | |
||
Assertion | nfnel | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfnel.1 | |
|
2 | nfnel.2 | |
|
3 | df-nel | |
|
4 | 1 2 | nfel | |
5 | 4 | nfn | |
6 | 3 5 | nfxfr | |