| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > nfab1 | Structured version Visualization version GIF version | ||
| Description: Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.) |
| Ref | Expression |
|---|---|
| nfab1 | ⊢ Ⅎ𝑥{𝑥 ∣ 𝜑} |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfsab1 2722 | . 2 ⊢ Ⅎ𝑥 𝑦 ∈ {𝑥 ∣ 𝜑} | |
| 2 | 1 | nfci 2893 | 1 ⊢ Ⅎ𝑥{𝑥 ∣ 𝜑} |
| Colors of variables: wff setvar class |
| Syntax hints: {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 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-ex 1780 df-nf 1784 df-sb 2065 df-clab 2715 df-nfc 2892 |
| This theorem is referenced by: nfabd2 2929 eqabf 2935 abid2fOLD 2937 nfrab1 3457 elabgf 3674 nfsbc1d 3806 ss2ab 4062 ab0ALT 4381 euabsn 4726 iunab 5051 iinab 5068 zfrep4 5293 rnep 5937 sniota 6552 opabiotafun 6989 nfixp1 8958 scottexs 9927 scott0s 9928 cp 9931 symgval 19388 ofpreima 32675 algextdeglem6 33763 qqhval2 33983 esum2dlem 34093 sigaclcu2 34121 bnj1366 34843 bnj1321 35041 bnj1384 35046 currysetlem 36946 currysetlem1 36948 bj-reabeq 37028 mptsnunlem 37339 topdifinffinlem 37348 scottabf 44259 compab 44461 ssfiunibd 45321 absnsb 47039 setrec2lem2 49213 |
| Copyright terms: Public domain | W3C validator |