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 ⊢ Ⅎ 𝑥 𝐴
Assertion nfint Ⅎ 𝑥 ∩ 𝐴

Proof

Step Hyp Ref Expression
1 nfint.1 ⊢ Ⅎ 𝑥 𝐴
2 dfint2 ⊢ ∩ 𝐴 = { 𝑦 ∣ ∀ 𝑧 ∈ 𝐴 𝑦 ∈ 𝑧 }
3 nfv ⊢ Ⅎ 𝑥 𝑦 ∈ 𝑧
4 1 3 nfralw ⊢ Ⅎ 𝑥 ∀ 𝑧 ∈ 𝐴 𝑦 ∈ 𝑧
5 4 nfab ⊢ Ⅎ 𝑥 { 𝑦 ∣ ∀ 𝑧 ∈ 𝐴 𝑦 ∈ 𝑧 }
6 2 5 nfcxfr ⊢ Ⅎ 𝑥 ∩ 𝐴