![]() |
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 4636 | . 2 ⊢ {𝐴} = {𝐴, 𝐴} | |
2 | nfsn.1 | . . 3 ⊢ Ⅎ𝑥𝐴 | |
3 | 2, 2 | nfpr 4689 | . 2 ⊢ Ⅎ𝑥{𝐴, 𝐴} |
4 | 1, 3 | nfcxfr 2890 | 1 ⊢ Ⅎ𝑥{𝐴} |
Colors of variables: wff setvar class |
Syntax hints: Ⅎwnfc 2876 {csn 4623 {cpr 4625 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-tru 1537 df-ex 1775 df-nf 1779 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-v 3464 df-un 3951 df-sn 4624 df-pr 4626 |
This theorem is referenced by: nfop 4887 iunopeqop 5519 nfpred 6309 nfsuc 6440 sniota 6537 dfmpo 8108 nosupbnd2 27743 noinfbnd2 27758 bnj958 34798 bnj1000 34799 bnj1446 34903 bnj1447 34904 bnj1448 34905 bnj1466 34911 bnj1467 34912 nfaltop 35817 stoweidlem21 45678 stoweidlem47 45704 nfdfat 46776 |
Copyright terms: Public domain | W3C validator |