Metamath Proof Explorer


Theorem nfoprab2

Description: The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 25-Apr-1995) (Revised by David Abernethy, 30-Jul-2012)

Ref Expression
Assertion nfoprab2 _ y x y z | φ

Proof

Step Hyp Ref Expression
1 df-oprab x y z | φ = w | x y z w = x y z φ
2 nfe1 y y z w = x y z φ
3 2 nfex y x y z w = x y z φ
4 3 nfab _ y w | x y z w = x y z φ
5 1 4 nfcxfr _ y x y z | φ