Metamath Proof Explorer


Theorem nfabd2

Description: Bound-variable hypothesis builder for a class abstraction. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by Mario Carneiro, 8-Oct-2016) (Proof shortened by Wolf Lammen, 10-May-2023) (New usage is discouraged.)

Ref Expression
Hypotheses nfabd2.1 yφ
nfabd2.2 φ¬xx=yxψ
Assertion nfabd2 φ_xy|ψ

Proof

Step Hyp Ref Expression
1 nfabd2.1 yφ
2 nfabd2.2 φ¬xx=yxψ
3 nfnae y¬xx=y
4 1 3 nfan yφ¬xx=y
5 4 2 nfabd φ¬xx=y_xy|ψ
6 5 ex φ¬xx=y_xy|ψ
7 nfab1 _yy|ψ
8 eqidd xx=yy|ψ=y|ψ
9 8 drnfc1 xx=y_xy|ψ_yy|ψ
10 7 9 mpbiri xx=y_xy|ψ
11 6 10 pm2.61d2 φ_xy|ψ