Theorem nfriota1 7333

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

Syntax hints:   ∧ wa 395   ∈ wcel 2109  Ⅎwnfc 2876  ℩cio 6450  ℩crio 7325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-v 3446  df-ss 3928  df-sn 4586  df-uni 4868  df-iota 6452  df-riota 7326

This theorem is referenced by:  riotaprop  7353  riotass2  7356  riotass  7357  riotaxfrd  7360  ttrcltr  9645  lble  12111  riotaneg  12138  zriotaneg  12623  nosupbnd1  27659  nosupbnd2  27661  noinfbnd1  27674  noinfbnd2  27676  poimirlem26  37633  riotaocN  39195  ltrniotaval  40568  cdlemksv2  40834  cdlemkuv2  40854  cdlemk36  40900  disjinfi  45179