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

Theorem nfriota 6783
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 1879 . . 3 𝑦
2 nfriota.1 . . . 4 𝑥𝜑
32a1i 11 . . 3 (⊤ → Ⅎ𝑥𝜑)
4 nfriota.2 . . . 4 𝑥𝐴
54a1i 11 . . 3 (⊤ → 𝑥𝐴)
61, 3, 5nfriotad 6782 . 2 (⊤ → 𝑥(𝑦𝐴 𝜑))
76trud 1642 1 𝑥(𝑦𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wtru 1633  wnf 1857  wnfc 2889  crio 6773
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-sn 4322  df-uni 4589  df-iota 6012  df-riota 6774
This theorem is referenced by:  csbriota  6786  nfoi  8584  lble  11167  nosupbnd1  32166  riotasvd  34745  riotasv2d  34746  riotasv2s  34747  cdleme26ee  36150  cdleme31sn1  36171  cdlemefs32sn1aw  36204  cdleme43fsv1snlem  36210  cdleme41sn3a  36223  cdleme32d  36234  cdleme32f  36236  cdleme40m  36257  cdleme40n  36258  cdlemk36  36703  cdlemk38  36705  cdlemkid  36726  cdlemk19x  36733  cdlemk11t  36736
  Copyright terms: Public domain W3C validator