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

Theorem nfriota 7118
 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 1798 . . 3 𝑦
2 nfriota.1 . . . 4 𝑥𝜑
32a1i 11 . . 3 (⊤ → Ⅎ𝑥𝜑)
4 nfriota.2 . . . 4 𝑥𝐴
54a1i 11 . . 3 (⊤ → 𝑥𝐴)
61, 3, 5nfriotadw 7114 . 2 (⊤ → 𝑥(𝑦𝐴 𝜑))
76mptru 1537 1 𝑥(𝑦𝐴 𝜑)
 Colors of variables: wff setvar class Syntax hints:  ⊤wtru 1531  Ⅎwnf 1777  Ⅎwnfc 2959  ℩crio 7105 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-rex 3142  df-sn 4560  df-uni 4831  df-iota 6307  df-riota 7106 This theorem is referenced by:  csbriota  7121  nfoi  8970  lble  11585  nosupbnd1  33207  riotasvd  36084  riotasv2d  36085  riotasv2s  36086  cdleme26ee  37488  cdleme31sn1  37509  cdlemefs32sn1aw  37542  cdleme43fsv1snlem  37548  cdleme41sn3a  37561  cdleme32d  37572  cdleme32f  37574  cdleme40m  37595  cdleme40n  37596  cdlemk36  38041  cdlemk38  38043  cdlemkid  38064  cdlemk19x  38071  cdlemk11t  38074
 Copyright terms: Public domain W3C validator