![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfab | Structured version Visualization version 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 2764 | . 2 ⊢ Ⅎ𝑥 𝑧 ∈ {𝑦 ∣ 𝜑} |
3 | 2 | nfci 2913 | 1 ⊢ Ⅎ𝑥{𝑦 ∣ 𝜑} |
Colors of variables: wff setvar class |
Syntax hints: Ⅎwnf 1746 {cab 2752 Ⅎwnfc 2910 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-clab 2753 df-nfc 2912 |
This theorem is referenced by: nfaba1 2933 nfun 4024 sbcel12 4240 sbceqg 4241 nfpw 4430 nfpr 4498 nfuni 4714 nfint 4755 intab 4775 nfiun 4817 nfiin 4818 nfiu1 4819 nfii1 4820 nfopab 4993 nfopab1 4994 nfopab2 4995 nfdm 5663 eusvobj2 6967 nfoprab1 7032 nfoprab2 7033 nfoprab3 7034 nfoprab 7035 fun11iun 7456 nfwrecs 7750 nfixp 8276 nfixp1 8277 reclem2pr 10266 nfwrd 13703 mreiincl 16737 lss1d 19469 disjabrex 30112 disjabrexf 30113 esumc 30983 bnj900 31877 bnj1014 31908 bnj1123 31932 bnj1307 31969 bnj1398 31980 bnj1444 31989 bnj1445 31990 bnj1446 31991 bnj1447 31992 bnj1467 32000 bnj1518 32010 bnj1519 32011 dfon2lem3 32579 nffrecs 32670 sdclem1 34489 heibor1 34559 dihglblem5 37908 ssfiunibd 41030 hoidmvlelem1 42333 nfsetrecs 44181 setrec2lem2 44189 setrec2 44190 |
Copyright terms: Public domain | W3C validator |