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 1801	. . 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 1544	1 ⊢ Ⅎ𝑥(℩𝑦 ∈ 𝐴 𝜑)

Syntax hints:  ⊤wtru 1538  Ⅎwnf 1780  Ⅎwnfc 2888  ℩crio 7387

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-nf 1781  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ral 3060  df-rex 3069  df-v 3480  df-ss 3980  df-sn 4632  df-uni 4913  df-iota 6516  df-riota 7388

This theorem is referenced by:  csbriota  7403  nfoi  9552  lble  12218  nosupbnd1  27774  noinfbnd1  27789  riotasvd  38938  riotasv2d  38939  riotasv2s  38940  cdleme26ee  40343  cdleme31sn1  40364  cdlemefs32sn1aw  40397  cdleme43fsv1snlem  40403  cdleme41sn3a  40416  cdleme32d  40427  cdleme32f  40429  cdleme40m  40450  cdleme40n  40451  cdlemk36  40896  cdlemk38  40898  cdlemkid  40919  cdlemk19x  40926  cdlemk11t  40929