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 φ
nfrabw.2 _ x A
Assertion nfrabw _ x y A | φ

Proof

Step Hyp Ref Expression
1 nfrabw.1 x φ
2 nfrabw.2 _ x A
3 df-rab y A | φ = y | y A φ
4 nftru y
5 2 nfcri x y A
6 5 a1i x y A
7 1 a1i x φ
8 6 7 nfand x y A φ
9 4 8 nfabdw _ x y | y A φ
10 9 mptru _ x y | y A φ
11 3 10 nfcxfr _ x y A | φ