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	|- F/ y ph
	nfabd2.2	|- ( ( ph /\ -. A. x x = y ) -> F/ x ps )
Assertion	nfabd2	|- ( ph -> F/_ x { y | ps } )

Proof

Step	Hyp	Ref	Expression
1		nfabd2.1	|- F/ y ph
2		nfabd2.2	|- ( ( ph /\ -. A. x x = y ) -> F/ x ps )
3		nfnae	|- F/ y -. A. x x = y
4	1 3	nfan	|- F/ y ( ph /\ -. A. x x = y )
5	4 2	nfabd	|- ( ( ph /\ -. A. x x = y ) -> F/_ x { y | ps } )
6	5	ex	|- ( ph -> ( -. A. x x = y -> F/_ x { y | ps } ) )
7		nfab1	|- F/_ y { y | ps }
8		eqidd	|- ( A. x x = y -> { y | ps } = { y | ps } )
9	8	drnfc1	|- ( A. x x = y -> ( F/_ x { y | ps } <-> F/_ y { y | ps } ) )
10	7 9	mpbiri	|- ( A. x x = y -> F/_ x { y | ps } )
11	6 10	pm2.61d2	|- ( ph -> F/_ x { y | ps } )