![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfsn | Structured version Visualization version GIF version |
Description: Bound-variable hypothesis builder for singletons. (Contributed by NM, 14-Nov-1995.) |
Ref | Expression |
---|---|
nfsn.1 | ⊢ Ⅎ𝑥𝐴 |
Ref | Expression |
---|---|
nfsn | ⊢ Ⅎ𝑥{𝐴} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfsn2 4479 | . 2 ⊢ {𝐴} = {𝐴, 𝐴} | |
2 | nfsn.1 | . . 3 ⊢ Ⅎ𝑥𝐴 | |
3 | 2, 2 | nfpr 4529 | . 2 ⊢ Ⅎ𝑥{𝐴, 𝐴} |
4 | 1, 3 | nfcxfr 2945 | 1 ⊢ Ⅎ𝑥{𝐴} |
Colors of variables: wff setvar class |
Syntax hints: Ⅎwnfc 2931 {csn 4466 {cpr 4468 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1775 ax-4 1789 ax-5 1886 ax-6 1945 ax-7 1990 ax-8 2081 ax-9 2089 ax-10 2110 ax-11 2124 ax-12 2139 ax-13 2342 ax-ext 2767 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1523 df-ex 1760 df-nf 1764 df-sb 2041 df-clab 2774 df-cleq 2786 df-clel 2861 df-nfc 2933 df-v 3434 df-un 3859 df-sn 4467 df-pr 4469 |
This theorem is referenced by: nfop 4720 iunopeqop 5295 nfpred 6020 nfsuc 6129 sniota 6208 dfmpo 7644 bnj958 31784 bnj1000 31785 bnj1446 31887 bnj1447 31888 bnj1448 31889 bnj1466 31895 bnj1467 31896 nosupbnd2 32770 nfaltop 32995 stoweidlem21 41802 stoweidlem47 41828 nfdfat 42796 |
Copyright terms: Public domain | W3C validator |