![]() |
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 2371. See nfabg 2911 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 2723 | . 2 ⊢ Ⅎ𝑥 𝑧 ∈ {𝑦 ∣ 𝜑} |
3 | 2 | nfci 2887 | 1 ⊢ Ⅎ𝑥{𝑦 ∣ 𝜑} |
Colors of variables: wff setvar class |
Syntax hints: Ⅎwnf 1786 {cab 2710 Ⅎwnfc 2884 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-10 2138 ax-11 2155 ax-12 2172 |
This theorem depends on definitions: df-bi 206 df-ex 1783 df-nf 1787 df-sb 2069 df-clab 2711 df-nfc 2886 |
This theorem is referenced by: nfaba1 2912 nfun 4126 sbcel12 4369 sbceqg 4370 nfpw 4580 nfpr 4652 nfint 4918 intab 4940 nfiun 4985 nfiin 4986 nfiu1 4989 nfii1 4990 nfopab1 5176 nfopab2 5177 nfdm 5907 eusvobj2 7350 nfoprab1 7419 nfoprab2 7420 nfoprab3 7421 nfoprab 7422 fiun 7876 f1iun 7877 nffrecs 8215 nfwrecsOLD 8249 nfixpw 8857 nfixp 8858 nfixp1 8859 reclem2pr 10989 nfwrd 14437 mreiincl 17481 lss1d 20439 iinabrex 31533 disjabrex 31546 disjabrexf 31547 esumc 32707 bnj900 33598 bnj1014 33630 bnj1123 33655 bnj1307 33692 bnj1398 33703 bnj1444 33712 bnj1445 33713 bnj1446 33714 bnj1447 33715 bnj1467 33723 bnj1518 33733 bnj1519 33734 fineqvrep 33753 dfon2lem3 34416 sdclem1 36248 heibor1 36315 dihglblem5 39807 ssfiunibd 43630 hoidmvlelem1 44922 nfsetrecs 47217 setrec2lem2 47225 setrec2 47226 |
Copyright terms: Public domain | W3C validator |