Metamath Proof Explorer


Theorem nfint

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

Proof

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