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

Theorem nfriota 7378
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 7373 . 2 (⊤ → 𝑥(𝑦𝐴 𝜑))
76mptru 1549 1 𝑥(𝑦𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wtru 1543  wnf 1786  wnfc 2884  crio 7364
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 2704
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 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-rex 3072  df-v 3477  df-in 3956  df-ss 3966  df-sn 4630  df-uni 4910  df-iota 6496  df-riota 7365
This theorem is referenced by:  csbriota  7381  nfoi  9509  lble  12166  nosupbnd1  27217  noinfbnd1  27232  riotasvd  37874  riotasv2d  37875  riotasv2s  37876  cdleme26ee  39279  cdleme31sn1  39300  cdlemefs32sn1aw  39333  cdleme43fsv1snlem  39339  cdleme41sn3a  39352  cdleme32d  39363  cdleme32f  39365  cdleme40m  39386  cdleme40n  39387  cdlemk36  39832  cdlemk38  39834  cdlemkid  39855  cdlemk19x  39862  cdlemk11t  39865
  Copyright terms: Public domain W3C validator