![]() |
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 2285 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | nfi 1682 |
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 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-10 1932 ax-12 1950 ax-13 2104 |
This theorem depends on definitions: df-bi 190 df-an 378 df-ex 1672 df-nf 1676 df-sb 1806 |
This theorem is referenced by: mo3 2356 eu1 2359 2mo 2400 2eu6 2407 cbvralf 2999 cbvralsv 3016 cbvrexsv 3017 cbvrab 3029 sbhypf 3081 mob2 3206 reu2 3214 reu2eqd 3223 sbcralt 3328 sbcreu 3332 cbvreucsf 3383 cbvrabcsf 3384 sbcel12 3776 sbceqg 3777 csbif 3922 rabasiun 4273 cbvopab1 4466 cbvopab1s 4468 cbvmptf 4486 cbvmpt 4487 opelopabsb 4711 csbopab 4733 csbopabgALT 4734 opeliunxp 4891 ralxpf 4986 cbviota 5558 csbiota 5582 isarep1 5672 cbvriota 6280 csbriota 6282 onminex 6653 tfis 6700 findes 6742 abrexex2g 6789 abrexex2 6793 dfoprab4f 6870 axrepndlem1 9035 axrepndlem2 9036 uzind4s 11242 mo5f 28199 ac6sf2 28302 esumcvg 28981 bj-mo3OLD 31515 wl-lem-moexsb 31967 wl-mo3t 31975 poimirlem26 32030 sbcalf 32416 sbcexf 32417 sbcrexgOLD 35699 sbcel12gOLD 36975 2sb5nd 36997 2sb5ndALT 37392 opeliun2xp 40622 |
Copyright terms: Public domain | W3C validator |