Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nf5i | Structured version Visualization version Unicode version |
Description: Deduce that is not free in from the definition. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Ref | Expression |
---|---|
nf5i.1 |
Ref | Expression |
---|---|
nf5i |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nf5-1 2023 | . 2 | |
2 | nf5i.1 | . 2 | |
3 | 1, 2 | mpg 1724 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wal 1481 wnf 1708 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-10 2019 |
This theorem depends on definitions: df-bi 197 df-ex 1705 df-nf 1710 |
This theorem is referenced by: nfe1 2027 nf5di 2119 19.9h 2120 19.21h 2121 19.23h 2122 equsexhv 2124 hban 2128 hb3an 2129 exlimih 2148 exlimdh 2149 nfal 2153 nfexOLD 2155 hbex 2156 nfa1OLD 2157 dvelimhw 2173 cbv3hv 2174 cbv3h 2266 equsalh 2294 equsexh 2295 nfae 2316 axc16i 2322 dvelimh 2336 nfs1 2365 sbh 2381 nfs1v 2437 hbsb 2441 sb7h 2454 nfsab1 2612 nfsab 2614 cleqh 2724 nfcii 2755 nfcri 2758 bnj596 30816 bnj1146 30862 bnj1379 30901 bnj1464 30914 bnj1468 30916 bnj605 30977 bnj607 30986 bnj916 31003 bnj964 31013 bnj981 31020 bnj983 31021 bnj1014 31030 bnj1123 31054 bnj1373 31098 bnj1417 31109 bnj1445 31112 bnj1463 31123 bnj1497 31128 bj-cbv3hv2 32728 bj-equsalhv 32744 bj-nfs1v 32759 bj-nfsab1 32772 bj-nfcri 32852 wl-nfalv 33312 nfequid-o 34195 nfa1-o 34200 2sb5ndVD 39146 2sb5ndALT 39168 |
Copyright terms: Public domain | W3C validator |