# Metamath Proof Explorer

## Theorem nfrabw

Description: A variable not free in a wff remains so in a restricted class abstraction. Version of nfrab with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 13-Oct-2003) (Revised by Gino Giotto, 10-Jan-2024)

Ref Expression
Hypotheses nfrabw.1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
nfrabw.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
Assertion nfrabw ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left\{{y}\in {A}|{\phi }\right\}$

### Proof

Step Hyp Ref Expression
1 nfrabw.1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
2 nfrabw.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
3 df-rab ${⊢}\left\{{y}\in {A}|{\phi }\right\}=\left\{{y}|\left({y}\in {A}\wedge {\phi }\right)\right\}$
4 nftru ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\top$
5 2 nfcri ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{y}\in {A}$
6 5 a1i ${⊢}\top \to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{y}\in {A}$
7 1 a1i ${⊢}\top \to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
8 6 7 nfand ${⊢}\top \to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}\wedge {\phi }\right)$
9 4 8 nfabdw ${⊢}\top \to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left\{{y}|\left({y}\in {A}\wedge {\phi }\right)\right\}$
10 9 mptru ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left\{{y}|\left({y}\in {A}\wedge {\phi }\right)\right\}$
11 3 10 nfcxfr ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left\{{y}\in {A}|{\phi }\right\}$