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

Theorem nfriota 7142
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 1811 . . 3 𝑦
2 nfriota.1 . . . 4 𝑥𝜑
32a1i 11 . . 3 (⊤ → Ⅎ𝑥𝜑)
4 nfriota.2 . . . 4 𝑥𝐴
54a1i 11 . . 3 (⊤ → 𝑥𝐴)
61, 3, 5nfriotadw 7137 . 2 (⊤ → 𝑥(𝑦𝐴 𝜑))
76mptru 1549 1 𝑥(𝑦𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wtru 1543  wnf 1790  wnfc 2879  crio 7128
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-tru 1545  df-ex 1787  df-nf 1791  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ral 3058  df-rex 3059  df-v 3400  df-in 3850  df-ss 3860  df-sn 4517  df-uni 4797  df-iota 6297  df-riota 7129
This theorem is referenced by:  csbriota  7145  nfoi  9053  lble  11672  nosupbnd1  33562  noinfbnd1  33577  riotasvd  36615  riotasv2d  36616  riotasv2s  36617  cdleme26ee  38019  cdleme31sn1  38040  cdlemefs32sn1aw  38073  cdleme43fsv1snlem  38079  cdleme41sn3a  38092  cdleme32d  38103  cdleme32f  38105  cdleme40m  38126  cdleme40n  38127  cdlemk36  38572  cdlemk38  38574  cdlemkid  38595  cdlemk19x  38602  cdlemk11t  38605
  Copyright terms: Public domain W3C validator