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

Theorem nfriota 6066
Description: A variable not free in a wff remains so in a restricted iota descriptor. (Contributed by NM, 12-Oct-2011.)
Hypotheses
Ref Expression
nfriota.1  |-  F/ x ph
nfriota.2  |-  F/_ x A
Assertion
Ref Expression
nfriota  |-  F/_ x
( iota_ y  e.  A  ph )
Distinct variable group:    x, y
Allowed substitution hints:    ph( x, y)    A( x, y)

Proof of Theorem nfriota
StepHypRef Expression
1 nftru 1599 . . 3  |-  F/ y T.
2 nfriota.1 . . . 4  |-  F/ x ph
32a1i 11 . . 3  |-  ( T. 
->  F/ x ph )
4 nfriota.2 . . . 4  |-  F/_ x A
54a1i 11 . . 3  |-  ( T. 
->  F/_ x A )
61, 3, 5nfriotad 6065 . 2  |-  ( T. 
->  F/_ x ( iota_ y  e.  A  ph )
)
76trud 1378 1  |-  F/_ x
( iota_ y  e.  A  ph )
Colors of variables: wff setvar class
Syntax hints:   T. wtru 1370   F/wnf 1589   F/_wnfc 2571   iota_crio 6056
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ral 2725  df-rex 2726  df-sn 3883  df-uni 4097  df-iota 5386  df-riota 6057
This theorem is referenced by:  csbriota  6069  nfoi  7733  lble  10287  riotasvd  32612  riotasv2d  32613  riotasv2s  32614  cdleme26ee  34009  cdleme31sn1  34030  cdlemefs32sn1aw  34063  cdleme43fsv1snlem  34069  cdleme41sn3a  34082  cdleme32d  34093  cdleme32f  34095  cdleme40m  34116  cdleme40n  34117  cdlemk36  34562  cdlemk38  34564  cdlemkid  34585  cdlemk19x  34592  cdlemk11t  34595
  Copyright terms: Public domain W3C validator