This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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