Theorem nfriota1 7116

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 7109	. 2 ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
2		nfiota1 6297	. 2 ⊢ Ⅎ𝑥(℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3	1, 2	nfcxfr 2918	1 ⊢ Ⅎ𝑥(℩𝑥 ∈ 𝐴 𝜑)

Syntax hints:   ∧ wa 400   ∈ wcel 2112  Ⅎwnfc 2900  ℩cio 6293  ℩crio 7108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ral 3076  df-rex 3077  df-v 3412  df-in 3866  df-ss 3876  df-sn 4524  df-uni 4800  df-iota 6295  df-riota 7109

This theorem is referenced by:  riotaprop  7136  riotass2  7139  riotass  7140  riotaxfrd  7143  lble  11630  riotaneg  11657  zriotaneg  12136  nosupbnd1  33483  nosupbnd2  33485  noinfbnd1  33498  noinfbnd2  33500  poimirlem26  35364  riotaocN  36786  ltrniotaval  38158  cdlemksv2  38424  cdlemkuv2  38444  cdlemk36  38490  disjinfi  42191