Metamath Proof Explorer


Theorem nfopab

Description: Bound-variable hypothesis builder for class abstraction. (Contributed by NM, 1-Sep-1999) Remove disjoint variable conditions. (Revised by Andrew Salmon, 11-Jul-2011)

Ref Expression
Hypothesis nfopab.1 z φ
Assertion nfopab _ z x y | φ

Proof

Step Hyp Ref Expression
1 nfopab.1 z φ
2 df-opab x y | φ = w | x y w = x y φ
3 nfv z w = x y
4 3 1 nfan z w = x y φ
5 4 nfex z y w = x y φ
6 5 nfex z x y w = x y φ
7 6 nfab _ z w | x y w = x y φ
8 2 7 nfcxfr _ z x y | φ