Description: Bound-variable hypothesis builder for intersection. (Contributed by NM, 2-Feb-1997) (Proof shortened by Andrew Salmon, 12-Aug-2011)
Ref | Expression | ||
---|---|---|---|
Hypothesis | nfint.1 | |- F/_ x A |
|
Assertion | nfint | |- F/_ x |^| A |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfint.1 | |- F/_ x A |
|
2 | dfint2 | |- |^| A = { y | A. z e. A y e. z } |
|
3 | nfv | |- F/ x y e. z |
|
4 | 1 3 | nfralw | |- F/ x A. z e. A y e. z |
5 | 4 | nfab | |- F/_ x { y | A. z e. A y e. z } |
6 | 2 5 | nfcxfr | |- F/_ x |^| A |