| 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 2377. See nfabg 2912 for a less restrictive version requiring more axioms. (Revised by GG, 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 2893 | 1 ⊢ Ⅎ𝑥{𝑦 ∣ 𝜑} |
| Colors of variables: wff setvar class |
| Syntax hints: Ⅎwnf 1783 {cab 2714 Ⅎwnfc 2890 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-10 2141 ax-11 2157 ax-12 2177 |
| This theorem depends on definitions: df-bi 207 df-ex 1780 df-nf 1784 df-sb 2065 df-clab 2715 df-nfc 2892 |
| This theorem is referenced by: nfaba1OLD 2914 nfunOLD 4171 sbcel12 4411 sbceqg 4412 nfpw 4619 nfpr 4692 nfint 4956 intab 4978 nfiun 5023 nfiin 5024 nfiu1OLD 5028 nfii1 5029 nfopab1 5213 nfopab2 5214 nfdm 5962 eusvobj2 7423 nfoprab1 7494 nfoprab2 7495 nfoprab3 7496 nfoprab 7497 fiun 7967 f1iun 7968 nffrecs 8308 nfwrecsOLD 8342 nfixpw 8956 nfixp 8957 nfixp1 8958 reclem2pr 11088 nfwrd 14581 mreiincl 17639 lss1d 20961 iinabrex 32582 disjabrex 32595 disjabrexf 32596 esumc 34052 bnj900 34943 bnj1014 34975 bnj1123 35000 bnj1307 35037 bnj1398 35048 bnj1444 35057 bnj1445 35058 bnj1446 35059 bnj1447 35060 bnj1467 35068 bnj1518 35078 bnj1519 35079 fineqvrep 35109 dfon2lem3 35786 sdclem1 37750 heibor1 37817 dihglblem5 41300 ssfiunibd 45321 hoidmvlelem1 46610 nfsetrecs 49205 setrec2lem2 49213 setrec2 49214 |
| Copyright terms: Public domain | W3C validator |