MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfriota1 Structured version   Unicode version

Theorem nfriota1 6270
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
StepHypRef Expression
1 df-riota 6263 . 2  |-  ( iota_ x  e.  A  ph )  =  ( iota x
( x  e.  A  /\  ph ) )
2 nfiota1 5563 . 2  |-  F/_ x
( iota x ( x  e.  A  /\  ph ) )
31, 2nfcxfr 2582 1  |-  F/_ x
( iota_ x  e.  A  ph )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 370    e. wcel 1868   F/_wnfc 2570   iotacio 5559   iota_crio 6262
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ral 2780  df-rex 2781  df-sn 3997  df-uni 4217  df-iota 5561  df-riota 6263
This theorem is referenced by:  riotaprop  6286  riotass2  6289  riotass  6290  riotaxfrd  6293  lble  10558  riotaneg  10586  zriotaneg  11049  poimirlem26  31877  riotaocN  32691  ltrniotaval  34064  cdlemksv2  34330  cdlemkuv2  34350  cdlemk36  34396  wessf1ornlem  37306  disjinfi  37315
  Copyright terms: Public domain W3C validator