![]() |
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 2366. See nfabg 2899 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 2716 | . 2 ⊢ Ⅎ𝑥 𝑧 ∈ {𝑦 ∣ 𝜑} |
3 | 2 | nfci 2879 | 1 ⊢ Ⅎ𝑥{𝑦 ∣ 𝜑} |
Colors of variables: wff setvar class |
Syntax hints: Ⅎwnf 1778 {cab 2703 Ⅎwnfc 2876 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-10 2130 ax-11 2147 ax-12 2167 |
This theorem depends on definitions: df-bi 206 df-ex 1775 df-nf 1779 df-sb 2061 df-clab 2704 df-nfc 2878 |
This theorem is referenced by: nfaba1OLD 2901 nfunOLD 4163 sbcel12 4405 sbceqg 4406 nfpw 4616 nfpr 4689 nfint 4956 intab 4978 nfiun 5023 nfiin 5024 nfiu1OLD 5028 nfii1 5029 nfopab1 5215 nfopab2 5216 nfdm 5949 eusvobj2 7408 nfoprab1 7478 nfoprab2 7479 nfoprab3 7480 nfoprab 7481 fiun 7948 f1iun 7949 nffrecs 8290 nfwrecsOLD 8324 nfixpw 8937 nfixp 8938 nfixp1 8939 reclem2pr 11082 nfwrd 14546 mreiincl 17604 lss1d 20936 iinabrex 32489 disjabrex 32502 disjabrexf 32503 esumc 33897 bnj900 34787 bnj1014 34819 bnj1123 34844 bnj1307 34881 bnj1398 34892 bnj1444 34901 bnj1445 34902 bnj1446 34903 bnj1447 34904 bnj1467 34912 bnj1518 34922 bnj1519 34923 fineqvrep 34944 dfon2lem3 35622 sdclem1 37457 heibor1 37524 dihglblem5 41010 ssfiunibd 44960 hoidmvlelem1 46252 nfsetrecs 48468 setrec2lem2 48476 setrec2 48477 |
Copyright terms: Public domain | W3C validator |