Theorem nfriota 7412

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091  df-v 3456  df-ss 3901  df-sn 4589  df-uni 4871  df-iota 6512  df-riota 7400

This theorem is used by:  csbriota  7415  nfoi  9535  lble  12296  nosupbnd1  28101  noinfbnd1  28116  riotasvd  40205  riotasv2d  40206  riotasv2s  40207  cdleme26ee  41609  cdleme31sn1  41630  cdlemefs32sn1aw  41663  cdleme43fsv1snlem  41669  cdleme41sn3a  41682  cdleme32d  41693  cdleme32f  41695  cdleme40m  41716  cdleme40n  41717  cdlemk36  42162  cdlemk38  42164  cdlemkid  42185  cdlemk19x  42192  cdlemk11t  42195