Theorem nfriota 7385

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 7381	. 2 ⊢ (⊤ → Ⅎ𝑥(℩𝑦 ∈ 𝐴 𝜑))
7	6	mptru 1577	1 ⊢ Ⅎ𝑥(℩𝑦 ∈ 𝐴 𝜑)

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

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 2215  ax-ext 2734

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 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ral 3079  df-rex 3089  df-v 3455  df-ss 3919  df-sn 4588  df-uni 4871  df-iota 6493  df-riota 7373

This theorem is used by:  csbriota  7388  nfoi  9489  lble  12194  nosupbnd1  27951  noinfbnd1  27966  riotasvd  39831  riotasv2d  39832  riotasv2s  39833  cdleme26ee  41235  cdleme31sn1  41256  cdlemefs32sn1aw  41289  cdleme43fsv1snlem  41295  cdleme41sn3a  41308  cdleme32d  41319  cdleme32f  41321  cdleme40m  41342  cdleme40n  41343  cdlemk36  41788  cdlemk38  41790  cdlemkid  41811  cdlemk19x  41818  cdlemk11t  41821