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 _ x A
Assertion nfint _ x A

Proof

Step Hyp Ref Expression
1 nfint.1 _ x A
2 dfint2 A = y | z A y z
3 nfv x y z
4 1 3 nfralw x z A y z
5 4 nfab _ x y | z A y z
6 2 5 nfcxfr _ x A