Theorem nfriota 7377

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

Hypotheses

Ref	Expression
nfriota.1	⊢ Ⅎ𝑥𝜑
nfriota.2	⊢ Ⅎ𝑥𝐴

Assertion

Ref	Expression
nfriota	⊢ Ⅎ𝑥(℩𝑦 ∈ 𝐴 𝜑)

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥, 𝑦)   𝐴(𝑥, 𝑦)

Proof of Theorem nfriota

Step	Hyp	Ref	Expression
1		nftru 1837	. . 3 ⊢ Ⅎ𝑦⊤
2		nfriota.1	. . . 4 ⊢ Ⅎ𝑥𝜑
3	2	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜑)
4		nfriota.2	. . . 4 ⊢ Ⅎ𝑥𝐴
5	4	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
6	1, 3, 5	nfriotadw 7373	. 2 ⊢ (⊤ → Ⅎ𝑥(℩𝑦 ∈ 𝐴 𝜑))
7	6	mptru 1577	1 ⊢ Ⅎ𝑥(℩𝑦 ∈ 𝐴 𝜑)

This proof depends on syntax axioms:  ⊤wtru 1571  Ⅎwnf 1816  Ⅎwnfc 2907  ℩crio 7364

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-v 3452  df-ss 3915  df-sn 4584  df-uni 4867  df-iota 6483  df-riota 7365

This theorem is used by:  csbriota  7380  nfoi  9486  lble  12239  nosupbnd1  28005  noinfbnd1  28020  riotasvd  39933  riotasv2d  39934  riotasv2s  39935  cdleme26ee  41337  cdleme31sn1  41358  cdlemefs32sn1aw  41391  cdleme43fsv1snlem  41397  cdleme41sn3a  41410  cdleme32d  41421  cdleme32f  41423  cdleme40m  41444  cdleme40n  41445  cdlemk36  41890  cdlemk38  41892  cdlemkid  41913  cdlemk19x  41920  cdlemk11t  41923