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 2722 | . 2 ⊢ Ⅎ𝑥 𝑦 ∈ {𝑥 ∣ 𝜑} | |
2 | 1 | nfci 2887 | 1 ⊢ Ⅎ𝑥{𝑥 ∣ 𝜑} |
Colors of variables: wff setvar class |
Syntax hints: {cab 2714 Ⅎwnfc 2884 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-10 2141 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-ex 1788 df-nf 1792 df-sb 2071 df-clab 2715 df-nfc 2886 |
This theorem is referenced by: nfabd2 2930 abid2f 2936 abeq2f 2937 nfrab1 3296 elabgtOLD 3582 elabgf 3583 elabgOLD 3586 nfsbc1d 3712 ss2ab 3973 ab0ALT 4291 abn0OLD 4296 euabsn 4642 iunab 4960 iinab 4976 zfrep4 5189 rnep 5796 sniota 6371 opabiotafun 6792 nfixp1 8599 scottexs 9503 scott0s 9504 cp 9507 symgval 18761 ofpreima 30722 qqhval2 31644 esum2dlem 31772 sigaclcu2 31800 bnj1366 32522 bnj1321 32720 bnj1384 32725 currysetlem 34871 currysetlem1 34873 bj-reabeq 34954 mptsnunlem 35246 topdifinffinlem 35255 scottabf 41531 compab 41733 ssfiunibd 42521 absnsb 44193 setrec2lem2 46071 |
Copyright terms: Public domain | W3C validator |