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) (Revised by Scott Fenton, 26-Oct-2024)

Ref Expression
Hypothesis nfopab.1 zφ
Assertion nfopab _zxy|φ

Proof

Step Hyp Ref Expression
1 nfopab.1 zφ
2 nftru x
3 nftru y
4 1 a1i zφ
5 2 3 4 nfopabd _zxy|φ
6 5 mptru _zxy|φ