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

Theorem nfriota 7245
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 𝑥𝜑
nfriota.2 𝑥𝐴
Assertion
Ref Expression
nfriota 𝑥(𝑦𝐴 𝜑)
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥,𝑦)

Proof of Theorem nfriota
StepHypRef Expression
1 nftru 1807 . . 3 𝑦
2 nfriota.1 . . . 4 𝑥𝜑
32a1i 11 . . 3 (⊤ → Ⅎ𝑥𝜑)
4 nfriota.2 . . . 4 𝑥𝐴
54a1i 11 . . 3 (⊤ → 𝑥𝐴)
61, 3, 5nfriotadw 7240 . 2 (⊤ → 𝑥(𝑦𝐴 𝜑))
76mptru 1546 1 𝑥(𝑦𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wtru 1540  wnf 1786  wnfc 2887  crio 7231
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-v 3434  df-in 3894  df-ss 3904  df-sn 4562  df-uni 4840  df-iota 6391  df-riota 7232
This theorem is referenced by:  csbriota  7248  nfoi  9273  lble  11927  nosupbnd1  33917  noinfbnd1  33932  riotasvd  36970  riotasv2d  36971  riotasv2s  36972  cdleme26ee  38374  cdleme31sn1  38395  cdlemefs32sn1aw  38428  cdleme43fsv1snlem  38434  cdleme41sn3a  38447  cdleme32d  38458  cdleme32f  38460  cdleme40m  38481  cdleme40n  38482  cdlemk36  38927  cdlemk38  38929  cdlemkid  38950  cdlemk19x  38957  cdlemk11t  38960
  Copyright terms: Public domain W3C validator