![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfss | Structured version Visualization version Unicode version |
Description: If ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
dfss2f.1 |
![]() ![]() ![]() ![]() |
dfss2f.2 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nfss |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfss2f.1 |
. . 3
![]() ![]() ![]() ![]() | |
2 | dfss2f.2 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 1, 2 | dfss3f 3435 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | nfra1 2780 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | nfxfr 1706 |
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 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-tru 1457 df-ex 1674 df-nf 1678 df-sb 1808 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2591 df-ral 2753 df-in 3422 df-ss 3429 |
This theorem is referenced by: ssrexf 3503 nfpw 3974 ssiun2s 4335 triun 4523 ssopab2b 4741 nffr 4826 nfrel 4938 nffun 5622 nff 5746 fvmptss 5980 ssoprab2b 6374 tfis 6707 ovmptss 6903 nfwrecs 7055 oawordeulem 7280 nnawordex 7363 r1val1 8282 cardaleph 8545 nfsum1 13804 nfsum 13805 nfcprod1 14012 nfcprod 14013 iuncon 20491 ovolfiniun 22502 ovoliunlem3 22505 ovoliun 22506 ovoliun2 22507 ovoliunnul 22508 limciun 22897 ssiun2sf 28222 ssrelf 28269 funimass4f 28282 esumiun 28963 bnj1408 29893 totbndbnd 32165 ss2iundf 36295 iunconlem2 37371 stoweidlem53 37951 stoweidlem57 37955 opnvonmbllem2 38492 iunopeqop 39044 |
Copyright terms: Public domain | W3C validator |