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 | φ