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

Metamath Proof Explorer

Theorem nfunid

Description: Deduction version of nfuni . (Contributed by NM, 18-Feb-2013)

Ref Expression
Hypothesis nfunid.3 ⊢ φ → Ⅎ _ x A
Assertion nfunid ⊢ φ → Ⅎ _ x ⋃ A

Proof

Step Hyp Ref Expression
1 nfunid.3 ⊢ φ → Ⅎ _ x A
2 dfuni2 ⊢ ⋃ A = y | ∃ z ∈ A y ∈ z
3 nfv ⊢ Ⅎ y φ
4 nfv ⊢ Ⅎ z φ
5 nfvd ⊢ φ → Ⅎ x y ∈ z
6 4 1 5 nfrexdw ⊢ φ → Ⅎ x ∃ z ∈ A y ∈ z
7 3 6 nfabdw ⊢ φ → Ⅎ _ x y | ∃ z ∈ A y ∈ z
8 2 7 nfcxfrd ⊢ φ → Ⅎ _ x ⋃ A