![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfriota1 | Structured version Visualization version GIF version |
Description: The abstraction variable in a restricted iota descriptor isn't free. (Contributed by NM, 12-Oct-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) |
Ref | Expression |
---|---|
nfriota1 | ⊢ Ⅎ𝑥(℩𝑥 ∈ 𝐴 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-riota 7314 | . 2 ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
2 | nfiota1 6451 | . 2 ⊢ Ⅎ𝑥(℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
3 | 1, 2 | nfcxfr 2906 | 1 ⊢ Ⅎ𝑥(℩𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 397 ∈ wcel 2107 Ⅎwnfc 2888 ℩cio 6447 ℩crio 7313 |
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 2708 |
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 2715 df-cleq 2729 df-clel 2815 df-nfc 2890 df-ral 3066 df-rex 3075 df-v 3448 df-in 3918 df-ss 3928 df-sn 4588 df-uni 4867 df-iota 6449 df-riota 7314 |
This theorem is referenced by: riotaprop 7342 riotass2 7345 riotass 7346 riotaxfrd 7349 ttrcltr 9653 lble 12108 riotaneg 12135 zriotaneg 12617 nosupbnd1 27065 nosupbnd2 27067 noinfbnd1 27080 noinfbnd2 27082 poimirlem26 36107 riotaocN 37674 ltrniotaval 39047 cdlemksv2 39313 cdlemkuv2 39333 cdlemk36 39379 disjinfi 43419 |
Copyright terms: Public domain | W3C validator |