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

Theorem nfriota 7373
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 7368 . 2 (⊤ → 𝑥(𝑦𝐴 𝜑))
76mptru 1549 1 𝑥(𝑦𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wtru 1543  wnf 1786  wnfc 2884  crio 7359
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 3954  df-ss 3964  df-sn 4628  df-uni 4908  df-iota 6492  df-riota 7360
This theorem is referenced by:  csbriota  7376  nfoi  9505  lble  12162  nosupbnd1  27197  noinfbnd1  27212  riotasvd  37764  riotasv2d  37765  riotasv2s  37766  cdleme26ee  39169  cdleme31sn1  39190  cdlemefs32sn1aw  39223  cdleme43fsv1snlem  39229  cdleme41sn3a  39242  cdleme32d  39253  cdleme32f  39255  cdleme40m  39276  cdleme40n  39277  cdlemk36  39722  cdlemk38  39724  cdlemkid  39745  cdlemk19x  39752  cdlemk11t  39755
  Copyright terms: Public domain W3C validator