![]() |
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 2784 | . 2 ⊢ Ⅎ𝑥 𝑦 ∈ {𝑥 ∣ 𝜑} | |
2 | 1 | nfci 2936 | 1 ⊢ Ⅎ𝑥{𝑥 ∣ 𝜑} |
Colors of variables: wff setvar class |
Syntax hints: {cab 2775 Ⅎwnfc 2933 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-10 2112 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-ex 1762 df-nf 1766 df-sb 2043 df-clab 2776 df-nfc 2935 |
This theorem is referenced by: nfabd2 2970 nfabd2OLD 2971 abid2f 2980 abeq2f 2981 nfrab1 3344 elabgt 3601 elabgf 3602 elabg 3604 nfsbc1d 3724 ss2ab 3960 ab0 4253 abn0 4256 euabsn 4569 iunab 4874 iinab 4889 zfrep4 5091 sniota 6216 opabiotafun 6611 nfixp1 8330 scottexs 9162 scott0s 9163 cp 9166 ofpreima 30100 qqhval2 30840 esum2dlem 30968 sigaclcu2 30996 bnj1366 31718 bnj1321 31913 bnj1384 31918 currysetlem 33827 currysetlem1 33829 mptsnunlem 34150 topdifinffinlem 34159 scottabf 40073 compab 40313 ssfiunibd 41117 absnsb 42778 setrec2lem2 44277 |
Copyright terms: Public domain | W3C validator |