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

Theorem nfriota 6241
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 1631 . . 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 6240 . 2  |-  ( T. 
->  F/_ x ( iota_ y  e.  A  ph )
)
76trud 1407 1  |-  F/_ x
( iota_ y  e.  A  ph )
Colors of variables: wff setvar class
Syntax hints:   T. wtru 1399   F/wnf 1621   F/_wnfc 2602   iota_crio 6231
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2809  df-rex 2810  df-sn 4017  df-uni 4236  df-iota 5534  df-riota 6232
This theorem is referenced by:  csbriota  6244  nfoi  7931  lble  10490  riotasvd  35084  riotasv2d  35085  riotasv2s  35086  cdleme26ee  36483  cdleme31sn1  36504  cdlemefs32sn1aw  36537  cdleme43fsv1snlem  36543  cdleme41sn3a  36556  cdleme32d  36567  cdleme32f  36569  cdleme40m  36590  cdleme40n  36591  cdlemk36  37036  cdlemk38  37038  cdlemkid  37059  cdlemk19x  37066  cdlemk11t  37069
  Copyright terms: Public domain W3C validator