Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nfriota | Structured version Visualization version GIF version |
Description: A variable not free in a wff remains so in a restricted iota descriptor. (Contributed by NM, 12-Oct-2011.) |
Ref | Expression |
---|---|
nfriota.1 | ⊢ Ⅎ𝑥𝜑 |
nfriota.2 | ⊢ Ⅎ𝑥𝐴 |
Ref | Expression |
---|---|
nfriota | ⊢ Ⅎ𝑥(℩𝑦 ∈ 𝐴 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nftru 1807 | . . 3 ⊢ Ⅎ𝑦⊤ | |
2 | nfriota.1 | . . . 4 ⊢ Ⅎ𝑥𝜑 | |
3 | 2 | a1i 11 | . . 3 ⊢ (⊤ → Ⅎ𝑥𝜑) |
4 | nfriota.2 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
5 | 4 | a1i 11 | . . 3 ⊢ (⊤ → Ⅎ𝑥𝐴) |
6 | 1, 3, 5 | nfriotadw 7240 | . 2 ⊢ (⊤ → Ⅎ𝑥(℩𝑦 ∈ 𝐴 𝜑)) |
7 | 6 | mptru 1546 | 1 ⊢ Ⅎ𝑥(℩𝑦 ∈ 𝐴 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ⊤wtru 1540 Ⅎwnf 1786 Ⅎwnfc 2887 ℩crio 7231 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-tru 1542 df-ex 1783 df-nf 1787 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ral 3069 df-rex 3070 df-v 3434 df-in 3894 df-ss 3904 df-sn 4562 df-uni 4840 df-iota 6391 df-riota 7232 |
This theorem is referenced by: csbriota 7248 nfoi 9273 lble 11927 nosupbnd1 33917 noinfbnd1 33932 riotasvd 36970 riotasv2d 36971 riotasv2s 36972 cdleme26ee 38374 cdleme31sn1 38395 cdlemefs32sn1aw 38428 cdleme43fsv1snlem 38434 cdleme41sn3a 38447 cdleme32d 38458 cdleme32f 38460 cdleme40m 38481 cdleme40n 38482 cdlemk36 38927 cdlemk38 38929 cdlemkid 38950 cdlemk19x 38957 cdlemk11t 38960 |
Copyright terms: Public domain | W3C validator |