Theorem nfriota 7379

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

Syntax hints:  ⊤wtru 1569  Ⅎwnf 1811  Ⅎwnfc 2908  ℩crio 7366

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1571  df-ex 1808  df-nf 1812  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rex 3088  df-v 3455  df-ss 3921  df-sn 4589  df-uni 4872  df-iota 6492  df-riota 7367

This theorem is referenced by:  csbriota  7382  nfoi  9475  lble  12166  nosupbnd1  27854  noinfbnd1  27869  riotasvd  39698  riotasv2d  39699  riotasv2s  39700  cdleme26ee  41102  cdleme31sn1  41123  cdlemefs32sn1aw  41156  cdleme43fsv1snlem  41162  cdleme41sn3a  41175  cdleme32d  41186  cdleme32f  41188  cdleme40m  41209  cdleme40n  41210  cdlemk36  41655  cdlemk38  41657  cdlemkid  41678  cdlemk19x  41685  cdlemk11t  41688