Theorem nfriota1 7381

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

This proof depends on syntax axioms:   ∧ wa 401   ∈ wcel 2145  Ⅎwnfc 2909  ℩cio 6491  ℩crio 7373

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ral 3079  df-rex 3089  df-v 3455  df-ss 3919  df-sn 4588  df-uni 4871  df-iota 6493  df-riota 7374

This theorem is used by:  riotaprop  7401  riotass2  7404  riotass  7405  riotaxfrd  7408  ttrcltr  9699  lble  12195  riotaneg  12222  zriotaneg  12738  nosupbnd1  27958  nosupbnd2  27960  noinfbnd1  27973  noinfbnd2  27975  poimirlem26  38403  riotaocN  40090  ltrniotaval  41462  cdlemksv2  41728  cdlemkuv2  41748  cdlemk36  41794  disjinfi  46032