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 2727 | . 2 ⊢ Ⅎ𝑥 𝑧 ∈ {𝑦 ∣ 𝜑} |
3 | 2 | nfci 2887 | 1 ⊢ Ⅎ𝑥{𝑦 ∣ 𝜑} |
Colors of variables: wff setvar class |
Syntax hints: Ⅎwnf 1791 {cab 2714 Ⅎwnfc 2884 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-10 2141 ax-11 2158 ax-12 2175 |
This theorem depends on definitions: df-bi 210 df-ex 1788 df-nf 1792 df-sb 2071 df-clab 2715 df-nfc 2886 |
This theorem is referenced by: nfaba1 2912 nfun 4079 sbcel12 4323 sbceqg 4324 nfpw 4534 nfpr 4606 nfint 4869 intab 4889 nfiun 4934 nfiin 4935 nfiu1 4938 nfii1 4939 nfopab1 5123 nfopab2 5124 nfdm 5820 eusvobj2 7206 nfoprab1 7272 nfoprab2 7273 nfoprab3 7274 nfoprab 7275 fiun 7716 f1iun 7717 nffrecs 8025 nfwrecs 8049 nfixpw 8597 nfixp 8598 nfixp1 8599 reclem2pr 10662 nfwrd 14098 mreiincl 17099 lss1d 20000 iinabrex 30627 disjabrex 30640 disjabrexf 30641 esumc 31731 bnj900 32622 bnj1014 32654 bnj1123 32679 bnj1307 32716 bnj1398 32727 bnj1444 32736 bnj1445 32737 bnj1446 32738 bnj1447 32739 bnj1467 32747 bnj1518 32757 bnj1519 32758 fineqvrep 32777 dfon2lem3 33480 sdclem1 35638 heibor1 35705 dihglblem5 39049 ssfiunibd 42521 hoidmvlelem1 43808 nfsetrecs 46063 setrec2lem2 46071 setrec2 46072 |
Copyright terms: Public domain | W3C validator |