![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfs1v | Structured version Visualization version Unicode version |
Description: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nfs1v |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hbs1 2265 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | nfi 1674 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-10 1915 ax-12 1933 ax-13 2091 |
This theorem depends on definitions: df-bi 189 df-an 373 df-ex 1664 df-nf 1668 df-sb 1798 |
This theorem is referenced by: mo3 2336 eu1 2339 2mo 2380 2eu6 2387 cbvralf 3013 cbvralsv 3030 cbvrexsv 3031 cbvrab 3043 sbhypf 3095 mob2 3218 reu2 3226 reu2eqd 3235 sbcralt 3340 sbcreu 3344 cbvreucsf 3397 cbvrabcsf 3398 sbcel12 3772 sbceqg 3773 csbif 3931 rabasiun 4282 cbvopab1 4473 cbvopab1s 4475 cbvmptf 4493 cbvmpt 4494 opelopabsb 4711 csbopab 4733 csbopabgALT 4734 opeliunxp 4886 ralxpf 4981 cbviota 5551 csbiota 5575 isarep1 5662 cbvriota 6262 csbriota 6264 onminex 6634 tfis 6681 findes 6723 abrexex2g 6770 abrexex2 6774 dfoprab4f 6851 axrepndlem1 9017 axrepndlem2 9018 uzind4s 11219 mo5f 28120 ac6sf2 28226 esumcvg 28907 bj-mo3OLD 31447 wl-lem-moexsb 31897 wl-mo3t 31905 poimirlem26 31966 sbcalf 32352 sbcexf 32353 sbcrexgOLD 35628 sbcel12gOLD 36905 2sb5nd 36927 2sb5ndALT 37329 opeliun2xp 40167 |
Copyright terms: Public domain | W3C validator |