Theorem nfriota1 6618

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	|- F/_ x ( iota_ x e. A ph )

Distinct variable group:   x, A

Allowed substitution hint:   ph( x)

Proof of Theorem nfriota1

Step	Hyp	Ref	Expression
1		df-riota 6611	. 2 |- ( iota_ x e. A ph ) = ( iota x ( x e. A /\ ph ) )
2		nfiota1 5853	. 2 |- F/_ x ( iota x ( x e. A /\ ph ) )
3	1, 2	nfcxfr 2762	1 |- F/_ x ( iota_ x e. A ph )

Syntax hints:   /\ wa 384   e. wcel 1990   F/_wnfc 2751   iotacio 5849   iota_crio 6610

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-sn 4178  df-uni 4437  df-iota 5851  df-riota 6611

This theorem is referenced by:  riotaprop  6635  riotass2  6638  riotass  6639  riotaxfrd  6642  lble  10975  riotaneg  11002  zriotaneg  11491  nosupbnd1  31860  nosupbnd2  31862  poimirlem26  33435  riotaocN  34496  ltrniotaval  35869  cdlemksv2  36135  cdlemkuv2  36155  cdlemk36  36201  wessf1ornlem  39371  disjinfi  39380