Theorem nfriota1 7384

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

This proof depends on syntax axioms:   ∧ wa 401   ∈ wcel 2144  Ⅎwnfc 2907  ℩cio 6492  ℩crio 7376

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-v 3452  df-ss 3896  df-sn 4584  df-uni 4867  df-iota 6494  df-riota 7377

This theorem is used by:  riotaprop  7404  riotass2  7407  riotass  7408  riotaxfrd  7411  ttrcltr  9717  lble  12269  riotaneg  12296  zriotaneg  12812  nosupbnd1  28071  nosupbnd2  28073  noinfbnd1  28086  noinfbnd2  28088  poimirlem26  38565  riotaocN  40267  ltrniotaval  41639  cdlemksv2  41905  cdlemkuv2  41925  cdlemk36  41971  disjinfi  46207