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

Theorem nfriota 7380
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 1806 . . 3 𝑦
2 nfriota.1 . . . 4 𝑥𝜑
32a1i 11 . . 3 (⊤ → Ⅎ𝑥𝜑)
4 nfriota.2 . . . 4 𝑥𝐴
54a1i 11 . . 3 (⊤ → 𝑥𝐴)
61, 3, 5nfriotadw 7375 . 2 (⊤ → 𝑥(𝑦𝐴 𝜑))
76mptru 1548 1 𝑥(𝑦𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wtru 1542  wnf 1785  wnfc 2883  crio 7366
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  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 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-rex 3071  df-v 3476  df-in 3955  df-ss 3965  df-sn 4629  df-uni 4909  df-iota 6495  df-riota 7367
This theorem is referenced by:  csbriota  7383  nfoi  9511  lble  12170  nosupbnd1  27441  noinfbnd1  27456  riotasvd  38129  riotasv2d  38130  riotasv2s  38131  cdleme26ee  39534  cdleme31sn1  39555  cdlemefs32sn1aw  39588  cdleme43fsv1snlem  39594  cdleme41sn3a  39607  cdleme32d  39618  cdleme32f  39620  cdleme40m  39641  cdleme40n  39642  cdlemk36  40087  cdlemk38  40089  cdlemkid  40110  cdlemk19x  40117  cdlemk11t  40120
  Copyright terms: Public domain W3C validator