Theorem nfriota 7389

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 1836	. . 3 ⊢ Ⅎ𝑦⊤
2		nfriota.1	. . . 4 ⊢ Ⅎ𝑥𝜑
3	2	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜑)
4		nfriota.2	. . . 4 ⊢ Ⅎ𝑥𝐴
5	4	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
6	1, 3, 5	nfriotadw 7385	. 2 ⊢ (⊤ → Ⅎ𝑥(℩𝑦 ∈ 𝐴 𝜑))
7	6	mptru 1576	1 ⊢ Ⅎ𝑥(℩𝑦 ∈ 𝐴 𝜑)

This proof depends on syntax axioms:  ⊤wtru 1570  Ⅎwnf 1815  Ⅎwnfc 2907  ℩crio 7376

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-v 3452  df-ss 3896  df-sn 4584  df-uni 4867  df-iota 6494  df-riota 7377

This theorem is used by:  csbriota  7392  nfoi  9509  lble  12270  nosupbnd1  28072  noinfbnd1  28087  riotasvd  40089  riotasv2d  40090  riotasv2s  40091  cdleme26ee  41493  cdleme31sn1  41514  cdlemefs32sn1aw  41547  cdleme43fsv1snlem  41553  cdleme41sn3a  41566  cdleme32d  41577  cdleme32f  41579  cdleme40m  41600  cdleme40n  41601  cdlemk36  42046  cdlemk38  42048  cdlemkid  42069  cdlemk19x  42076  cdlemk11t  42079