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

Theorem nfriota 7327
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 7322 . 2 (⊤ → 𝑥(𝑦𝐴 𝜑))
76mptru 1549 1 𝑥(𝑦𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wtru 1543  wnf 1786  wnfc 2888  crio 7313
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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ral 3066  df-rex 3075  df-v 3448  df-in 3918  df-ss 3928  df-sn 4588  df-uni 4867  df-iota 6449  df-riota 7314
This theorem is referenced by:  csbriota  7330  nfoi  9451  lble  12108  nosupbnd1  27065  noinfbnd1  27080  riotasvd  37421  riotasv2d  37422  riotasv2s  37423  cdleme26ee  38826  cdleme31sn1  38847  cdlemefs32sn1aw  38880  cdleme43fsv1snlem  38886  cdleme41sn3a  38899  cdleme32d  38910  cdleme32f  38912  cdleme40m  38933  cdleme40n  38934  cdlemk36  39379  cdlemk38  39381  cdlemkid  39402  cdlemk19x  39409  cdlemk11t  39412
  Copyright terms: Public domain W3C validator