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

Theorem nfriota 6577
 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 1727 . . 3 𝑦
2 nfriota.1 . . . 4 𝑥𝜑
32a1i 11 . . 3 (⊤ → Ⅎ𝑥𝜑)
4 nfriota.2 . . . 4 𝑥𝐴
54a1i 11 . . 3 (⊤ → 𝑥𝐴)
61, 3, 5nfriotad 6576 . 2 (⊤ → 𝑥(𝑦𝐴 𝜑))
76trud 1490 1 𝑥(𝑦𝐴 𝜑)
 Colors of variables: wff setvar class Syntax hints:  ⊤wtru 1481  Ⅎwnf 1705  Ⅎwnfc 2748  ℩crio 6567 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-sn 4151  df-uni 4405  df-iota 5812  df-riota 6568 This theorem is referenced by:  csbriota  6580  nfoi  8366  lble  10922  riotasvd  33743  riotasv2d  33744  riotasv2s  33745  cdleme26ee  35149  cdleme31sn1  35170  cdlemefs32sn1aw  35203  cdleme43fsv1snlem  35209  cdleme41sn3a  35222  cdleme32d  35233  cdleme32f  35235  cdleme40m  35256  cdleme40n  35257  cdlemk36  35702  cdlemk38  35704  cdlemkid  35725  cdlemk19x  35732  cdlemk11t  35735
 Copyright terms: Public domain W3C validator