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.) Add disjoint variable condition to avoid ax-13 2390. See nfabg 2985 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024.) |
Ref | Expression |
---|---|
nfab.1 | ⊢ Ⅎ𝑥𝜑 |
Ref | Expression |
---|---|
nfab | ⊢ Ⅎ𝑥{𝑦 ∣ 𝜑} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfab.1 | . . 3 ⊢ Ⅎ𝑥𝜑 | |
2 | 1 | nfsab 2812 | . 2 ⊢ Ⅎ𝑥 𝑧 ∈ {𝑦 ∣ 𝜑} |
3 | 2 | nfci 2964 | 1 ⊢ Ⅎ𝑥{𝑦 ∣ 𝜑} |
Colors of variables: wff setvar class |
Syntax hints: Ⅎwnf 1784 {cab 2799 Ⅎwnfc 2961 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-10 2145 ax-11 2161 ax-12 2177 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2800 df-nfc 2963 |
This theorem is referenced by: nfaba1 2986 nfun 4141 sbcel12 4360 sbceqg 4361 nfpw 4560 nfpr 4628 nfint 4886 intab 4906 nfiun 4949 nfiin 4950 nfiu1 4953 nfii1 4954 nfopab 5134 nfopab1 5135 nfopab2 5136 nfdm 5823 eusvobj2 7149 nfoprab1 7215 nfoprab2 7216 nfoprab3 7217 nfoprab 7218 fiun 7644 f1iun 7645 nfwrecs 7949 nfixpw 8480 nfixp 8481 nfixp1 8482 reclem2pr 10470 nfwrd 13894 mreiincl 16867 lss1d 19735 disjabrex 30332 disjabrexf 30333 esumc 31310 bnj900 32201 bnj1014 32233 bnj1123 32258 bnj1307 32295 bnj1398 32306 bnj1444 32315 bnj1445 32316 bnj1446 32317 bnj1447 32318 bnj1467 32326 bnj1518 32336 bnj1519 32337 dfon2lem3 33030 nffrecs 33120 sdclem1 35033 heibor1 35103 dihglblem5 38449 ssfiunibd 41596 hoidmvlelem1 42897 nfsetrecs 44809 setrec2lem2 44817 setrec2 44818 |
Copyright terms: Public domain | W3C validator |