Theorem nfriota1 7322

Description: The abstraction variable in a restricted iota descriptor isn't free. (Contributed by NM, 12-Oct-2011.) (Revised by Mario Carneiro, 15-Oct-2016.)

Assertion

Ref	Expression
nfriota1	⊢ Ⅎ𝑥(℩𝑥 ∈ 𝐴 𝜑)

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem nfriota1

Step	Hyp	Ref	Expression
1		df-riota 7315	. 2 ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
2		nfiota1 6449	. 2 ⊢ Ⅎ𝑥(℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3	1, 2	nfcxfr 2895	1 ⊢ Ⅎ𝑥(℩𝑥 ∈ 𝐴 𝜑)

Syntax hints:   ∧ wa 395   ∈ wcel 2114  Ⅎwnfc 2882  ℩cio 6445  ℩crio 7314

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2183  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ral 3051  df-rex 3060  df-v 3441  df-ss 3917  df-sn 4580  df-uni 4863  df-iota 6447  df-riota 7315

This theorem is referenced by:  riotaprop  7342  riotass2  7345  riotass  7346  riotaxfrd  7349  ttrcltr  9627  lble  12096  riotaneg  12123  zriotaneg  12607  nosupbnd1  27684  nosupbnd2  27686  noinfbnd1  27699  noinfbnd2  27701  poimirlem26  37816  riotaocN  39504  ltrniotaval  40876  cdlemksv2  41142  cdlemkuv2  41162  cdlemk36  41208  disjinfi  45473