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

Metamath Proof Explorer

Theorem nfriota

Description: A variable not free in a wff remains so in a restricted iota descriptor. (Contributed by NM, 12-Oct-2011)

Ref Expression
Hypotheses nfriota.1 ⊢ Ⅎ x φ
nfriota.2 ⊢ Ⅎ _ x A
Assertion nfriota ⊢ Ⅎ _ x ι y ∈ A | φ

Proof

Step Hyp Ref Expression
1 nfriota.1 ⊢ Ⅎ x φ
2 nfriota.2 ⊢ Ⅎ _ x A
3 nftru ⊢ Ⅎ y ⊤
4 1 a1i ⊢ ⊤ → Ⅎ x φ
5 2 a1i ⊢ ⊤ → Ⅎ _ x A
6 3 4 5 nfriotadw ⊢ ⊤ → Ⅎ _ x ι y ∈ A | φ
7 6 mptru ⊢ Ⅎ _ x ι y ∈ A | φ