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

Theorem nfriota 6254
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 1609 . . 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 6253 . 2  |-  ( T. 
->  F/_ x ( iota_ y  e.  A  ph )
)
76trud 1388 1  |-  F/_ x
( iota_ y  e.  A  ph )
Colors of variables: wff setvar class
Syntax hints:   T. wtru 1380   F/wnf 1599   F/_wnfc 2615   iota_crio 6244
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-rex 2820  df-sn 4028  df-uni 4246  df-iota 5551  df-riota 6245
This theorem is referenced by:  csbriota  6257  nfoi  7939  lble  10495  riotasvd  33777  riotasv2d  33778  riotasv2s  33779  cdleme26ee  35174  cdleme31sn1  35195  cdlemefs32sn1aw  35228  cdleme43fsv1snlem  35234  cdleme41sn3a  35247  cdleme32d  35258  cdleme32f  35260  cdleme40m  35281  cdleme40n  35282  cdlemk36  35727  cdlemk38  35729  cdlemkid  35750  cdlemk19x  35757  cdlemk11t  35760
  Copyright terms: Public domain W3C validator