Theorem nfriota 7400

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

Syntax hints:  ⊤wtru 1541  Ⅎwnf 1783  Ⅎwnfc 2890  ℩crio 7387

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-v 3482  df-ss 3968  df-sn 4627  df-uni 4908  df-iota 6514  df-riota 7388

This theorem is referenced by:  csbriota  7403  nfoi  9554  lble  12220  nosupbnd1  27759  noinfbnd1  27774  riotasvd  38957  riotasv2d  38958  riotasv2s  38959  cdleme26ee  40362  cdleme31sn1  40383  cdlemefs32sn1aw  40416  cdleme43fsv1snlem  40422  cdleme41sn3a  40435  cdleme32d  40446  cdleme32f  40448  cdleme40m  40469  cdleme40n  40470  cdlemk36  40915  cdlemk38  40917  cdlemkid  40938  cdlemk19x  40945  cdlemk11t  40948