Theorem nfriota1 7376

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

This proof depends on syntax axioms:   ∧ wa 400   ∈ wcel 2142  Ⅎwnfc 2909  ℩cio 6490  ℩crio 7368

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1572  df-ex 1809  df-nf 1813  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ral 3079  df-rex 3089  df-v 3456  df-ss 3921  df-sn 4589  df-uni 4872  df-iota 6492  df-riota 7369

This theorem is used by:  riotaprop  7396  riotass2  7399  riotass  7400  riotaxfrd  7403  ttrcltr  9683  lble  12173  riotaneg  12200  zriotaneg  12715  nosupbnd1  27889  nosupbnd2  27891  noinfbnd1  27904  noinfbnd2  27906  poimirlem26  38325  riotaocN  40011  ltrniotaval  41383  cdlemksv2  41649  cdlemkuv2  41669  cdlemk36  41715  disjinfi  45938