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

Theorem nfriota 7400
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 1804 . . 3 𝑦
2 nfriota.1 . . . 4 𝑥𝜑
32a1i 11 . . 3 (⊤ → Ⅎ𝑥𝜑)
4 nfriota.2 . . . 4 𝑥𝐴
54a1i 11 . . 3 (⊤ → 𝑥𝐴)
61, 3, 5nfriotadw 7396 . 2 (⊤ → 𝑥(𝑦𝐴 𝜑))
76mptru 1547 1 𝑥(𝑦𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wtru 1541  wnf 1783  wnfc 2890  crio 7387
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-v 3482  df-ss 3968  df-sn 4627  df-uni 4908  df-iota 6514  df-riota 7388
This theorem is referenced by:  csbriota  7403  nfoi  9554  lble  12220  nosupbnd1  27759  noinfbnd1  27774  riotasvd  38957  riotasv2d  38958  riotasv2s  38959  cdleme26ee  40362  cdleme31sn1  40383  cdlemefs32sn1aw  40416  cdleme43fsv1snlem  40422  cdleme41sn3a  40435  cdleme32d  40446  cdleme32f  40448  cdleme40m  40469  cdleme40n  40470  cdlemk36  40915  cdlemk38  40917  cdlemkid  40938  cdlemk19x  40945  cdlemk11t  40948
  Copyright terms: Public domain W3C validator