![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfab1 | Structured version Visualization version GIF version |
Description: Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Ref | Expression |
---|---|
nfab1 | ⊢ Ⅎ𝑥{𝑥 ∣ 𝜑} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfsab1 2709 | . 2 ⊢ Ⅎ𝑥 𝑦 ∈ {𝑥 ∣ 𝜑} | |
2 | 1 | nfci 2878 | 1 ⊢ Ⅎ𝑥{𝑥 ∣ 𝜑} |
Colors of variables: wff setvar class |
Syntax hints: {cab 2701 Ⅎwnfc 2875 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-10 2129 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-ex 1774 df-nf 1778 df-sb 2060 df-clab 2702 df-nfc 2877 |
This theorem is referenced by: nfabd2 2921 eqabf 2927 abid2fOLD 2929 nfrab1 3443 elabgtOLD 3655 elabgf 3656 elabgOLD 3659 nfsbc1d 3787 ss2ab 4048 ab0ALT 4368 abn0OLD 4373 euabsn 4722 iunab 5044 iinab 5061 zfrep4 5286 rnep 5916 sniota 6524 opabiotafun 6962 nfixp1 8907 scottexs 9877 scott0s 9878 cp 9881 symgval 19273 ofpreima 32314 algextdeglem6 33224 qqhval2 33417 esum2dlem 33545 sigaclcu2 33573 bnj1366 34295 bnj1321 34493 bnj1384 34498 currysetlem 36282 currysetlem1 36284 bj-reabeq 36364 mptsnunlem 36675 topdifinffinlem 36684 scottabf 43454 compab 43656 ssfiunibd 44470 absnsb 46188 setrec2lem2 47893 |
Copyright terms: Public domain | W3C validator |