Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > nfab | GIF version |
Description: Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Ref | Expression |
---|---|
nfab.1 | ⊢ Ⅎ𝑥𝜑 |
Ref | Expression |
---|---|
nfab | ⊢ Ⅎ𝑥{𝑦 ∣ 𝜑} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfab.1 | . . 3 ⊢ Ⅎ𝑥𝜑 | |
2 | 1 | nfsab 2032 | . 2 ⊢ Ⅎ𝑥 𝑧 ∈ {𝑦 ∣ 𝜑} |
3 | 2 | nfci 2168 | 1 ⊢ Ⅎ𝑥{𝑦 ∣ 𝜑} |
Colors of variables: wff set class |
Syntax hints: Ⅎwnf 1349 {cab 2026 Ⅎwnfc 2165 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-io 630 ax-5 1336 ax-7 1337 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-8 1395 ax-10 1396 ax-11 1397 ax-i12 1398 ax-bndl 1399 ax-4 1400 ax-17 1419 ax-i9 1423 ax-ial 1427 ax-i5r 1428 |
This theorem depends on definitions: df-bi 110 df-nf 1350 df-sb 1646 df-clab 2027 df-nfc 2167 |
This theorem is referenced by: nfaba1 2183 nfrabxy 2490 sbcel12g 2865 sbceqg 2866 nfun 3099 nfpw 3371 nfpr 3420 nfop 3565 nfuni 3586 nfint 3625 intab 3644 nfiunxy 3683 nfiinxy 3684 nfiunya 3685 nfiinya 3686 nfiu1 3687 nfii1 3688 nfopab 3825 nfopab1 3826 nfopab2 3827 repizf2 3915 nfdm 4578 fun11iun 5147 eusvobj2 5498 nfoprab1 5554 nfoprab2 5555 nfoprab3 5556 nfoprab 5557 nfrecs 5922 nffrec 5982 |
Copyright terms: Public domain | W3C validator |